***********************************************************************
* A Direct Denotational Semantics for the Eager Functional Language   *
* from Chapter 11 of Reynolds                                         *
***********************************************************************

Written by Paul Hudak.

> module EagerFL where

SYNTAX
======

Some type synonyms to use Reynolds names:

> type NatConst  = Int		-- but should not include negative numbers
> type BoolConst = Bool
> type Tag       = NatConst

> data Exp = 
> -- constants:
>     NatConst NatConst		-- integer literals
>   | BoolConst BoolConst	-- booleans
>   | Nil			-- nil
> -- arithmetic:
>   | Neg Exp			-- negation
>   | Exp :+: Exp		-- addition
>   | Exp :-: Exp		-- subtraction
>   | Exp :*: Exp		-- multiplication
>   | Exp :/: Exp		-- division
>   | Exp `Rem` Exp		-- remainder
> -- relational operators:
>   | Exp :=:  Exp		-- equality
>   | Exp :/=: Exp		-- inequality
>   | Exp :<:  Exp		-- less than
>   | Exp :<=: Exp		-- less than or equal
>   | Exp :>:  Exp		-- greater than
>   | Exp :>=: Exp		-- greater than or equal
> -- logical operators:
>   | Not Exp			-- negation
>   | Exp :/\:  Exp		-- conjunction (and)
>   | Exp :\/:  Exp		-- disjunction (or)
>   | Exp :=>:  Exp		-- implication
>   | Exp :<=>: Exp		-- if and only if
> -- conditional:
>   | If Exp Exp Exp            -- conditional
> -- variables, lambdas, and applications:
>   | Var Var			-- variables
>   | App Exp Exp		-- applications
>   | Lam Pat Exp		-- functions with pattern arguments
> -- tuples:
>   | Tup [Exp]			-- tuples
>   | Prj Exp Tag		-- tuple projection
> -- sums:
>   | Sum Tag Exp		-- sums (i.e. alternatives; tagged values)
>   | SumCase Exp [Exp]		-- sum discrimination (i.e. case)
> -- errors:
>   | Error			-- run-time error
>   | TypeError			-- type error
> -- binding forms:
>   | Let    [(Pat,Exp)] Exp	-- let expression
>   | LetRec [(Var,Pat,Exp)] Exp-- recursive let expression
>   deriving (Eq, Show)
>
> data Pat = Pat1 Var
>          | Pat2 [Pat]
>   deriving (Eq, Show)

Variables are just strings:

> type Var = String

FIXITIES
========

> infixl 9 :*:, :/:, `Rem`
> infixl 8 :-:, :+:
> infix  7 :=:, :/=:, :<:, :>:, :<=:, :>=:
> infixl 6 :/\:
> infixl 5 :\/:
> infixr 4 :=>:
> infixr 3 :<=>:

SEMANTIC DOMAINS
================

> data VStar = Norm V
>            | Err  Err
>      deriving (Eq,Show)
>
> data Err   = DynErr
>            | TypErr
>      deriving (Eq,Show)
>
> data V     = VInt  Int
>            | VBool Bool
>            | VNil
>            | VTup  [V]
>            | VSum  (Int, V)
>            | VFun  (V -> VStar)
>      deriving (Eq,Show)
>
> instance Show (V -> VStar) where
>   show f = "[Function]"
>
> instance Eq (V -> VStar) where
>   f == g  =  False
>
> err   = Err  DynErr
> tyerr = Err  TypErr
> nil   = Norm VNil

AUXILIARY FUNCTIONS 
===================

Projections:

> i_norm = Norm
>
> i_int  = VInt
> i_bool = VBool
> i_tup  = VTup
> i_alt  = VSum
> i_fun  = VFun

Error propagation:

> (***) :: (V -> VStar) -> (VStar -> VStar)
> f *** Norm z = f z
> f *** Err e  = Err e

Type checking:

> int ::  (Int -> VStar) -> (V -> VStar)
> f `int`  VInt i  = f i
> f `int`  _       = tyerr
>
> bool :: (Bool -> VStar) -> (V -> VStar)
> f `bool` VBool b = f b
> f `bool` _       = tyerr
>
> tup ::  ([V] -> VStar) -> (V -> VStar)
> f `tup` VTup ts  = f ts
> f `tup` _        = tyerr
>
> alt ::  ((Int,V) -> VStar) -> (V -> VStar)
> f `alt`  VSum s  = f s
> f `alt`  _       = tyerr
>
> fun ::  ((V->VStar) -> VStar) -> (V -> VStar)
> f `fun`  VFun g  = f g
> f `fun`  _       = tyerr

Both error propagation and type-checking:

