implement lambda abstraction and application

grammar/hindley-milner.cf

@@ -10,6 +10,8 @@ EIf.     Exp1 ::= "if" Exp1 "then" Exp1 "else" Exp1 ;
 EIsZero. Exp2 ::= "iszero" "(" Exp ")" ;
 ETyped.  Exp  ::= Exp1 ":" Type ;
 ELet.    Exp1 ::= "let" Pattern "=" Exp1 "in" ScopedExp ;
+EAbs.    Exp1 ::= "λ" Pattern ":" Type "." ScopedExp ;
+EApp.    Exp1 ::= Exp1 Exp2 ;
 
 ScopedExp. ScopedExp ::= Exp1 ;
 
@@ -18,3 +20,4 @@ coercions Exp 3 ;
 
 TNat.  Type ::= "Nat" ;
 TBool. Type ::= "Bool" ;
+TArrow. Type ::= Type "->" Type ;

src/HM/Eval.hs

@@ -1,10 +1,15 @@
 {-# LANGUAGE LambdaCase #-}
+
 module HM.Eval where
 
-import           Control.Monad.Foil      (Distinct, Scope, addSubst,
-                                          identitySubst)
-import           Control.Monad.Free.Foil (AST (Var), substitute)
-import           HM.Syntax
+import Control.Monad.Foil
+  ( Distinct,
+    Scope,
+    addSubst,
+    identitySubst,
+  )
+import Control.Monad.Free.Foil (AST (Var), substitute)
+import HM.Syntax
 
 -- $setup
 -- >>> :set -XOverloadedStrings
@@ -14,7 +19,7 @@
 -- Right "true"
 -- >>> eval emptyScope "if (iszero (2 - (true + 1))) then true else 0"
 -- Left "Unsupported expression in addition"
-eval :: Distinct n => Scope n -> Exp n -> Either String (Exp n)
+eval :: (Distinct n) => Scope n -> Exp n -> Either String (Exp n)
 eval _scope (Var x) = Right (Var x)
 eval _scope ETrue = Right ETrue
 eval _scope EFalse = Right EFalse
@@ -24,26 +29,36 @@
   r' <- eval scope r
   case (l', r') of
     (ENat x, ENat y) -> Right (ENat (x + y))
-    _                -> Left "Unsupported expression in addition"
+    _ -> Left "Unsupported expression in addition"
 eval scope (ESub l r) = do
   l' <- eval scope l
   r' <- eval scope r
   case (l', r') of
     (ENat x, ENat y) -> Right (ENat (x - y))
-    _                -> Left "Unsupported expression in subtraction"
+    _ -> Left "Unsupported expression in subtraction"
 eval scope (EIf cond then_ else_) = do
   cond' <- eval scope cond
   case cond' of
-    ETrue  -> eval scope then_
+    ETrue -> eval scope then_
     EFalse -> eval scope else_
-    _      -> Left "Unsupported condition in if statement"
-eval scope (EIsZero n) = eval scope n >>= \case
-  ENat n'
-    | n' == 0   -> Right ETrue
-    | otherwise -> Right EFalse
-  _       -> Left "Unsupported expression in iszero"
+    _ -> Left "Unsupported condition in if statement"
+eval scope (EIsZero n) =
+  eval scope n >>= \case
+    ENat n'
+      | n' == 0 -> Right ETrue
+      | otherwise -> Right EFalse
+    _ -> Left "Unsupported expression in iszero"
 eval scope (ETyped e _) = eval scope e
 eval scope (ELet e1 x e2) = do
   e1' <- eval scope e1
   let subst = addSubst identitySubst x e1'
   eval scope (substitute scope subst e2)
+eval _scope (EAbs type_ x e) = Right (EAbs type_ x e)
+eval scope (EApp e1 e2) = do
+  e1' <- eval scope e1
+  e2' <- eval scope e2
+  case e1' of
+    EAbs _ x e -> do
+      let subst = addSubst identitySubst x e2'
+      eval scope (substitute scope subst e)
+    _ -> Left "Unsupported expression in application"

src/HM/Parser/Abs.hs

@@ -29,12 +29,14 @@ data Exp
     | EIsZero Exp
     | ETyped Exp Type
     | ELet Pattern Exp ScopedExp
+    | EAbs Pattern Type ScopedExp
+    | EApp Exp Exp
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
 
 data ScopedExp = ScopedExp Exp
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
 
-data Type = TNat | TBool
+data Type = TNat | TBool | TArrow Type Type
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic)
 
 newtype Ident = Ident String

src/HM/Parser/Doc.txt

@@ -27,11 +27,11 @@ The set of reserved words is the set of terminals appearing in the grammar. Thos
 The reserved words used in Parser are the following:
   | ``Bool`` | ``Nat`` | ``else`` | ``false``
   | ``if`` | ``in`` | ``iszero`` | ``let``
-  | ``then`` | ``true`` |  |
+  | ``then`` | ``true`` | ``λ`` |
 
 The symbols used in Parser are the following:
   | + | - | ( | )
-  | : | = |  |
+  | : | = | . | ->
 
 ===Comments===
 There are no single-line comments in the grammar.There are no multiple-line comments in the grammar.
@@ -54,12 +54,15 @@ All other symbols are terminals.
   |  |  **|**  | //Exp3//
   | //Exp1// | -> | ``if`` //Exp1// ``then`` //Exp1// ``else`` //Exp1//
   |  |  **|**  | ``let`` //Pattern// ``=`` //Exp1// ``in`` //ScopedExp//
+  |  |  **|**  | ``λ`` //Pattern// ``:`` //Type// ``.`` //ScopedExp//
+  |  |  **|**  | //Exp1// //Exp2//
   |  |  **|**  | //Exp2//
   | //Exp// | -> | //Exp1// ``:`` //Type//
   |  |  **|**  | //Exp1//
   | //ScopedExp// | -> | //Exp1//
   | //Type// | -> | ``Nat``
   |  |  **|**  | ``Bool``
+  |  |  **|**  | //Type// ``->`` //Type//