having-effect, section 1, first-class-functions

Main.purs

-- | Some exercising for http://okmij.org/ftp/Computation/having-effect.html

module Main where

import Control.Monad.Eff.Console
import Control.Bind (bind)

import Data.Boolean (otherwise)
import Data.Eq ((==))
import Data.Semigroup ((<>))
import Data.Semiring ((+))
import Data.Show (class Show, show)

demo code expr = do
  log ("Running `" <> code <> "`")
  log ("=> " <> show (runDomEnv expr))
  log ""

main = do
  demo "incYou 42"
    (incYou <| int 42)
  
  demo "areYouEvenEqual 42 42"
    (areYouEvenEqual <| int 42 <| int 42)
  
  demo "areYouEvenEqual 42 41"
    (areYouEvenEqual <| int 42 <| int 41)
  
  demo "allThingsEqual 1 2 3 4 5"
    (allThingsEqual <| int 1 <| int 2 <| int 3 <| int 4 <| int 5)
  
  demo "allThingsEqual 1 1 1 1 1"
    (allThingsEqual <| int 1 <| int 1 <| int 1 <| int 1 <| int 1)
  
  demo "yCombinator 42"
    (yCombinator <| int 42)
  
  demo "yCombinator (\\x -> inc x)"
    (yCombinator <| (lam "x" (inc <| var "x")))

-- | Basic language. Primitives.
class EBasic d where
  int :: Int -> d
  inc :: d
  app :: d -> d -> d

infixl 1 app as <|

incInc2 :: forall d. EBasic d => d
incInc2 = inc <| (inc <| int 2)

-- | Conditional language. Conditionals and comparison.
class ECond d where
  equal :: d
  if_ :: d -> d -> d -> d

equal42Matter :: forall d. (EBasic d, ECond d) => d
equal42Matter =
  if_
    (equal <| int 42 <| int 42)
    (int 1)
    (int 0)

class Lam d where
  var :: VarName -> d
  lam :: VarName -> d -> d


-- | Domain for denotations.
data Dom
  = DInt  Int
  | DBool Boolean
  | DFun  (Dom -> Dom)
  | DErr  String

instance showDom :: Show Dom where
  show = case _ of
    DInt  a -> show a
    DBool a -> show a
    DFun  _ -> "<fn>"
    DErr  e -> "Error: " <> e

typeMismatch
  :: { label    :: String
     , expected :: String
     , got      :: Dom
     }
  -> Dom
typeMismatch { label, expected, got } =
  case got of
    DErr err -> DErr (label <> ": " <> err)
    _        -> DErr (label <> ": expected " <> expected <> ", got " <> typeOf got)

typeOf :: Dom -> String
typeOf = case _ of
  DInt  _ -> "int"
  DBool _ -> "bool"
  DFun  _ -> "fn"
  DErr  _ -> "err"

-- | Domain with an environment.
newtype DomEnv = DomEnv (Env -> Dom)

-- | Evaluate given `DomEnv` with given `Env`
withEnv :: DomEnv -> Env -> Dom
withEnv (DomEnv f) env = f env

-- | Evaluate `DomEnv` with empty environment
runDomEnv :: DomEnv -> Dom
runDomEnv = (_ `withEnv` emptyEnv)
  where
    emptyEnv = Env
      \name -> DErr (name <> " is undefined")

-- | Identifiers for variables.
type VarName = String

-- | Environment for variables.
newtype Env = Env (VarName -> Dom)

-- | Get a binding from an environment.
lookup :: VarName -> Env -> Dom
lookup name (Env env) = env name

-- | Add a binding to an environment
extend :: VarName -> Dom -> Env -> Env
extend name e (Env env) = Env
  \name1 ->
     if name == name1
     then e
     else env name1

instance domEnvBasic :: EBasic DomEnv where
  int a = DomEnv
    \_ -> DInt a

  inc = DomEnv
    \_ -> DFun
      case _ of
        DInt a -> DInt (a + 1)
        got    -> typeMismatch { label: "inc", expected: "int", got }

  app e1 e2 = DomEnv
    \env ->
      case e1 `withEnv` env of
        DFun f -> f (e2 `withEnv` env)
        got    -> typeMismatch { label: "app", expected: "fn", got }

instance domEnvCond :: ECond DomEnv where
  equal = DomEnv
    \env -> DFun
       case _ of
         DInt a -> DFun
           case _ of
             DInt b -> DBool (a == b)
             got -> typeMismatch { label: "equal<2>", expected: "int", got }
         got -> typeMismatch { label: "equal<1>", expected: "int", got }
         
  if_ e1 e2 e3 = DomEnv
    \env ->
      case e1 `withEnv` env of
        DBool cond
          | cond      -> e2 `withEnv` env
          | otherwise -> e3 `withEnv` env
        got -> typeMismatch { label: "if_<1>", expected: "bool", got }

instance domEnvLam :: Lam DomEnv where
  var name   = DomEnv (lookup name)
  lam name body = DomEnv
    \env -> DFun
       \value -> body `withEnv` extend name value env

incYou :: forall d. (EBasic d, Lam d) => d
incYou =
  lam "a"
    (inc <| var "a")

areYouEvenEqual :: forall d. (EBasic d, ECond d, Lam d) => d
areYouEvenEqual =
  lam "a"
    (lam "b"
      (if_ (equal <| var "a" <| var "b")
           (int 1)
           (int 0)))

allThingsEqual :: forall d. (EBasic d, ECond d, Lam d) => d
allThingsEqual =
  lam "a"
    (lam "b"
      (lam "c"
        (lam "d"
           (lam "e"
              (if_
                 (equal <| var "a" <| var "b")
                 (if_
                    (equal <| var "b" <| var "c")
                    (if_
                      (equal <| var "c" <| var "d")
                      (if_
                         (equal <| var "d" <| var "e")
                         (int 1) -- FINALLY
                         (int 0))
                      (int 0))
                    (int 0))
                 (int 0))))))

-- | Not sure if I got it right, but it blows the stack at that point I am happy.
yCombinator :: forall d. (EBasic d, Lam d) => d
yCombinator =
  lam "f"
    ((lam "x" (var "x" <| var "x"))
       <| (lam "x" (var "f" <| (var "x" <| var "x"))))