> f `ints`  x = ((f `int`)  ***) x
> f `bools` x = ((f `bool`) ***) x
> f `tups`  x = ((f `tup`)  ***) x
> f `alts`  x = ((f `alt`)  ***) x
> f `funs`  x = ((f `fun`)  ***) x

Note the following equivalences:

Reynolds  Haskell
--------------------
f_*       (f ***)
f_int     (f `int`)
f_int*    (f `ints`)
etc.

ENVIRONMENTS
============

> type E = Var -> V
>
> extend :: E -> Var -> V -> E
> extend e v i v' = if v == v' then i else e v'

So "extend s v i" is equivalent to "s [v:i]" in Reynolds.

> emptyE x = error ("Unbound variable: " ++ x)

Syntax Expansion
================

An infinite supply of fresh variabes, using the convention that no
variable name in the program begins with "_":

> names = map (("_"++).show) [0..]

SEMANTICS
=========

The key semantic function:

> meaning :: Exp -> E -> VStar
> meaning = mean . desugar

After desugaring:

> mean :: Exp -> E -> VStar
> -- constants:
> mean Nil           eta = nil
> mean Error         eta = err
> mean TypeError     eta = tyerr
> mean (NatConst k)  eta = i_norm (i_int  k)
> mean (BoolConst b) eta = i_norm (i_bool b)
>
> -- unops:
> mean (Neg e) eta = (\i -> i_norm (i_int  (-i)))    `ints`  mean e eta
> mean (Not e) eta = (\b -> i_norm (i_bool (not b))) `bools` mean e eta
>
> -- binops:
> mean (e :+:  e')  eta = binop i_int  ints  (+)  e e' eta
> mean (e :-:  e')  eta = binop i_int  ints  (-)  e e' eta
> mean (e :*:  e')  eta = binop i_int  ints  (*)  e e' eta
> mean (e :/=: e')  eta = binop i_bool ints  (/=) e e' eta
> mean (e :<:  e')  eta = binop i_bool ints  (<)  e e' eta
> mean (e :>:  e')  eta = binop i_bool ints  (>)  e e' eta
> mean (e :<=: e')  eta = binop i_bool ints  (<=) e e' eta
> mean (e :>=: e')  eta = binop i_bool ints  (>=) e e' eta
> mean (e :/\: e')  eta = binop i_bool bools (&&) e e' eta
> mean (e :\/: e')  eta = binop i_bool bools (||) e e' eta
> mean (e :=>: e')  eta = binop i_bool bools  f   e e' eta
>   where f b b' = if b then b' else True   -- not b || b'
> mean (e :<=>: e') eta = binop i_bool bools  f   e e' eta
>   where f b b' = if b then b' else not b' -- (b&&b')||(not (b||b'))
>
> -- equality:
> -- mean (e :=:  e')  eta = binop i_bool ints  (==) e e' eta
> mean (e :=:  e')  eta =
>   (\i -> (\i' -> i_norm (i_bool (i==i'))) *** mean e' eta) *** mean e  eta
>
> -- division and remainder:
> mean (e :/: e') eta =
>   (\i -> (\i' -> if i'==0 then err
>                  else i_norm (i_int (i `div` i'))) `ints` (mean e' eta))
>                                                    `ints` (mean e  eta)
> mean (e `Rem` e') eta =
>   (\i -> (\i' -> if i'==0 then err
>                  else i_norm (i_int (i `rem` i'))) `ints` (mean e' eta))
>                                                    `ints` (mean e  eta)
> -- conditional
> mean (If b c a) eta =
>   (\b -> if b then mean c eta else mean a eta) `bools` mean b eta
>
> -- vars, apps, and lambdas:
> mean (Var v) eta = i_norm (eta v)
>
> mean (App e e') eta =
>   (\f -> (\x -> f x) *** mean e' eta) `funs` mean e eta
>
> mean (Lam (Pat1  v) e) eta =
>   i_norm (i_fun (\z -> mean e (extend eta v z)))
> mean (Lam (Pat2 ps) e) eta = 
>   error "Lambda patterns should be desugared."
>
> -- tuples
> mean (Tup es) eta =
>   (\zs -> i_norm (i_tup zs)) `tups` 
>   foldr f (Norm (VTup [])) (map (\e -> mean e eta) es)
>   where f (Err  e) vs               = Err e
>         f (Norm _) (Err e)          = Err e
>         f (Norm e) (Norm (VTup es)) = Norm (VTup (e:es))
>
> mean (Prj e k) eta =
>   (\ts -> if k < length ts
>           then i_norm (ts !! k)
>           else tyerr           ) `tups` mean e eta
>
> -- sums:
> mean (Sum k e) eta =
>   (\z -> i_norm (i_alt (k,z))) *** mean e eta
>
> mean (SumCase e fs) eta =
>   (\(k,z) -> if k < length fs 
>              then (\f -> f z) `funs` mean (fs!!k) eta
>              else tyerr                                 )
>   `alts` mean e eta
>
> -- let expression:
> mean (Let eqns e) eta = error "Let expression should be desugared."
>
> -- recursive let:
> mean (LetRec eqns e) eta = 
>   let eta' = foldr f eta eqns
>       f (v,Pat1 u,e) eta = extend eta v 
>                              (i_fun (\z -> mean e (extend eta' u z)))
>   in mean e eta'

Auxilliary function for strict binary operators:

> binop inj tc op e e' eta =
>   (\i -> (\i' -> i_norm (inj (op i i'))) `tc` (meaning e' eta))
>                                          `tc` (meaning e  eta)

DESUGARING
==========

Top-level desugaring:

> desugar :: Exp -> Exp
> desugar e = desug e [] names

Main desugaring function:

> desug :: Exp -> [(Var,Exp)] -> [Var] -> Exp
> -- constants:
> desug Nil           as vs = Nil
> desug Error         as vs = Error
> desug TypeError     as vs = TypeError
> desug (NatConst k)  as vs = NatConst k
> desug (BoolConst b) as vs = BoolConst b
>
> -- unops:
> desug (Neg e) as vs   = Neg (desug e as vs)
> desug (Not e) as vs   = Not (desug e as vs)
> desug (Prj e k) as vs = Prj (desug e as vs) k
> desug (Sum k e) as vs = Sum k (desug e as vs)
>
> -- binops:
> desug (e :+:   e') as vs = bDesug e e' (:+:)  as vs
> desug (e :-:   e') as vs = bDesug e e' (:-:)  as vs
> desug (e :*:   e') as vs = bDesug e e' (:*:)  as vs
> desug (e :=:   e') as vs = bDesug e e' (:=:)  as vs
> desug (e :/=:  e') as vs = bDesug e e' (:/=:) as vs
> desug (e :<:   e') as vs = bDesug e e' (:<:)  as vs
> desug (e :>:   e') as vs = bDesug e e' (:>:)  as vs
> desug (e :<=:  e') as vs = bDesug e e' (:<=:) as vs
> desug (e :>=:  e') as vs = bDesug e e' (:>=:) as vs
> desug (e :/\:  e') as vs = bDesug e e' (:/\:) as vs
> desug (e :\/:  e') as vs = bDesug e e' (:\/:) as vs
> desug (e :=>:  e') as vs = bDesug e e' (:=>:) as vs
> desug (e :<=>: e') as vs = bDesug e e' (:<=>:)as vs
> desug (e :/:   e') as vs = bDesug e e' (:/:)  as vs
> desug (e `Rem` e') as vs = bDesug e e'  Rem   as vs
> desug (App  e  e') as vs = bDesug e e'  App   as vs
>
> -- ternary op:
> desug (If b c a) as vs =
>   If (desug b as vs) (desug c as vs) (desug a as vs)
>
> -- n-ary ops:
> desug (Tup es)       as vs = 
>   Tup (map (\e -> desug e as vs) es)
> desug (SumCase e fs) as vs = 
>   SumCase (desug e as vs) (map (\e -> desug e as vs) fs)
>
> -- variables:
> desug (Var v) as vs = lookUp v as
>
> -- lambda:
> desug (Lam (Pat1  v) e) as    vs  = Lam (Pat1 v) (desug e as vs)
> desug (Lam (Pat2 ps) e) as (v:vs) =
>   let as' = depat ps (Var v) 0
>   in Lam (Pat1 v) (desug e (as'++as) vs)
>
> -- let expression:
> desug (Let eqns exp) as vs = 
>   desug (expand eqns) as vs
>   where expand  []          = exp
>         expand ((p,e):eqns) = App (Lam p (expand eqns)) e
>
> -- recursive let:
> desug (LetRec eqns e) as vs =
>   LetRec (map f eqns) (desug e as vs)
>   where f (v,p,e) =
>              let Lam p' e' = desug (Lam p e) as vs
>              in (v,p',e')

Auxilary functions for desugaring:

Binary operators:

> bDesug e1 e2 op as vs = desug e1 as vs `op` desug e2 as vs

Variable lookup:

> lookUp v as = case lookup v as of
>                 Just e  -> e
>                 Nothing -> Var v
>                         -- error ("Unknown variable: " ++ v)

Compiling patterns:

> depat []     e n = []
> depat (p:ps) e n = dep1 p e n ++ depat ps e (n+1)

> dep1 (Pat1 v)  e n = [(v, Prj e n)]
> dep1 (Pat2 ps) e n = depat ps (Prj e n) 0

TESTS
=====

> tpats = [Pat1 "a", Pat2 [Pat1 "b", Pat1 "c"], Pat1 "d"]
> t1 = depat tpats (Var "v") 0

t1 ==> [("a", Prj (Var "v") 0),
        ("b", Prj (Prj (Var "v") 1) 0),
        ("c", Prj (Prj (Var "v") 1) 1),
        ("d", Prj (Var "v") 2)]

> tlam = Lam (Pat2 tpats) (Var "b" :+: Var "d")
> t2 = desugar tlam

t2 ==> Lam (Pat1 "v0") (Prj (Prj (Var "v0") 1) 0 :+: Prj (Var "v0") 2)

Complete programs:
------------------

> test p = meaning p emptyE

Factorial:

> p1 = LetRec [("fac", Pat1 "n", 
>               If (Var "n" :=: NatConst 0)
>                  (NatConst 1)
>                  (Var "n" :*: App (Var "fac") (Var "n" :-: NatConst 1))
>              )]
>        (App (Var "fac") (NatConst 5))

test p1 ==> Norm (VInt 120)

Lists:

> listFns = [(Pat1 "cons",
>            Lam (Pat2 [Pat1 "x", Pat1 "xs"]) (Tup [Var "x", Var "xs"])),
>           (Pat1 "car",
>            Lam (Pat1 "xs") (Prj (Var "xs") 0)),
>           (Pat1 "cdr",
>            Lam (Pat1 "xs") (Prj (Var "xs") 1)),
>           (Pat1 "null",
>            Lam (Pat1 "xs") (Var "xs" :=: Nil))]

> alist = [(Pat1 "l1",
>           App (Var "cons") 
>               (Tup [NatConst 1,
>                     (App (Var "cons")
>                          (Tup [NatConst 2, Nil]))]))]

> p2 = Let (listFns++alist)
>          (App (Var "cdr") (Var "l1"))

test p2 ==> Norm (VTup [VInt 2,VNil])

These are from Reynolds: reduce (fold) and append (defined using reduce):

> red = ("reduce",
>        Pat2 [Pat1 "x", Pat1 "f", Pat1 "a"],
>        If (App (Var "null") (Var "x"))
>           (Var "a")
>           (App (App (Var "f") (App (Var "car") (Var "x")))
>                (App (Var "reduce") (Tup [App (Var "cdr") (Var "x"),
>                                          Var "f",
>                                          Var "a"]))))

> app = (Pat1 "append",
>        Lam (Pat2 [Pat1 "x", Pat1 "y"])
>            (App (Var "reduce")
>                 (Tup [Var "x",
>                       Lam (Pat1 "i")
>                           (Lam (Pat1 "z")
>                                (App (Var "cons") 
>                                     (Tup [Var "i",Var "z"]))),
>                       Var "y"])))

Test of append:

> p3 = Let (listFns++alist)
>          (LetRec [red]
>                  (Let [app]
>                       (App (Var "append")
>                            (Tup [Var "l1", Var "l1"]))))

test p3 ==> Norm (VTup [VInt 1,VTup [VInt 2,VTup [VInt 1,VTup [VInt 2,VNil]]]])

Desugaring of a variant of p4:

App(Lam(Pat1"cons")
    (App(Lam(Pat1"car")
         (App(Lam(Pat1"cdr")
              (App(Lam(Pat1"null")
                   (LetRec[("reduce",
                     Pat1"_0",
                     If(App(Var"null")
                           (Prj(Var"_0")0))
                       (Prj(Var"_0")2)
                       (App(App(Prj(Var"_0")1)
                               (App(Var"car")(Prj(Var"_0")0)))
                           (App(Var"reduce")
                               (Tup[App(Var"cdr")(Prj(Var"_0")0),
                                    Prj(Var"_0")1,
                                    Prj(Var"_0")2]))))]
                     (App(Lam(Pat1"append")
                          (App(Var"append")
                              (Tup[Nil,Nil])))
                         (Lam(Pat1"_0")(App(App(App(Var"reduce")
                                                   (Prj(Var"_0")0))
                                               (Lam(Pat1"i")
                                                (Lam(Pat1"z")
                                                 (App(Var"cons")
                                                     (Tup[Var"i",Var"z"])))))
                                           (Prj(Var"_0")1))))))
                  (Lam(Pat1"xs")(Var"xs":=:Nil))))
             (Lam(Pat1"xs")(Prj(Var"xs")1))))
        (Lam(Pat1"xs")(Prj(Var"xs")0))))
   (Lam(Pat1"_0")(Tup [Prj(Var"_0")0,Prj(Var"_0")1]))