lambda-calculator 3.0.0.1 → 3.1.0.0

raw patch · 25 files changed

+1364/−277 lines, 25 filesdep +microlensPVP ok

version bump matches the API change (PVP)

Dependencies added: microlens

API changes (from Hackage documentation)

Files

• app/CliOptions.hs +10/−5
• app/Repl/SystemF.hs +2/−2
• lambda-calculator.cabal +21/−9
• scripts/HLint.hs +1/−1
• src/Language/Lambda/Shared/Errors.hs +8/−1
• src/Language/Lambda/Shared/UniqueSupply.hs +20/−2
• src/Language/Lambda/SystemF.hs +85/−11
• src/Language/Lambda/SystemF/Eval.hs +179/−0
• src/Language/Lambda/SystemF/Expression.hs +86/−18
• src/Language/Lambda/SystemF/Parser.hs +27/−12
• src/Language/Lambda/SystemF/State.hs +67/−30
• src/Language/Lambda/SystemF/TypeCheck.hs +134/−67
• src/Language/Lambda/Untyped.hs +1/−3
• test/Language/Lambda/SystemF/EvalSpec.hs +247/−0
• test/Language/Lambda/SystemF/Examples/BoolSpec.hs +30/−0
• test/Language/Lambda/SystemF/Examples/NatSpec.hs +75/−0
• test/Language/Lambda/SystemF/ExpressionSpec.hs +100/−57
• test/Language/Lambda/SystemF/HspecUtils.hs +65/−0
• test/Language/Lambda/SystemF/ParserSpec.hs +17/−1
• test/Language/Lambda/SystemF/TypeCheckSpec.hs +70/−49
• test/Language/Lambda/SystemFSpec.hs +111/−4
• test/Language/Lambda/Untyped/EvalSpec.hs +8/−2
• test/Language/Lambda/Untyped/Examples/BoolSpec.hs +0/−1
• test/Language/Lambda/Untyped/Examples/NatSpec.hs +0/−1
• test/Language/Lambda/Untyped/HspecUtils.hs +0/−1

@@ -29,13 +29,18 @@  cliParser :: Parser CliOptions cliParser = CliOptions -  <$> flag Untyped SystemF language+  <$> language   <*> switch version-  where language = long "system-f"-          <> short 'f'-          <> internal -- this is a secret feature-          <> help "Use the System F interpreter"+  where language = flag' SystemF systemF <|> flag Untyped Untyped untyped          version = long "version"           <> short 'v'           <> help "Print the version"++        systemF = long "system-f"+          <> short 'f'+          <> help "Use the System F interpreter"++        untyped = long "untyped"+          <> short 'l'+          <> help "Use the Untyped Lambda Calculus interpreter"

@@ -23,7 +23,7 @@ runSystemFRepl   = void . runExceptT . evalStateT (evalReplOpts replOpts) $ initialState   where replOpts = mkReplOpts banner' $ evalSystemF . pack-        initialState = mkTypecheckState defaultUniques+        initialState = mkTypecheckState defaultUniques defaultTyUniques  banner' :: MultiLine -> Repl String banner' _ = unpack <$> prompt (singleton upperLambda)@@ -34,7 +34,7 @@    let res = runTypecheck (evalText input) state'   case res of-    Left err -> liftIO . putStrLn . pack . show $ err+    Left err -> liftIO . putStrLn . textDisplay $ err     Right (res', newState) -> do       put newState       liftIO . putStrLn . prettyPrint $ res'

@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.34.7.+-- This file has been generated from package.yaml by hpack version 0.35.0. -- -- see: https://github.com/sol/hpack ----- hash: 4320ff01290c0c866383cba3463f4090d1413eb4efc9bff24cfae0496fd819f5+-- hash: 3256f86f253ee771f5e7374ff11bcb34286722368054e4e233095c13c9abe64b  name:           lambda-calculator-version:        3.0.0.1+version:        3.1.0.0 synopsis:       A lambda calculus interpreter description:    A simple implementation of the Untyped Lambda Calculus category:       LambdaCalculus,Language,Teaching@@ -15,7 +15,7 @@ bug-reports:    https://github.com/sgillespie/lambda-calculator/issues author:         Sean D Gillespie maintainer:     sean@mistersg.net-copyright:      2016 Sean Gillespie+copyright:      2016-2023 Sean Gillespie license:        MIT license-file:   LICENSE build-type:     Simple@@ -34,6 +34,7 @@       Language.Lambda.Untyped.Parser       Language.Lambda.Untyped.State       Language.Lambda.SystemF+      Language.Lambda.SystemF.Eval       Language.Lambda.SystemF.Expression       Language.Lambda.SystemF.Parser       Language.Lambda.SystemF.State@@ -67,6 +68,8 @@       MultiParamTypeClasses       MultiWayIf       NamedFieldPuns+      NoImplicitPrelude+      OverloadedStrings       PartialTypeSignatures       PatternGuards       PolyKinds@@ -78,12 +81,11 @@       TypeFamilies       TypeSynonymInstances       ViewPatterns-      NoImplicitPrelude-      OverloadedStrings   ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints   build-depends:       base >=4.9 && <5     , containers+    , microlens     , mtl     , parsec     , prettyprinter@@ -125,6 +127,8 @@       MultiParamTypeClasses       MultiWayIf       NamedFieldPuns+      NoImplicitPrelude+      OverloadedStrings       PartialTypeSignatures       PatternGuards       PolyKinds@@ -136,14 +140,13 @@       TypeFamilies       TypeSynonymInstances       ViewPatterns-      NoImplicitPrelude-      OverloadedStrings   ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N   build-depends:       base >=4.9 && <5     , bytestring     , containers     , lambda-calculator+    , microlens     , mtl     , optparse-applicative     , prettyprinter@@ -181,6 +184,8 @@       MultiParamTypeClasses       MultiWayIf       NamedFieldPuns+      NoImplicitPrelude+      OverloadedStrings       PartialTypeSignatures       PatternGuards       PolyKinds@@ -192,11 +197,11 @@       TypeFamilies       TypeSynonymInstances       ViewPatterns-      ImplicitPrelude   ghc-options: -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N   build-depends:       base >=4.9 && <5     , hlint+    , microlens     , mtl     , prettyprinter     , rio@@ -206,7 +211,11 @@   type: exitcode-stdio-1.0   main-is: Spec.hs   other-modules:+      Language.Lambda.SystemF.EvalSpec+      Language.Lambda.SystemF.Examples.BoolSpec+      Language.Lambda.SystemF.Examples.NatSpec       Language.Lambda.SystemF.ExpressionSpec+      Language.Lambda.SystemF.HspecUtils       Language.Lambda.SystemF.ParserSpec       Language.Lambda.SystemF.TypeCheckSpec       Language.Lambda.SystemFSpec@@ -245,6 +254,8 @@       MultiParamTypeClasses       MultiWayIf       NamedFieldPuns+      NoImplicitPrelude+      OverloadedStrings       PartialTypeSignatures       PatternGuards       PolyKinds@@ -263,6 +274,7 @@     , containers     , hspec     , lambda-calculator+    , microlens     , mtl     , prettyprinter     , rio

@@ -1,7 +1,7 @@ module Main (main) where  import Language.Haskell.HLint (hlint)-import System.Exit (exitFailure, exitSuccess)+import RIO  arguments :: [String] arguments = [ 

@@ -3,7 +3,8 @@     isLambdaException,     isLetError,     isParseError,-    isImpossibleError+    isImpossibleError,+    isTyMismatchError,   ) where  import RIO@@ -27,6 +28,7 @@   -- Examples:   --   --     (\x: X. x) (y:Y)+  --     (\x: T. x) [U]   | TyMismatchError Text    -- | A catch-all error that indicates a bug in this project@@ -38,6 +40,7 @@ instance Display LambdaException where   textDisplay (ParseError txt) = "Parse error " <> txt   textDisplay (InvalidLet txt) = "Illegal nested let: " <> txt+  textDisplay (TyMismatchError txt) = "Type error: " <> txt   textDisplay ImpossibleError = "An impossible error occurred! Please file a bug."  instance Show LambdaException where@@ -59,3 +62,7 @@ isImpossibleError :: LambdaException -> Bool isImpossibleError ImpossibleError = True isImpossibleError _ = False++isTyMismatchError :: LambdaException -> Bool+isTyMismatchError (TyMismatchError _) = True+isTyMismatchError _ = False

@@ -1,9 +1,27 @@ module Language.Lambda.Shared.UniqueSupply where +import Language.Lambda.Shared.Errors (LambdaException(..))++import Control.Monad.Except (MonadError(..), throwError) import RIO-import RIO.Text (pack)+import RIO.List (find)+import RIO.Text (pack, toUpper) -defaultUniques :: [Text]+type Unique = Text++defaultUniques :: [Unique] defaultUniques = map pack strings   where strings = concatMap (\p -> map (:p) . reverse $ ['a'..'z']) suffix         suffix = "" : map show [(0::Int)..]++defaultTyUniques :: [Unique]+defaultTyUniques = map toUpper defaultUniques++next+  :: (Ord name, MonadError LambdaException m)+  => [name] -- ^ Unique supply+  -> [name] -- ^ Free Variables+  -> m name+next freeVars uniques' = case find (`notElem` freeVars) uniques' of+  Just unique -> pure unique+  Nothing -> throwError ImpossibleError

@@ -1,26 +1,100 @@ module Language.Lambda.SystemF (-  Globals(),   evalText,+  typecheckText,+  runEvalText,+  runTypecheckText,+  execEvalText,+  execTypecheckText,+  unsafeExecEvalText,+  unsafeExecTypecheckText,+  defaultUniques,+  defaultTyUniques,+  mkState,    module Language.Lambda.SystemF.Expression,   module Language.Lambda.SystemF.Parser,   module Language.Lambda.SystemF.State   ) where -import Control.Monad.Except-import RIO-import qualified RIO.Text as Text-import qualified Data.Map as Map- import Language.Lambda.Shared.Errors+import Language.Lambda.Shared.UniqueSupply (defaultUniques, defaultTyUniques)+import Language.Lambda.SystemF.Eval (evalExpr) import Language.Lambda.SystemF.Expression import Language.Lambda.SystemF.Parser import Language.Lambda.SystemF.State+import Language.Lambda.SystemF.TypeCheck -type Globals = Map.Map String (SystemFExpr String String)+import Control.Monad.Except+import RIO+import qualified RIO.Text as Text+import qualified RIO.Map as Map -evalText :: Text -> Typecheck Text (SystemFExpr Text Text)-evalText text = case parseExpr text of-  Left err -> throwError $ ParseError $ Text.pack $ show err-  Right res -> return res+evalText+  :: Text+  -> Typecheck Text (TypedExpr Text)+evalText = either throwParseError processExpr . parseExpr+    where throwParseError = throwError . ParseError . Text.pack . show +typecheckText+  :: Text+  -> Typecheck Text (Ty Text)+typecheckText = either throwParseError typecheck . parseExpr+    where throwParseError = throwError . ParseError . Text.pack . show++runEvalText+  :: Text+  -> Globals Text+  -> Either LambdaException (TypedExpr Text, TypecheckState Text)+runEvalText input globals' = runTypecheck (evalText input) (mkState globals')++runTypecheckText+  :: Text+  -> Globals Text+  -> Either LambdaException (Ty Text, TypecheckState Text)+runTypecheckText input globals'+  = runTypecheck (typecheckText input) (mkState globals')++execEvalText+  :: Text+  -> Globals Text+  -> Either LambdaException (TypedExpr Text)+execEvalText input globals'+  = execTypecheck (evalText input) (mkState globals')++execTypecheckText+  :: Text+  -> Globals Text+  -> Either LambdaException (Ty Text)+execTypecheckText input globals'+  = execTypecheck (typecheckText input) (mkState globals')++unsafeExecEvalText+  :: Text+  -> Globals Text+  -> TypedExpr Text+unsafeExecEvalText input globals'+  = unsafeExecTypecheck (evalText input) (mkState globals')++unsafeExecTypecheckText+  :: Text+  -> Globals Text+  -> Ty Text+unsafeExecTypecheckText input globals'+  = unsafeExecTypecheck (typecheckText input) (mkState globals')++mkState :: Globals Text -> TypecheckState Text+mkState globals' = TypecheckState globals' defaultUniques defaultTyUniques++processExpr :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)+processExpr (Let n expr) = tcAndEval expr >>= addBinding n+processExpr expr = tcAndEval expr++tcAndEval :: SystemFExpr Text -> Typecheck Text (TypedExpr Text)+tcAndEval expr = do+  ty <- typecheck expr+  reduced <- evalExpr expr++  pure $ TypedExpr reduced ty++addBinding :: Text -> TypedExpr Text -> Typecheck Text (TypedExpr Text)+addBinding name expr = modifyGlobals (Map.insert name expr) >> pure expr

@@ -0,0 +1,179 @@+module Language.Lambda.SystemF.Eval+  ( evalExpr,+    subGlobals,+    betaReduce,+    alphaConvert,+    etaConvert,+    freeVarsOf+  ) where++import Language.Lambda.Shared.Errors+import Language.Lambda.Shared.UniqueSupply (next)+import Language.Lambda.SystemF.Expression+import Language.Lambda.SystemF.State++import Control.Monad.Except (throwError)+import Prettyprinter+import RIO+import qualified RIO.Map as Map++-- | Evaluates an expression+evalExpr+  :: (Pretty name, Ord name)+  => SystemFExpr name+  -> Typecheck name (SystemFExpr name)+evalExpr = evalTopLevel++-- | Evaluates a top-level expression+evalTopLevel+  :: (Pretty name, Ord name)+  => SystemFExpr name+  -> Typecheck name (SystemFExpr name)+evalTopLevel (Let n expr) = Let n <$> (subGlobals expr >>= evalInner)+evalTopLevel expr = subGlobals expr >>= evalInner++-- | Evaluates a non top-level expression. Does NOT support Lets+evalInner+  :: (Pretty name, Ord name)+  => SystemFExpr name+  -> Typecheck name (SystemFExpr name)+evalInner (Abs n ty expr) = Abs n ty <$> evalInner expr+evalInner (App e1 e2) = evalApp e1 e2+evalInner (TyAbs n expr) = TyAbs n <$> evalInner expr+evalInner (TyApp expr ty) = evalTyApp expr ty+evalInner (Let n expr) = throwError . InvalidLet . prettyPrint $ Let n expr+evalInner expr = pure expr++subGlobals :: Ord name => SystemFExpr name -> Typecheck name (SystemFExpr name)+subGlobals expr = getGlobals >>= subGlobals'+  where subGlobals' globals' = case expr of+          Var x -> pure . maybe expr (view _expr) $ globals' Map.!? x+          VarAnn x _ -> pure . maybe expr (view _expr) $ globals' Map.!? x+          App e1 e2 -> App <$> subGlobals e1 <*> subGlobals e2+          Abs name ty expr'+            | Map.member name globals' -> pure expr+            | otherwise -> Abs name ty <$> subGlobals expr'+          _ -> pure expr++evalApp+  :: (Pretty name, Ord name)+  => SystemFExpr name+  -> SystemFExpr name+  -> Typecheck name (SystemFExpr name)+evalApp e1 e2 = do+  e1' <- evalInner e1+  e2' <- evalInner e2++  betaReduce e1' e2'++evalTyApp+  :: (Pretty name, Ord name)+  => SystemFExpr name+  -> Ty name+  -> Typecheck name (SystemFExpr name)+evalTyApp expr ty = case expr of+  TyAbs name inner -> evalInner $ substituteTyInExpr ty name inner+  Abs name (TyForAll tyName ty') inner ->+    Abs name (substituteTy ty tyName ty') <$> evalInner inner+  VarAnn name (TyForAll tyName ty') -> pure $ VarAnn name (substituteTy ty tyName ty')+  _ -> TyApp <$> evalInner expr <*> pure ty++betaReduce+  :: (Ord name, Pretty name)+  => SystemFExpr name+  -> SystemFExpr name+  -> Typecheck name (SystemFExpr name)+betaReduce e1 e2 = case e1 of+  App e1' e2' -> App <$> betaReduce e1' e2' <*> pure e2+  Abs n _ e1' -> do+    converted <- alphaConvert (freeVarsOf e2) e1'+    evalInner $ substitute converted n e2+  Let _ _ -> throwError ImpossibleError+  _ -> pure $ App e1 e2++alphaConvert+  :: (Ord name, Pretty name)+  => [name]+  -> SystemFExpr name+  -> Typecheck name (SystemFExpr name)+alphaConvert freeVars (Abs name ty body) = do+  uniques <- getVarUniques+  nextName <- next freeVars uniques+  alphaConvertAbs name ty body freeVars nextName+alphaConvert _ expr = pure expr++etaConvert :: Ord name => SystemFExpr name -> SystemFExpr name+etaConvert (Abs name ty body) = case body of+  App e1 (Var name')+    | name == name' -> etaConvert e1+    | otherwise -> Abs name ty (App (etaConvert e1) (Var name'))+  body'@Abs{}+    | body' == eta' -> Abs name ty body'+    | otherwise -> etaConvert $ Abs name ty eta'+    where eta' = etaConvert body'+  _ -> Abs name ty $ etaConvert body+etaConvert (App e1 e2) = App (etaConvert e1) (etaConvert e2)+etaConvert expr = expr++substitute+  :: Eq name+  => SystemFExpr name+  -> name+  -> SystemFExpr name+  -> SystemFExpr name+substitute expr forName inExpr+  = case expr of+      (Var n)+        | n == forName -> inExpr+        | otherwise -> expr+      (VarAnn n _)+        | n == forName -> inExpr+        | otherwise -> expr+      (Abs n ty body)+        | n == forName -> expr+        | otherwise -> Abs n ty $ substitute body forName inExpr+      (App e1 e2) -> App (sub e1) (sub e2)+      (TyAbs n body) -> TyAbs n $ substitute body forName inExpr+      (TyApp body ty) -> TyApp (substitute body forName inExpr) ty+      _ -> inExpr+  where sub expr' = substitute expr' forName inExpr++substituteTyInExpr+  :: Eq name+  => Ty name+  -> name+  -> SystemFExpr name+  -> SystemFExpr name+substituteTyInExpr ty forName inExpr+  = case inExpr of+      VarAnn name ty' -> VarAnn name (substituteTy ty forName ty')+      App e1 e2 -> App (sub e1) (sub e2)+      Abs name ty' expr -> Abs name (substituteTy ty forName ty') (sub expr)+      TyAbs name expr -> TyAbs name (sub expr)+      TyApp expr ty' -> TyApp (sub expr) (substituteTy ty forName ty')+      _ -> inExpr+  where sub = substituteTyInExpr ty forName++freeVarsOf+  :: (Ord name, Pretty name)+  => SystemFExpr name+  -> [name]+freeVarsOf (Abs n _ expr) = filter (/=n) . freeVarsOf $ expr+freeVarsOf (App e1 e2) = freeVarsOf e1 ++ freeVarsOf e2+freeVarsOf (Var n) = [n]+freeVarsOf (VarAnn n _) = [n]+freeVarsOf (Let _ expr) = freeVarsOf expr+freeVarsOf (TyAbs _ expr) = freeVarsOf expr+freeVarsOf (TyApp expr _) = freeVarsOf expr++alphaConvertAbs+  :: (Ord name, Pretty name)+  => name+  -> Ty name+  -> SystemFExpr name+  -> [name]+  -> name+  -> Typecheck name (SystemFExpr name)+alphaConvertAbs name ty body freeVars nextName+  | name `elem` freeVars = pure $ Abs nextName ty (substitute body name (Var nextName))+  | otherwise = Abs name ty <$> alphaConvert freeVars body

@@ -1,7 +1,11 @@ module Language.Lambda.SystemF.Expression   ( SystemFExpr(..),+    TypedExpr(..),     Ty(..),+    _expr,+    _ty,     prettyPrint,+    substituteTy,     upperLambda   ) where @@ -10,46 +14,91 @@ import Prettyprinter.Render.Text (renderStrict) import RIO -data SystemFExpr name ty+data SystemFExpr name+  -- | A global binding: `let x = y`+  = Let name (SystemFExpr name)   -- | Variable: `x`-  = Var name+  | Var name+  -- | Variable annotated with type: `x:T`+  | VarAnn name (Ty name)   -- | Function application: `x y`-  | App (SystemFExpr name ty) (SystemFExpr name ty)+  | App (SystemFExpr name) (SystemFExpr name)   -- | Lambda abstraction: `\x: X. x`-  | Abs name (Ty ty) (SystemFExpr name ty)+  | Abs name (Ty name) (SystemFExpr name)   -- | Type Abstraction: `\X. body`-  | TyAbs ty (SystemFExpr name ty)                  +  | TyAbs name (SystemFExpr name)   -- | Type Application: `x [X]`-  | TyApp (SystemFExpr name ty) (Ty ty)+  | TyApp (SystemFExpr name) (Ty name)   deriving (Eq, Show) +data TypedExpr name = TypedExpr+  { teExpr :: SystemFExpr name,+    teTy :: Ty name+  } deriving (Eq, Show)+ data Ty name   = TyVar name                  -- ^ Type variable (T)   | TyArrow (Ty name) (Ty name) -- ^ Type arrow    (T -> U)   | TyForAll name (Ty name)     -- ^ Universal type (forall T. X)-  deriving (Eq, Show)+  deriving (Show) -instance (Pretty name, Pretty ty) => Pretty (SystemFExpr name ty) where+instance (Pretty name) => Pretty (SystemFExpr name) where   pretty (Var name) = pretty name+  pretty (VarAnn name ty) = prettyVarAnn name ty   pretty (App e1 e2) = prettyApp e1 e2   pretty (Abs name ty body) = prettyAbs name ty body+  pretty (Let name expr) = prettyLet name expr   pretty (TyAbs ty body) = prettyTyAbs ty body   pretty (TyApp expr ty) = prettyTyApp expr ty +instance Pretty name => Pretty (TypedExpr name) where+  pretty expr = pretty (expr ^. _expr) <+> colon <+> pretty (expr ^. _ty)+ instance Pretty name => Pretty (Ty name) where   pretty = prettyTy False +instance Eq name => Eq (Ty name) where+  (==) = isTyEquivalent++_expr :: Lens' (TypedExpr name) (SystemFExpr name)+_expr = lens teExpr (\res expr -> res { teExpr = expr })++_ty :: Lens' (TypedExpr name) (Ty name)+_ty = lens teTy (\res ty -> res { teTy = ty })+ prettyPrint :: Pretty pretty => pretty -> Text prettyPrint expr = renderStrict docStream   where docStream = layoutPretty defaultLayoutOptions (pretty expr) +substituteTy+  :: Eq name+  => Ty name+  -> name+  -> Ty name+  -> Ty name+substituteTy ty forName inTy+  = case inTy of+      TyVar n+        | n == forName -> ty+        | otherwise -> inTy+      TyArrow t1 t2 -> TyArrow (sub t1) (sub t2)+      TyForAll n ty'+        | n == forName -> inTy+        | otherwise -> TyForAll n (sub ty')+  where sub = substituteTy ty forName+ upperLambda :: Char upperLambda = 'Λ' +prettyVarAnn :: Pretty name => name -> Ty name -> Doc a+prettyVarAnn var ty = pretty var <> colon <> prettyTy' ty+  where prettyTy' (TyVar _) = prettyTy True ty+        prettyTy' _ = parens $ prettyTy True ty+ prettyApp-  :: (Pretty name, Pretty ty)-  => SystemFExpr name ty-  -> SystemFExpr name ty+  :: Pretty name+  => SystemFExpr name+  -> SystemFExpr name   -> Doc a prettyApp e1@Abs{} e2@Abs{} = parens (pretty e1) <+> parens (pretty e2) prettyApp e1@Abs{} e2 = parens (pretty e1) <+> pretty e2@@ -58,10 +107,10 @@ prettyApp e1 e2 = pretty e1 <+> pretty e2  prettyAbs-  :: (Pretty name, Pretty ty)+  :: Pretty name   => name-  -> Ty ty-  -> SystemFExpr name ty+  -> Ty name+  -> SystemFExpr name   -> Doc ann prettyAbs name ty body   = lambda@@ -70,11 +119,14 @@     <+> pretty body'   where (names, body') = uncurryAbs name ty body -prettyTyAbs :: (Pretty name, Pretty ty) => ty -> SystemFExpr name ty -> Doc ann+prettyLet :: Pretty name => name -> SystemFExpr name -> Doc ann+prettyLet name expr = "let" <+> pretty name <+> equals <+> pretty expr++prettyTyAbs :: (Pretty name) => name -> SystemFExpr name -> Doc ann prettyTyAbs name body = upperLambda' <+> hsep (map pretty names) <> dot     <+> pretty body'   where (names, body') = uncurryTyAbs name body-prettyTyApp :: (Pretty name, Pretty ty) => SystemFExpr name ty -> Ty ty -> Doc ann+prettyTyApp :: (Pretty name) => SystemFExpr name -> Ty name -> Doc ann prettyTyApp expr ty = pretty expr <+> brackets (pretty ty)  prettyTy :: Pretty name => Bool -> Ty name -> Doc ann@@ -82,6 +134,13 @@ prettyTy compact (TyArrow t1 t2) = prettyTyArrow compact t1 t2 prettyTy compact (TyForAll name ty) = prettyTyForAll compact name ty +isTyEquivalent :: Eq name => Ty name -> Ty name -> Bool+isTyEquivalent t1 t2+  | t1 `isTySame` t2 = True+  | otherwise = case (t1, t2) of+      (TyForAll n1 t1', TyForAll n2 t2') -> (n1, t1') `areForAllsEquivalent` (n2, t2')+      _ -> False+ prettyTyArrow :: Pretty name => Bool -> Ty name -> Ty name -> Doc ann prettyTyArrow compact (TyArrow t1 t2) t3   = prettyTyArrow' compact compositeTy $ prettyTy compact t3@@ -107,18 +166,27 @@ upperLambda' :: Doc ann upperLambda' = pretty upperLambda +isTySame :: Eq name => Ty name -> Ty name -> Bool+isTySame (TyVar n1) (TyVar n2) = n1 == n2+isTySame (TyArrow t1 t2) (TyArrow t1' t2') = t1 == t1' && t2 == t2'+isTySame (TyForAll n1 t1) (TyForAll n2 t2) = n1 == n2 && t1 == t2+isTySame _ _ = False++areForAllsEquivalent :: Eq name => (name, Ty name) -> (name, Ty name) -> Bool+areForAllsEquivalent (n1, t1) (n2, t2) = t1 == substituteTy (TyVar n1) n2 t2+ prettyTyArrow' :: Bool -> Doc ann -> Doc ann -> Doc ann prettyTyArrow' compact doc1 doc2 = doc1 `add'` "->" `add'` doc2   where add'           | compact = (<>)            | otherwise = (<+>) -uncurryAbs :: n -> Ty t -> SystemFExpr n t -> ([(n, Ty t)], SystemFExpr n t)+uncurryAbs :: n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n) uncurryAbs name ty = uncurry' [(name, ty)]    where uncurry' ns (Abs n' t' body') = uncurry' ((n', t'):ns) body'         uncurry' ns body'             = (reverse ns, body') -uncurryTyAbs :: t -> SystemFExpr n t -> ([t], SystemFExpr n t)+uncurryTyAbs :: n -> SystemFExpr n -> ([n], SystemFExpr n) uncurryTyAbs ty = uncurry' [ty]   where uncurry' ts (TyAbs t' body') = uncurry' (t':ts) body'         uncurry' ts body'            = (reverse ts, body')

@@ -13,46 +13,61 @@  import Language.Lambda.SystemF.Expression -parseExpr :: Text -> Either ParseError (SystemFExpr Text Text)-parseExpr = parse (whitespace *> expr <* eof) ""+parseExpr :: Text -> Either ParseError (SystemFExpr Text)+parseExpr = parse (whitespace *> topLevelExpr <* eof) ""  parseType :: Text -> Either ParseError (Ty Text) parseType = parse (whitespace *> ty <* eof) "" +-- Lets can only be at the top level+topLevelExpr :: Parser (SystemFExpr Text)+topLevelExpr = let' <|> expr+ -- Parse expressions-expr :: Parser (SystemFExpr Text Text)+expr :: Parser (SystemFExpr Text) expr = try tyapp <|> try app <|> term -app :: Parser (SystemFExpr Text Text)+app :: Parser (SystemFExpr Text) app = chainl1 term (return App) -tyapp :: Parser (SystemFExpr Text Text)+tyapp :: Parser (SystemFExpr Text) tyapp = TyApp       <$> term       <*> ty'   where ty' = symbol '[' *> ty <* symbol ']' -term :: Parser (SystemFExpr Text Text)+term :: Parser (SystemFExpr Text) term = try abs <|> tyabs <|> var <|> parens expr -var :: Parser (SystemFExpr Text Text)-var = Var <$> exprId+let' :: Parser (SystemFExpr Text)+let' = Let <$> ident <*> expr+  where ident = symbol' "let" *> exprId <* symbol '=' -abs :: Parser (SystemFExpr Text Text)+var :: Parser (SystemFExpr Text)+var = try varann <|> var'+  where var' = Var <$> exprId+        varann = VarAnn <$> (exprId <* symbol ':') <*> ty++abs :: Parser (SystemFExpr Text) abs = curry'-    <$> (symbol '\\' *> many1 args <* symbol '.') +    <$> (symbol '\\' *> many1 args <* symbol '.')     <*> expr   where args = (,) <$> (exprId <* symbol ':') <*> ty         curry' = flip . foldr . uncurry $ Abs -tyabs :: Parser (SystemFExpr Text Text)+tyabs :: Parser (SystemFExpr Text) tyabs = curry' <$> args <*> expr   where args = symbol '\\' *> many1 typeId <* symbol '.'         curry' = flip (foldr TyAbs)  -- Parse type expressions ty :: Parser (Ty Text)-ty = try arrow+ty = try forall <|> try arrow++forall :: Parser (Ty Text)+forall = curry' <$> args <*> ty+  where args = symbol' "forall" *> many1 typeId <* symbol '.'+        curry' = flip $ foldr TyForAll  arrow :: Parser (Ty Text) arrow = chainr1 tyterm (symbol' "->" $> TyArrow)

@@ -2,23 +2,31 @@   ( TypecheckState(..),     Typecheck(),     Context(),+    Binding(..),+    Globals(),     runTypecheck,     execTypecheck,     unsafeRunTypecheck,     unsafeExecTypecheck,     mkTypecheckState,-    context,-    uniques,+    _context,+    _globals,+    _varUniques,+    _tyUniques,     getContext,-    getUniques,-    modifyContext,-    modifyUniques,-    setContext,-    setUniques+    getGlobals,+    getVarUniques,+    getTyUniques,+    modifyGlobals,+    modifyVarUniques,+    modifyTyUniques,+    setGlobals,+    setVarUniques,+    setTyUniques   ) where  import Language.Lambda.Shared.Errors (LambdaException(..))-import Language.Lambda.SystemF.Expression (Ty(..))+import Language.Lambda.SystemF.Expression  import Control.Monad.Except (Except(), runExcept) import RIO@@ -26,16 +34,24 @@ import qualified RIO.Map as Map  data TypecheckState name = TypecheckState-  { tsContext :: Context name,-    tsUniques :: [name]-  }+  { tsGlobals :: Globals name,+    tsVarUniques :: [name],  -- ^ A unique supply of term-level variables+    tsTyUniques :: [name]    -- ^ A unique supply of type-level variables+  } deriving (Eq, Show)  type Typecheck name   = StateT (TypecheckState name)       (Except LambdaException) -type Context name = Map name (Ty name)+type Globals name = Map name (TypedExpr name) +type Context name = Map name (Binding name)++data Binding name+  = BindTerm (Ty name)+  | BindTy+  deriving (Eq, Show)+ runTypecheck   :: Typecheck name result   -> TypecheckState name@@ -59,31 +75,52 @@ unsafeExecTypecheck computation state' = either impureThrow id tcResult   where tcResult = execTypecheck computation state' -mkTypecheckState :: [name] -> TypecheckState name+mkTypecheckState :: [name] -> [name] -> TypecheckState name mkTypecheckState = TypecheckState Map.empty -uniques :: Lens' (TypecheckState name) [name]-uniques f state' = (\uniques' -> state' { tsUniques = uniques' })-  <$> f (tsUniques state')+_context :: SimpleGetter (TypecheckState name) (Context name)+_context = to (getContext' . tsGlobals)+  where getContext' :: Globals name -> Context name+        getContext' = Map.map (\expr -> BindTerm (expr ^. _ty))+        +_globals :: Lens' (TypecheckState name) (Globals name)+_globals f state' = (\globals' -> state' { tsGlobals = globals' })+  <$> f (tsGlobals state') -context :: Lens' (TypecheckState name) (Context name)-context f state' = (\context' -> state' { tsContext = context' })-  <$> f (tsContext state')+_varUniques :: Lens' (TypecheckState name) [name]+_varUniques f state' = (\uniques' -> state' { tsVarUniques = uniques' })+  <$> f (tsVarUniques state') -getUniques :: Typecheck name [name]-getUniques = gets (^. uniques)+_tyUniques :: Lens' (TypecheckState name) [name]+_tyUniques f state' = (\uniques' -> state' { tsTyUniques = uniques' })+  <$> f (tsTyUniques state') +getVarUniques :: Typecheck name [name]+getVarUniques = gets (^. _varUniques)++getTyUniques :: Typecheck name [name]+getTyUniques = gets (^. _tyUniques)+ getContext :: Typecheck name (Context name)-getContext = gets (^. context)+getContext = gets (^. _context) -modifyContext :: (Context name -> Context name) -> Typecheck name ()-modifyContext f = modify $ context %~ f+getGlobals :: Typecheck name (Globals name)+getGlobals = gets (^. _globals) -modifyUniques :: ([name] -> [name]) -> Typecheck name ()-modifyUniques f = modify $ uniques %~ f+modifyGlobals :: (Globals name -> Globals name) -> Typecheck name ()+modifyGlobals f = modify $ _globals %~ f -setUniques :: [name] -> Typecheck name ()-setUniques uniques' = modify (& uniques .~ uniques')+modifyVarUniques :: ([name] -> [name]) -> Typecheck name ()+modifyVarUniques f = modify $ _varUniques %~ f -setContext :: Context name -> Typecheck name ()-setContext context' = modify (& context .~ context')+modifyTyUniques :: ([name] -> [name]) -> Typecheck name ()+modifyTyUniques f = modify $ _tyUniques %~ f++setVarUniques :: [name] -> Typecheck name ()+setVarUniques uniques' = modify $ _varUniques .~ uniques'++setTyUniques :: [name] -> Typecheck name ()+setTyUniques uniques' = modify $ _tyUniques .~ uniques'++setGlobals :: Globals name -> Typecheck name ()+setGlobals globals' = modify $ _globals .~ globals'

@@ -7,116 +7,183 @@ import Control.Monad.Except (MonadError(..)) import Prettyprinter import RIO-import qualified RIO.List as List import qualified RIO.Map as Map  type UniqueSupply n = [n] type Context' n t = Map n t --- TODO: name/ty different types typecheck   :: (Ord name, Pretty name)-  => SystemFExpr name name+  => SystemFExpr name   -> Typecheck name (Ty name)-typecheck (Var v) = typecheckVar v-typecheck (Abs n t body) = typecheckAbs n t body-typecheck (App e1 e2) = typecheckApp e1 e2-typecheck (TyAbs t body) = typecheckTyAbs t body-typecheck (TyApp e ty) = typecheckTyApp e ty+typecheck expr = do+  ctx <- getContext+  typecheckTopLevel ctx expr -typecheckVar :: Ord name => name -> Typecheck name (Ty name)-typecheckVar var = getContext >>= defaultToFreshTyVar . Map.lookup var-  where defaultToFreshTyVar (Just v) = return v-        defaultToFreshTyVar Nothing = TyVar <$> unique+typecheckTopLevel+  :: (Ord name, Pretty name)+  => Context name+  -> SystemFExpr name+  -> Typecheck name (Ty name)+typecheckTopLevel ctx (Let n expr) = typecheckLet ctx n expr+typecheckTopLevel ctx expr = typecheckExpr ctx expr +typecheckLet+  :: (Pretty name, Ord name)+  => Context name+  -> name+  -> SystemFExpr name+  -> Typecheck name (Ty name)+typecheckLet ctx _ = typecheckExpr ctx+  +typecheckExpr+  :: (Ord name, Pretty name)+  => Context name+  -> SystemFExpr name+  -> Typecheck name (Ty name)+typecheckExpr ctx (Var v) = typecheckVar ctx v+typecheckExpr ctx (VarAnn v ty) = typecheckVarAnn ctx v ty+typecheckExpr ctx (Abs n t body) = typecheckAbs ctx n t body+typecheckExpr ctx (App e1 e2) = typecheckApp ctx e1 e2+typecheckExpr ctx (TyAbs t body) = typecheckTyAbs ctx t body+typecheckExpr ctx (TyApp e ty) = typecheckTyApp ctx e ty+typecheckExpr _ (Let _ _) = throwError ImpossibleError++typecheckVar :: Ord name => Context name -> name -> Typecheck name (Ty name)+typecheckVar ctx = defaultToUnique . typecheckVar' ctx+  where defaultToUnique = maybe (TyVar <$> tyUnique) pure+    +typecheckVarAnn+  :: (Ord name, Pretty name)+  => Context name+  -> name+  -> Ty  name+  -> Typecheck name (Ty name)+typecheckVarAnn ctx var ty = maybe (pure ty) checkContextType maybeTy+  where checkContextType ty'+          | ty' == ty = pure ty+          | otherwise = throwError $ tyMismatchError ty' ty+        maybeTy = typecheckVar' ctx var+ typecheckAbs   :: (Ord name, Pretty name)-  => name+  => Context name+  -> name   -> Ty name-  -> SystemFExpr name name+  -> SystemFExpr name   -> Typecheck name (Ty name)-typecheckAbs name ty body-  = modifyContext (Map.insert name ty)-    >> TyArrow ty <$> typecheck body+typecheckAbs ctx name ty body = typecheckAbs' ty' (Map.insert name (BindTerm ty') ctx)+  where typecheckAbs' (TyForAll tyName tyBody) ctx' = do+          inner <- typecheckExpr (Map.insert tyName BindTy ctx') body+          pure $ TyForAll tyName (TyArrow tyBody inner)+        typecheckAbs' t ctx' = TyArrow t <$> typecheckExpr ctx' body +        ty' = liftForAlls ty+       typecheckApp   :: (Ord name, Pretty name)-  => SystemFExpr name name-  -> SystemFExpr name name+  => Context name+  -> SystemFExpr name+  -> SystemFExpr name   -> Typecheck name (Ty name)-typecheckApp e1 e2 = do+typecheckApp ctx e1 e2 = do   -- Typecheck expressions-  t1 <- typecheck e1-  t2 <- typecheck e2+  t1 <- typecheckExpr ctx e1+  t2 <- typecheckExpr ctx e2 -  -- Verify the type of t1 is an Arrow   (t1AppInput, t1AppOutput) <- case t1 of-    (TyArrow appInput appOutput) -> return (appInput, appOutput)-    t1' -> throwError $ tyMismatchError t1' t1+    (TyArrow appInput appOutput) -> pure (appInput, appOutput)+    (TyForAll n1 (TyArrow appInput _))+      -> pure (TyForAll n1 appInput, t2)+    _ -> throwError $ TyMismatchError "Not Arrow"    -- Verify the output of e1 matches the type of e2-  if t1AppInput == t2+  if t1AppInput `isTyEquivalent` t2     then return t1AppOutput     else throwError $ tyMismatchError (TyArrow t2 t1AppOutput) (TyArrow t1 t1AppOutput)  typecheckTyAbs   :: (Ord name, Pretty name)-  => name-  -> SystemFExpr name name+  => Context name+  -> name+  -> SystemFExpr name   -> Typecheck name (Ty name)-typecheckTyAbs ty body-  = modifyContext (Map.insert ty (TyVar ty))-    >> TyForAll ty <$> typecheck body+typecheckTyAbs ctx ty body = TyForAll ty <$> typecheckExpr ctx' body+  where ctx' = Map.insert ty BindTy ctx  typecheckTyApp   :: (Ord name, Pretty name)-  => SystemFExpr name name+  => Context name+  -> SystemFExpr name   -> Ty name   -> Typecheck name (Ty name)-typecheckTyApp (TyAbs t expr) ty = typecheck $ substitute ty t expr-typecheckTyApp expr _ = typecheck expr+typecheckTyApp ctx expr ty = do+  -- Clear in-scope type variables+  let ctx' = Map.filter isTyBind ctx+  +  typecheckExpr ctx' expr >>= \case+    TyForAll tyName tyBody -> pure $ substituteTy ty tyName tyBody+    _ -> do+      err <- tyAppMismatchError ctx expr ty+      throwError err -unique :: Typecheck name name-unique = getUniques >>= fromJust' . List.headMaybe-  where fromJust' (Just u) = return u-        fromJust' Nothing = throwError ImpossibleError+  where+    isTyBind BindTy = False+    isTyBind _ = True -substitute-  :: Eq n-  => Ty n-  -> n-  -> SystemFExpr n n-  -> SystemFExpr n n-substitute ty name (App e1 e2) = App (substitute ty name e1) (substitute ty name e2)-substitute ty name (Abs n ty' e) = Abs n (substituteTy ty name ty') (substitute ty name e)-substitute ty name (TyAbs ty' e) = TyAbs ty' (substitute ty name e) -substitute ty name (TyApp e ty') = TyApp (substitute ty name e) (substituteTy ty name ty')-substitute _ _ expr = expr+typecheckVar' :: Ord name => Context name -> name -> Maybe (Ty name)+typecheckVar' ctx var = Map.lookup var ctx >>= \case+  BindTerm ty@(TyForAll tyName tyBody)+    | Map.member tyName ctx -> Just tyBody+    | otherwise -> Just ty+  BindTerm ty -> Just ty+  BindTy -> Nothing -substituteTy-  :: Eq name-  => Ty name-  -> name-  -> Ty name-  -> Ty name-substituteTy ty name (TyArrow t1 t2) -  = TyArrow (substituteTy ty name t1) (substituteTy ty name t2)-substituteTy ty name ty'@(TyVar name') -  | name == name' = ty-  | otherwise     = ty'-substituteTy _ name t2@(TyForAll name' t2') -  | name == name' = t2-  | otherwise     = TyForAll name' (substituteTy t2 name t2')+liftForAlls :: Ty name -> Ty name+liftForAlls ty = foldr TyForAll res tyNames+  where (tyNames, res) = liftForAlls' ty +liftForAlls' :: Ty name -> ([name], Ty name)+liftForAlls' (TyVar name) = ([], TyVar name)+liftForAlls' (TyForAll name body) = (name:names, body')+  where (names, body') = liftForAlls' body+liftForAlls' (TyArrow t1 t2) = (n1 ++ n2, TyArrow t1' t2')+  where (n1, t1') = liftForAlls' t1+        (n2, t2') = liftForAlls' t2 +isTyEquivalent :: Ord name => Ty name -> Ty name -> Bool+isTyEquivalent t1 t2+  | t1 == t2 = True+  | otherwise = case (t1, t2) of+      (TyForAll n1 t1', TyForAll n2 t2') -> (n1, t1') `areForAllsEquivalent` (n2, t2')+      _ -> False++areForAllsEquivalent :: Ord name => (name, Ty name) -> (name, Ty name) -> Bool+areForAllsEquivalent (n1, t1) (n2, t2) = t1 == substituteTy (TyVar n1) n2 t2++tyUnique :: Typecheck name name+tyUnique = getTyUniques >>= tyUnique'+    where tyUnique' (u:us) = setTyUniques us $> u+          tyUnique' _ = throwError ImpossibleError+ tyMismatchError-  :: (Pretty t1, Pretty t2)-  => t1-  -> t2-  -> LambdaException+  :: Pretty ty => ty -> ty -> LambdaException tyMismatchError expected actual   = TyMismatchError   $ "Couldn't match expected type "   <> prettyPrint expected   <> " with actual type "   <> prettyPrint actual++tyAppMismatchError+  :: (Ord name, Pretty name)+  => Context name+  -> SystemFExpr name+  -> Ty name+  -> Typecheck name LambdaException+tyAppMismatchError ctx expr appTy = tyAppMismatchError' <$> typecheckExpr ctx expr+  where tyAppMismatchError' actual = TyMismatchError+          $ "Cannot apply type "+          <> prettyPrint appTy+          <> " to non-polymorphic type "+          <> prettyPrint actual

@@ -1,4 +1,3 @@-{-# LANGUAGE FlexibleInstances #-} module Language.Lambda.Untyped (   evalText,   runEvalText,@@ -25,9 +24,8 @@ import Language.Lambda.Untyped.State  evalText :: Text -> Eval Text (LambdaExpr Text)-evalText = either throwParseError evalExpr' . parseExpr+evalText = either throwParseError evalExpr . parseExpr   where throwParseError = throwError . ParseError . Text.pack . show-        evalExpr' = evalExpr  runEvalText   :: Text

@@ -0,0 +1,247 @@+module Language.Lambda.SystemF.EvalSpec (spec) where++import RIO+import RIO.Map (fromList)+import Test.Hspec++import Language.Lambda.Shared.Errors+import Language.Lambda.Shared.UniqueSupply (defaultUniques, defaultTyUniques)+import Language.Lambda.SystemF.Expression+import Language.Lambda.SystemF.Eval+import Language.Lambda.SystemF.HspecUtils+import Language.Lambda.SystemF.State++spec :: Spec+spec = do+  let evalExpr' expr = execTypecheck (evalExpr expr) $+          mkTypecheckState defaultUniques defaultTyUniques+  +  describe "evalExpr" $ do+    it "Does not reduce normal form" $ do+      "x" `shouldEvalTo` "x"++    it "beta reduces" $ do+      "(\\x:T. x) y:T" `shouldEvalTo` "y:T"+      "(\\f:(T->T) x:T. f x) (g:T->T) (y:T)" `shouldEvalTo` "g:(T->T) y:T"+      "\\x:T. (\\y:T. y) x" `shouldEvalTo` "\\x:T. x"+      "(\\f:(T->T) x:T. f x) (\\f:T. x:T)" `shouldEvalTo` "\\z:T. x:T"++    it "reduces let bodies" $ do+      "let x = (\\y:Y. y) z:Y" `shouldEvalTo` "let x = z:Y"++    it "nested let expressions fail" $ do+      eval "let x = let y = z" `shouldFailWith` isLambdaException++    it "reduces type abstractions to A normal form" $ do+      "\\T. (\\y:T. y) x:T" `shouldEvalTo` "\\T. x:T"++    it "reduces type applications" $ do+      "(\\T. x:T) [X]" `shouldEvalTo` "x:X"+      "(\\x:(forall T. T). x) [X]" `shouldEvalTo` "\\x:X. x"+      "x:(forall T. T) [X]" `shouldEvalTo` "x:X"+      "(\\x:(forall T. T). x) (\\X. y:X)" `shouldEvalTo` "\\X. y:X"++  describe "subGlobals" $ do+    let subGlobals' :: SystemFExpr Text -> SystemFExpr Text+        subGlobals' expr = unsafeExecTypecheck (subGlobals expr) state+        state = TypecheckState globals' defaultUniques defaultTyUniques+        globals' = fromList [("w", TypedExpr (Var "x") (TyVar "X"))]+    +    it "subs simple variables" $ do+      subGlobals' (Var "w")  `shouldBe` Var "x"+      subGlobals' (VarAnn "w" (TyVar "X"))  `shouldBe` Var "x"+      +    it "does not sub shadowed bindings" $ do+      let expr = Abs "w" (TyVar "W") $ Var "w"+      subGlobals' expr `shouldBe` expr+      +    xit "does not capture globals" $ do+      let expr = Abs "x" (TyVar "X") $ Var "w"+      subGlobals' expr `shouldBe` Abs "a" (TyVar "X") (Var "x")++  describe "betaReduce" $ do+    let betaReduce' :: SystemFExpr Text -> SystemFExpr Text -> SystemFExpr Text+        betaReduce' e1 e2 = unsafeExecTypecheck (betaReduce e1 e2) $+          mkTypecheckState defaultUniques defaultTyUniques+    +    it "reduces simple applications" $ do+      let e1 = Abs "x" (TyVar "T") (Var "x")+          e2 = Var "y"++      betaReduce' e1 e2 `shouldBe` e2++    it "reduces nested abstractions" $ do+      let e1 = Abs "x" (TyVar "T") (Abs "y" (TyVar "U") (Var "x"))+          e2 = Var "z"+      betaReduce' e1 e2 `shouldBe` Abs "y" (TyVar "U") (Var "z")++    it "reduces inner applications" $ do+      let e1 = Abs "f" (TyArrow (TyVar "T") (TyVar "T")) $+            App (Var "f") (VarAnn "x" (TyVar "T"))+          e2 = Var "g"+      betaReduce' e1 e2 `shouldBe` App (Var "g") (VarAnn "x" (TyVar "T"))++    it "does not reduce unreducible expressions" $ do+      let e2 = Var "y"++      betaReduce' (Var "x") e2+        `shouldBe` App (Var "x") (Var "y")+      betaReduce' (VarAnn "x" (TyVar "T")) e2+        `shouldBe` App (VarAnn "x" (TyVar "T")) (Var "y")+      betaReduce' (TyAbs "X" (Var "x")) e2+        `shouldBe` App (TyAbs "X" (Var "x")) e2+      betaReduce' (TyApp (Var "x") (TyVar "X")) e2+        `shouldBe` App (TyApp (Var "x") (TyVar "X")) e2++    it "does not reduce irreducible chained applications" $ do+      let e1 = App (Var "x") (Var "y")+          e2 = Var "z"+      betaReduce' e1 e2 `shouldBe` App (App (Var "x") (Var "y")) (Var "z")++    it "does not sub shadowed bindings" $ do+      let e1 = Abs "x" (TyVar "T") (Abs "x" (TyVar "U") (Var "x"))+          e2 = Var "z"+      betaReduce' e1 e2 `shouldBe` Abs "x" (TyVar "U") (Var "x")++    it "fails to reduce Let" $ do+      let e1 = Let "x" (Var "x")+          e2 = Var "z"+      evaluate (betaReduce' e1 e2) `shouldThrow` isImpossibleError++    it "avoids capture" $ do+      let beta :: SystemFExpr Text -> SystemFExpr Text -> SystemFExpr Text+          beta e1 e2 = unsafeExecTypecheck (betaReduce e1 e2) $+            mkTypecheckState ["z"] defaultTyUniques+      +      let e1 = Abs "f" (TyArrow (TyVar "T") (TyVar "U")) $+            Abs "x" (TyVar "U") $+              App (Var "f") (Var "x")+          e2 = Abs "f" (TyVar "T") $ Var "x"+      beta e1 e2 `shouldBe` Abs "z" (TyVar "U") (Var "x")++  describe "evalTyApp" $ do+    it "reduces simple type applications" $ do+      let expr = TyApp+            (TyAbs "T" (VarAnn "x" (TyVar "T")))+            (TyVar "X")++      evalExpr' expr `shouldBeRight` VarAnn "x" (TyVar "X")++    it "reduces type applications with abstractions" $ do+      let expr = TyApp+            (TyAbs "T" (Abs "x" (TyVar "T") (Var "x")))+            (TyVar "X")++      evalExpr' expr `shouldBeRight` Abs "x" (TyVar "X") (Var "x")++    it "does not reduce irreducible expressions" $ do+      let tyApp inner = TyApp (TyAbs "T" inner) (TyVar "X")++      evalExpr' (tyApp (Var "x")) `shouldBeRight` Var "x"+      evalExpr' (tyApp (VarAnn "x" (TyVar "Z"))) `shouldBeRight` VarAnn "x" (TyVar "Z")+      evalExpr' (tyApp (Abs "x" (TyVar "Z") (Var "x")))+        `shouldBeRight` Abs "x" (TyVar "Z") (Var "x")++    it "fails on let" $ do+      let expr = TyApp (Let "x" (VarAnn "y" (TyVar "T"))) (TyVar "X")+      evalExpr' expr `shouldSatisfy` either isLetError (const False)++    it "reduces nested expressions" $ do+      let tyApp inner = TyApp (TyAbs "T" inner) (TyVar "X")+      +      let e1 = App (Var "f") (VarAnn "x" (TyVar "T"))+      evalExpr' (tyApp e1) `shouldBeRight` App (Var "f") (VarAnn "x" $ TyVar "X")++      let e2 = Abs "x" (TyVar "U") (VarAnn "t" $ TyVar "T")+      evalExpr' (tyApp e2) `shouldBeRight` Abs "x" (TyVar "U") (VarAnn "t" $ TyVar "X")++      let e3 = TyAbs "U" $ VarAnn "x" (TyVar "T")+      evalExpr' (tyApp e3) `shouldBeRight` TyAbs "U" (VarAnn "x" $ TyVar "X")++      let e4 = TyApp (VarAnn "x" (TyVar "T")) (TyVar "U")+      evalExpr' (tyApp e4) `shouldBeRight` TyApp (VarAnn "x" $ TyVar "X") (TyVar "U")++      let e5 = TyApp+            (TyAbs "U" $ VarAnn "x" (TyVar "U"))+            (TyVar "T")+      evalExpr' (tyApp e5) `shouldBeRight` VarAnn "x" (TyVar "X")++    it "reduces in nested types" $ do+      let tyApp inner = TyApp (TyAbs "T" inner) (TyVar "X")++      let e1 = VarAnn "f" $ TyArrow (TyVar "T") (TyVar "U")+      evalExpr' (tyApp e1) `shouldBeRight` VarAnn "f" (TyArrow (TyVar "X") (TyVar "U"))++      let e2 = VarAnn "f" $ TyForAll "T" (TyVar "T")+      evalExpr' (tyApp e2) `shouldBeRight` e2++      let e3 = VarAnn "f" $ TyForAll "U" (TyVar "T")+      evalExpr' (tyApp e3) `shouldBeRight` VarAnn "f" (TyForAll "U" (TyVar "X"))+                ++  describe "alphaConvert" $ do+    let alphaConvert' :: [Text] -> [Text] -> SystemFExpr Text -> SystemFExpr Text+        alphaConvert' uniques' fvs expr = unsafeExecTypecheck (alphaConvert fvs expr) $+          mkTypecheckState uniques' defaultTyUniques+    +    it "alpha converts simple expressions" $ do+      let freeVars = ["x"] :: [Text]+          expr = Abs "x" (TyVar "T") (Var "x")+          uniques' = ["y"]+      alphaConvert' uniques' freeVars expr `shouldBe` Abs "y" (TyVar "T") (Var "y")++    it "avoids captures" $ do+      let freeVars = ["x"]+          expr = Abs "x" (TyVar "T") (Var "x")+          uniques' = ["x", "y"]+      alphaConvert' uniques' freeVars expr `shouldBe` Abs "y" (TyVar "T") (Var "y")++  describe "etaConvert" $ do+    it "eta converts simple expressions" $ do+      let expr :: SystemFExpr Text+          expr = Abs "x" (TyVar "T") $ App (Var "f") (Var "x")+      etaConvert expr `shouldBe` Var "f"+      +    it "eta converts nested applications" $ do+      let expr1 :: SystemFExpr Text+          expr1 = Abs "y" (TyVar "T")  $ App (App (Var "f") (Var "x")) (Var "y")+      etaConvert expr1 `shouldBe` App (Var "f") (Var "x")++      let expr2 :: SystemFExpr Text+          expr2 = Abs "x" (TyArrow (TyVar "T") (TyVar "T")) $+            Abs "y" (TyVar "T") $+              App (App (Var "f") (Var "x")) (Var "y")+      etaConvert expr2 `shouldBe` Var "f" ++      let expr3 :: SystemFExpr Text+          expr3 = Abs "x" (TyVar "T") $+            Abs "y" (TyArrow (TyVar "T") (TyVar "T")) $+              App (Var "y") (Var "x")+      etaConvert expr3 `shouldBe` expr3++      let expr4 :: SystemFExpr Text+          expr4 = Abs "f" (TyVar "T") $+            Abs "x" (TyVar "T") (Var "x")+      etaConvert expr4 `shouldBe` expr4+      +    it "ignores non-eta convertable expressions" $ do+      let expr :: SystemFExpr Text+          expr = Abs "x" (TyVar "T") $ Var "x"+      etaConvert expr `shouldBe` expr++  describe "freeVarsOf" $ do+    let freeVarsOf' :: SystemFExpr Text -> [Text]+        freeVarsOf' = freeVarsOf+    +    it "Returns simple vars" $ do+      freeVarsOf' (Var "x") `shouldBe` ["x"]+      freeVarsOf' (VarAnn "x" (TyVar "T")) `shouldBe` ["x"]+      +    it "Does not return bound vars" $ +      freeVarsOf' (Abs "x" (TyVar "T") (Var "x")) `shouldBe` []+      +    it "Returns nested simple vars" $+      freeVarsOf' (Abs "x" (TyVar "T") (Var "y")) `shouldBe` ["y"]+                                                             +    it "Returns applied simple vars" $+      freeVarsOf' (App (Var "x") (Var "y")) `shouldBe` ["x", "y"]

@@ -0,0 +1,30 @@+module Language.Lambda.SystemF.Examples.BoolSpec where++import RIO+import Test.Hspec++import Language.Lambda.SystemF.HspecUtils++spec :: Spec+spec = describe "Bool" $ do+  -- Bool is the definition of Booleans. We represent bools+  -- using Church Encodings:+  --+  -- true:  \T. \t:T f:T. t+  -- false: \T. \t:T f:T. f+  -- false: \T. \t:T f:T. f+  describe "not" $ do+    -- not takes a Bool and returns its opposite value+    --+    -- not(true)  = false+    -- not(false) = true+    --+    -- not is defined by+    -- not = \x. x (\t f. f) (\t f. t)+    it "not true = false" $+      "(\\x:(forall T. T -> T -> T). \\X. \\t:X f:X. (x [X]) f t) (\\U. \\t:U f:U. t)"+        `shouldEvalTo` "\\X. \\t:X f:X. f"++    it "not false = true" $+      "(\\x:(forall T. T-> T -> T). \\X. \\t:X f:X. (x [X]) f t) (\\U. \\t:U f:U. f)"+        `shouldEvalTo` "\\X. \\t:X f:X. t"

@@ -0,0 +1,75 @@+module Language.Lambda.SystemF.Examples.NatSpec where++import RIO+import Test.Hspec++import Language.Lambda.SystemF (evalText)+import Language.Lambda.SystemF.HspecUtils++spec :: Spec+spec = describe "Nat" $ do+  -- Nat is the definition of natural numbers. More precisely, Nat+  -- is the set of nonnegative integers.  We represent nats using+  -- Church Encodings:+  --+  -- 0: \f:(T->T) x:T. x+  -- 1: \f:(T->T) x:T. f x+  -- 2: \f:(T->T) x:T. f (f x)+  -- ...and so on++  describe "successor" $ do+    -- successor is a function that adds 1+    -- succ(0) = 1+    -- succ(1) = 2+    -- ... and so forth+    --+    -- successor is defined by+    -- succ = \n:((T->T)->T->T) f:(T->T) x:T. f (n f x)+    it "succ 0 = 1" $ do+      "(\\n:((T->T)->T->T) f:(T->T) x:T. f (n f x)) (\\f:(T->T) x:T. x)"+        `shouldEvalTo` "\\f:(T->T) x:T. f x"++    it "succ 1 = 2" $+      "(\\n:((T->T)->T->T) f:(T->T) x:T. f (n f x)) (\\f:(T->T) x:T. f x)"+        `shouldEvalTo` "\\f:(T->T) x:T. f (f x)"++  describe "add" $ do+    -- add(m, n) = m + n+    --+    -- It is defined by applying successor m times on n:+    -- add = \m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)+    it "add 0 2 = 2" $+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)) (\\f:(T->T) x:T. x) (\\f:(T->T) x:T. f (f x))"+        `shouldEvalTo` "\\f:(T->T) x:T. f (f x)"++    it "add 3 2 = 5" $+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)) (\\f:(T->T) x:T. f (f (f x))) (\\f:(T->T) x:T. f (f x))"+        `shouldEvalTo` "\\f:(T->T) x:T. f (f (f (f (f x))))"++    it "add 0 n = n" $+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T) x:T. m f (n f x)) (\\f:(T->T) x:T. x) n:((T->T)->T->T)"+        `shouldEvalTo` "\\f:(T->T) x:T. n:((T->T)->T->T) f x"++  describe "multiply" $ do+    -- multiply(m, n) = m * n+    --+    -- multiply is defined by applying add m times+    -- multiply = \m n f x. m (n f x) x)+    --+    -- Using eta conversion, we can omit the parameter x+    -- multiply = \m n f. m (n f)+    it "multiply 0 2 = 0" $+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. x) (\\f:(T->T) x:T. f (f x))"+        `shouldEvalTo` "\\f:(T->T) x:T. x"++    it "multiply 2 3 = 6" $+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. f (f x)) (\\f:(T->T) x:T. f (f (f x)))"+        `shouldEvalTo` "\\f:(T->T) x:T. f (f (f (f (f (f x)))))"++    it "multiply 0 n = 0" $+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. x) n:((T->T)->T->T)"+        `shouldEvalTo` "\\f:(T->T) x:T. x"++    it "multiply 1 n = n" $+      "(\\m:((T->T)->T->T) n:((T->T)->T->T) f:(T->T). m (n f)) (\\f:(T->T) x:T. f x) n:((T->T)->T->T)"+        `shouldEvalTo` "\\f:(T->T) x:T. n:((T->T)->T->T) f x"

@@ -1,4 +1,3 @@-{-# LANGUAGE OverloadedStrings, NoImplicitPrelude #-} module Language.Lambda.SystemF.ExpressionSpec where  import RIO@@ -7,81 +6,125 @@ import Language.Lambda.SystemF.Expression  spec :: Spec-spec = describe "prettyPrint" $ do-  let prettyPrint' :: SystemFExpr Text Text -> Text-      prettyPrint' = prettyPrint+spec = do+  describe "prettyPrint" $ do+    let prettyPrint' :: SystemFExpr Text -> Text+        prettyPrint' = prettyPrint -      prettyPrintTy :: Ty Text -> Text-      prettyPrintTy = prettyPrint+        prettyPrintTy :: Ty Text -> Text+        prettyPrintTy = prettyPrint   -  it "prints simple variables" $-    prettyPrint' (Var "x") `shouldBe` "x"+    it "prints simple variables" $+      prettyPrint' (Var "x") `shouldBe` "x" -  it "prints simple applications" $-    prettyPrint' (App (Var "a") (Var "b")) `shouldBe` "a b"+    it "prints annotated variables" $+      prettyPrint' (VarAnn "x" (TyVar "T")) `shouldBe` "x:T" -  it "prints simple abstractions" $ -    prettyPrint' (Abs "x" (TyVar "T") (Var "x")) `shouldBe` "λ x:T. x"+    it "prints simple applications" $+      prettyPrint' (App (Var "a") (Var "b")) `shouldBe` "a b" -  it "prints simple type abstractions" $-    prettyPrint' (TyAbs "X" (Var "x")) `shouldBe` "Λ X. x"+    it "prints simple abstractions" $ +      prettyPrint' (Abs "x" (TyVar "T") (Var "x")) `shouldBe` "λ x:T. x" -  it "prints simple type applications" $ -    prettyPrint' (TyApp (Var "t") (TyVar "T")) `shouldBe` "t [T]"+    it "prints simple type abstractions" $+      prettyPrint' (TyAbs "X" (Var "x")) `shouldBe` "Λ X. x" -  it "prints nested abstractions" $-    prettyPrint' (Abs "f" (TyVar "F") (Abs "x" (TyVar "X") (Var "x")))-      `shouldBe` "λ f:F x:X. x"+    it "prints simple type applications" $ +      prettyPrint' (TyApp (Var "t") (TyVar "T")) `shouldBe` "t [T]" -  it "prints abstractions with composite types" $ do-    prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyVar "Y")) (Var "f"))-      `shouldBe ` "λ f:(X->Y). f"+    it "prints simple let expressions" $+      prettyPrint' (Let "x" (Var "y")) `shouldBe` "let x = y" -    prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z"))) (Var "f"))-      `shouldBe ` "λ f:(X->Y->Z). f"+    it "prints annotated variables with composite types" $+      prettyPrint' (VarAnn "x" (TyArrow (TyVar "T") (TyVar "V"))) `shouldBe` "x:(T->V)" -  it "prints nested type abstractions" $-    prettyPrint' (TyAbs "A" (TyAbs "B" (Var "x")))-      `shouldBe` "Λ A B. x"+    it "prints nested abstractions" $+      prettyPrint' (Abs "f" (TyVar "F") (Abs "x" (TyVar "X") (Var "x")))+        `shouldBe` "λ f:F x:X. x" -  it "prints nested applications" $-    prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))-      `shouldBe` "f x y"+    it "prints abstractions with composite types" $ do+      prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyVar "Y")) (Var "f"))+        `shouldBe ` "λ f:(X->Y). f" -  it "prints parenthesized applications" $ do-    prettyPrint' (App (Var "w") (App (Var "x") (Var "y")))-      `shouldBe` "w (x y)"+      prettyPrint' (Abs "f" (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z"))) (Var "f"))+        `shouldBe ` "λ f:(X->Y->Z). f" -    prettyPrint' (App (Abs "t" (TyVar "T") (Var "t")) (Var "x"))-      `shouldBe` "(λ t:T. t) x"+    it "prints nested type abstractions" $+      prettyPrint' (TyAbs "A" (TyAbs "B" (Var "x")))+        `shouldBe` "Λ A B. x" -    prettyPrint' (App (Abs "f" (TyVar "F") (Var "f")) (Abs "g" (TyVar "G") (Var "g")))-      `shouldBe` "(λ f:F. f) (λ g:G. g)"+    it "prints nested applications" $+      prettyPrint' (App (App (Var "f") (Var "x")) (Var "y"))+        `shouldBe` "f x y" -  it "prints simple types" $-    prettyPrintTy (TyVar "X") `shouldBe` "X"+    it "prints parenthesized applications" $ do+      prettyPrint' (App (Var "w") (App (Var "x") (Var "y")))+        `shouldBe` "w (x y)" -  it "print simple arrow types" $-    prettyPrintTy (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"+      prettyPrint' (App (Abs "t" (TyVar "T") (Var "t")) (Var "x"))+        `shouldBe` "(λ t:T. t) x" -  it "prints simple forall types" $-    prettyPrintTy (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"+      prettyPrint' (App (Abs "f" (TyVar "F") (Var "f")) (Abs "g" (TyVar "G") (Var "g")))+        `shouldBe` "(λ f:F. f) (λ g:G. g)" -  it "prints chained arrow types" $-    prettyPrintTy (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))-      `shouldBe` "X -> Y -> Z"+    it "prints simple types" $+      prettyPrintTy (TyVar "X") `shouldBe` "X" -  it "prints nested arrow types" $-    prettyPrintTy (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))-      `shouldBe` "(T -> U) -> V"+    it "print simple arrow types" $+      prettyPrintTy (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B" -  it "prints complex forall types" $-    prettyPrintTy (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))-      `shouldBe` "forall A. A -> A"+    it "prints simple forall types" $+      prettyPrintTy (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X" -  it "prints nested forall types" $-    prettyPrintTy (TyForAll "W" -                  (TyForAll "X" -                    (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))-      `shouldBe` "forall W. forall X. W -> X -> Y"+    it "prints chained arrow types" $+      prettyPrintTy (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))+        `shouldBe` "X -> Y -> Z" +    it "prints nested arrow types" $+      prettyPrintTy (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))+        `shouldBe` "(T -> U) -> V"++    it "prints complex forall types" $+      prettyPrintTy (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))+        `shouldBe` "forall A. A -> A"++    it "prints nested forall types" $+      prettyPrintTy (TyForAll "W" +                     (TyForAll "X" +                      (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))+        `shouldBe` "forall W. forall X. W -> X -> Y"++  describe "(==)" $ do+    let tyvar = "X" :: Text+    +    it "same types return true" $ do+      TyVar tyvar `shouldBe` TyVar tyvar+      TyArrow (TyVar tyvar) (TyVar tyvar) `shouldBe` TyArrow (TyVar tyvar) (TyVar tyvar)+      TyForAll tyvar (TyVar tyvar) `shouldBe` TyForAll tyvar (TyVar tyvar)++    it "equivalent foralls return true" $+      TyForAll tyvar (TyVar tyvar) `shouldBe` TyForAll "Y" (TyVar "Y")++    it "unequal types return false" $ do+      TyVar tyvar `shouldNotBe` TyVar "Y"+      TyArrow (TyVar tyvar) (TyVar tyvar) `shouldNotBe` TyArrow (TyVar "Y") (TyVar "Y")+      TyForAll tyvar (TyVar tyvar) `shouldNotBe` TyForAll tyvar (TyVar "Y")+      TyVar tyvar `shouldNotBe` TyForAll tyvar (TyVar tyvar)++  describe "substituteTy" $ do+    let sub :: Ty Text -> Text -> Ty Text -> Ty Text+        sub = substituteTy+    +    it "substititues simple types" $ do+      sub (TyVar "X") "Y" (TyVar "Y") `shouldBe` TyVar "X"+      sub (TyVar "X") "Y" (TyVar "Z") `shouldBe` TyVar "Z"+      sub (TyArrow (TyVar "Z") (TyVar "X")) "Y" (TyVar "Y")+        `shouldBe` TyArrow (TyVar "Z") (TyVar "X")+      sub (TyForAll "X" (TyVar "Z")) "Y" (TyVar "Y")+        `shouldBe` TyForAll "X" (TyVar "Z")+      sub (TyVar "X") "Y" (TyForAll "Z" (TyVar "Y"))+        `shouldBe` TyForAll "Z" (TyVar "X")++    it "does not capture foralls" $ do+      sub (TyVar "X") "Y" (TyForAll "Y" (TyVar "Y"))+        `shouldBe` TyForAll "Y" (TyVar "Y")

@@ -0,0 +1,65 @@+module Language.Lambda.SystemF.HspecUtils where++import Language.Lambda.Shared.Errors+import Language.Lambda.SystemF++import RIO+import Test.Hspec+import qualified RIO.Map as Map++shouldEvalTo :: Text -> Text -> Expectation+shouldEvalTo input expected = eval input `shouldBe` eval expected++shouldTypecheckTo :: Text -> Text -> Expectation+shouldTypecheckTo = shouldTypecheckToWithGlobals []++shouldTypecheckToWithGlobals :: [(Text, TypedExpr Text)] -> Text -> Text -> Expectation+shouldTypecheckToWithGlobals globals expr ty = typecheck' globals expr `shouldHaveType` ty++shouldBeRight+  :: (Show l, Show r, Eq l, Eq r)+  => Either l r+  -> r+  -> Expectation+shouldBeRight res = (res `shouldBe`) . Right++shouldBeLeft+  :: (Show l, Show r, Eq l, Eq r)+  => Either l r+  -> l+  -> Expectation+shouldBeLeft res = (res `shouldBe`) . Left++shouldHaveType+  :: Either LambdaException (Ty Text)+  -> Text+  -> Expectation+shouldHaveType res tyRepr = case parseType tyRepr of+    Left err -> expectationFailure $+      "Could not parse type " <> show tyRepr <> ": " <> show err+    Right ty -> res `shouldBe` Right ty++shouldFailWith+  :: Show a+  => Either LambdaException a+  -> Selector LambdaException+  -> Expectation+shouldFailWith res selector = case res of+  Left err -> err `shouldSatisfy` selector+  Right res' -> expectationFailure $+        "did not get expected failure: " <> show res'++eval :: Text -> Either LambdaException (TypedExpr Text)+eval input = execTypecheck (evalText input) initialState+  where initialState = mkTypecheckState defaultUniques defaultTyUniques++typecheck' :: [(Text, TypedExpr Text)] -> Text -> Either LambdaException (Ty Text)+typecheck' globals input = execTypecheck (typecheckText input) initialState+  where initialState = TypecheckState (Map.fromList globals) defaultUniques defaultTyUniques++runTypecheck'+  :: [(Text, TypedExpr Text)]+  -> Text+  -> Either LambdaException (Ty Text, TypecheckState Text)+runTypecheck' globals input = runTypecheck (typecheckText input) initialState+  where initialState = TypecheckState (Map.fromList globals) defaultUniques defaultTyUniques

@@ -1,4 +1,3 @@-{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-} module Language.Lambda.SystemF.ParserSpec (spec) where  import Data.Either@@ -7,6 +6,7 @@ import Test.Hspec  import Language.Lambda.SystemF.Expression+import Language.Lambda.SystemF.HspecUtils import Language.Lambda.SystemF.Parser  spec :: Spec@@ -15,6 +15,9 @@     it "parses simple variables" $       parseExpr "x" `shouldBe` Right (Var "x") +    it "parses annotated variables" $+      parseExpr "x:T" `shouldBe` Right (VarAnn "x" (TyVar "T"))+     it "parses parenthesized variables" $       parseExpr "(x)" `shouldBe` Right (Var "x") @@ -27,6 +30,11 @@     it "parses simple type applications" $        parseExpr "x [T]" `shouldBe` Right (TyApp (Var "x") (TyVar "T")) +    it "parses simple lets" $ do+      parseExpr "let x = t" `shouldBeRight` Let "x" (Var "t")+      parseExpr "let f = \\x: T. x" `shouldBeRight`+        Let "f" (Abs "x" (TyVar "T") (Var "x"))+     it "parses nested abstractions" $       parseExpr "\\a:A b:B. b"          `shouldBe` Right (Abs "a" (TyVar "A") (Abs "b" (TyVar "B") (Var "b")))@@ -56,6 +64,9 @@     it "does not parse trailing errors" $       parseExpr "x +" `shouldSatisfy` isLeft +    it "does not parse misplaced lets" $+      parseExpr "\\x: T. let y = x" `shouldSatisfy` isLeft+     it "ignores whitespace" $ do       let exprs = [             " x ",@@ -84,3 +95,8 @@        parseType "(W -> V) -> U"         `shouldBe` Right (TyArrow (TyArrow (TyVar "W") (TyVar "V")) (TyVar "U"))++    it "parses forall types" $ do+      parseType "forall T. T" `shouldBeRight` TyForAll "T" (TyVar "T")+      parseType "forall T U. T->U"+        `shouldBeRight` TyForAll "T" (TyForAll "U" (TyArrow (TyVar "T") (TyVar "U")))

@@ -1,71 +1,92 @@ module Language.Lambda.SystemF.TypeCheckSpec (spec) where -import Data.Either-import Data.Map-import Prettyprinter-import Test.Hspec- import Language.Lambda.Shared.Errors import Language.Lambda.SystemF.Expression import Language.Lambda.SystemF.State-import Language.Lambda.SystemF.TypeCheck+import Language.Lambda.SystemF.HspecUtils -tc uniqs ctx expr = execTypecheck (typecheck expr) (TypecheckState (fromList ctx) uniqs)+import Control.Monad.Except+import Data.Map+import Lens.Micro+import RIO+import Test.Hspec  spec :: Spec spec = describe "typecheck" $ do-  it "typechecks simple variables in context" $-    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")+  let someGlobal = ("x", TypedExpr (Var "y") (TyVar "X"))+  +  it "typechecks simple variables" $ do+    typecheck' [someGlobal] "x" `shouldHaveType` "X"+    typecheck' [] "x" `shouldHaveType` "Z" -  it "typechecks simple variables not in context" $ -    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")+  it "typechecks annotated variables" $ do+    typecheck' [someGlobal] "x:X" `shouldHaveType` "X"+    typecheck' [someGlobal] "x:X" `shouldHaveType` "X" -  it "typechecks simple abstractions" $-    tc [] [] (Abs "x" (TyVar "A") (Var "x")) -      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))+    typecheck' [someGlobal] "x:Y" `shouldFailWith` isTyMismatchError -  it "typechecks simple applications" $ do-    let ctx = [-          ("f", TyArrow (TyVar "T") (TyVar "U")),-          ("a", TyVar "T")-          ]+  it "typechecks abstractions" $+    typecheck' [] "\\x:A. x" `shouldHaveType` "A -> A" -    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")+  it "typechecks applications" $ do+    let globals'+          = [ ("f", TypedExpr (Var "f") $ TyArrow (TyVar "T") (TyVar "U")),+              ("a", TypedExpr (Var "a") $ TyVar "T"),+              ("b", TypedExpr (Var "b") (TyVar "B"))+            ] -  it "apply variable to variable fails" $ do-    let ctx = [-          ("a", TyVar "A"),-          ("b", TyVar "B")-          ]+    typecheck' globals' "f a" `shouldHaveType` "U"+    typecheck' [] "(\\t: T. t) x:T" `shouldHaveType` "T" -    tc ["C"] ctx (App (Var "a") (Var "b")) -      `shouldSatisfy` isLeft+    -- Polymorphic application+    typecheck' [] "\\x:(forall T. T). x"+      `shouldHaveType` "forall T. T -> T"+    typecheck' [] "\\x:(forall T. T->U). x"+      `shouldHaveType` "forall T. (T -> U) -> (T -> U)"+    typecheck' [] "\\x:(U->(forall T. T)). x"+      `shouldHaveType` "forall T. (U -> T) -> (U -> T)"+    typecheck' [] "\\x:(forall T. T). x:T"+      `shouldHaveType` "forall T. T -> T"+    typecheck' [] "(\\z:(forall X. X). z) (\\X. a:X)"+      `shouldHaveType` "forall X. X"+    typecheck' [] "(\\x:(forall T. T). x) (\\X. y:X)"+      `shouldHaveType` "forall X. X" -  it "apply arrow to variable of wrong type fails" $ do-    let ctx = [-          ("f", TyArrow (TyVar "F") (TyVar "G")),-          ("b", TyVar "B")-          ]+    typecheck' globals' "a b" `shouldFailWith` isTyMismatchError+    typecheck' globals' "f b" `shouldFailWith` isTyMismatchError -    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft+  it "typechecks let expressions" $ do+    typecheck' [] "let x = y" `shouldHaveType` "Z"+    typecheck' [] "\\x:T. let y = z" `shouldFailWith` isLambdaException -  it "typechecks simple type abstractions" $-    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))+  it "typechecks type abstractions" $ do+    typecheck' [] "\\X. (\\x:X. x)" `shouldHaveType` "forall X. X->X"+    typecheck' [] "\\X. x" `shouldHaveType` "forall X. Z" -  it "typechecks type abstractions with simple abstraction" $-    tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) -      `shouldBe` Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))+  it "typechecks type applications" $ do+    let globals'+          = [ ("y", TypedExpr (Var "y") (TyVar "Y")),+              ("x", TypedExpr (Var "x") $ TyVar "A")] -  it "typechecks type abstractions with application" $-    tc [] [("y", TyVar "Y")] -      (App (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y")) -           (Var "y"))-      `shouldBe` Right (TyVar "Y")+    typecheck' globals' "((\\X.\\x:X.x) [Y]) y" `shouldHaveType` "Y"+    typecheck' globals' "(\\X. x) [T]" `shouldHaveType` "A"+    typecheck' globals' "(\\X. z: X) [T]" `shouldHaveType` "T"+    typecheck' globals' "(\\X. (\\x:X. x)) [Y]" `shouldHaveType` "Y -> Y"+    typecheck' globals' "(z:forall X. X) [Y]" `shouldHaveType` "Y"+    typecheck' globals' "\\x:(forall X. X). x [Y]" `shouldHaveType` "forall X. X -> Y"+    +  +    typecheck' [] "x:T [U]" `shouldFailWith` isTyMismatchError+    typecheck' globals' "x [U]" `shouldFailWith` isTyMismatchError -  it "typechecks simple type applications" $-    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))-      `shouldBe` Right (TyVar "A")+  it "doesn't modify context" $ do+    let exprs+          = [ "\\x:A. x",+              "\\X. x" ] -  it "typechecks type applications with simple abstraction" $-    tc [] [] (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))-      `shouldBe` Right (TyArrow (TyVar "Y") (TyVar "Y"))+    forM_ exprs $ \expr -> do+      let ctx = do+            (_, state) <- runTypecheck' [] expr+            pure $ state ^. _context+      +      ctx `shouldBeRight` empty

@@ -1,9 +1,116 @@ module Language.Lambda.SystemFSpec where -import Test.Hspec-+import Language.Lambda.Shared.Errors (LambdaException(..), isLambdaException) import Language.Lambda.SystemF+import Language.Lambda.SystemF.HspecUtils +import Lens.Micro+import RIO+import RIO.Map (empty, fromList)+import Test.Hspec+ spec :: Spec-spec = describe "evalString" $ -  return ()+spec = do+  describe "evalText" $ do+    let eval' :: Text -> Either LambdaException (SystemFExpr Text)+        eval' = over _Right (^. _expr) . eval++    it "evaluates simple text" $ do+      eval' "x" `shouldBeRight` Var "x"+      eval' "\\x:T. x" `shouldBeRight` Abs "x" (TyVar "T") (Var "x")+      eval' "\\X. x" `shouldBeRight` TyAbs "X" (Var "x")++    it "reduces simple applications" $+      eval' "(\\x:T. x) y:T" `shouldBeRight` VarAnn "y" (TyVar "T")++    it "reduces applications with nested redexes" $+      eval' "(\\f:T->T x:T. f x) (\\y:T. y)"+        `shouldBeRight` Abs "x" (TyVar "T") (Var "x")++    it "lets update state" $ do+      let act = evalText "let x = a: A" >> evalText "x"++      unsafeExecTypecheck act (mkTypecheckState [] [])+        `shouldBe` TypedExpr (VarAnn "a" (TyVar "A")) (TyVar "A")++  describe "runEvalText" $ do+    let runEvalText' input = extract $ runEvalText input empty+        extract = _Right %~ (^. _expr) . fst+    +    it "evaluates simple text" $ do+      runEvalText' "x" `shouldBeRight` Var "x"+      runEvalText' "\\x:T. x" `shouldBeRight` Abs "x" (TyVar "T") (Var "x")+      runEvalText' "\\X. x" `shouldBeRight` TyAbs "X" (Var "x")++  describe "execEvalText" $ do+    let execEvalText' input = extract $ execEvalText input empty+        extract = over _Right (^. _expr)+    +    it "evaluates simple text" $ do+      execEvalText' "x" `shouldBeRight` Var "x"+      execEvalText' "\\x:T. x" `shouldBeRight` Abs "x" (TyVar "T") (Var "x")+      execEvalText' "\\X. x" `shouldBeRight` TyAbs "X" (Var "x")++  describe "unsafeExecEvalText" $ do+    let unsafeExecEvalText' input = extract $ unsafeExecEvalText input empty+        extract = (^. _expr)++    it "evaluates simple text" $ do+      unsafeExecEvalText' "x" `shouldBe` Var "x"+      unsafeExecEvalText' "\\x:T. x" `shouldBe` Abs "x" (TyVar "T") (Var "x")+      unsafeExecEvalText' "\\X. x" `shouldBe` TyAbs "X" (Var "x")++    it "throws errors" $ do+      evaluate (unsafeExecEvalText' "\\x. x") `shouldThrow` isLambdaException++  describe "typecheckText" $ do+    let tc :: Text -> Either LambdaException (Ty Text)+        tc input = execTypecheck (typecheckText input) initialState++        initialState = mkTypecheckState defaultUniques defaultTyUniques++    it "typechecks simple text" $ do+      tc "x" `shouldHaveType` "Z"+      tc "\\x:T. x" `shouldHaveType` "T -> T"+      tc "\\X. x" `shouldHaveType` "forall X. Z"+      tc "(\\x:T. x) y:T" `shouldHaveType` "T"+      tc "(\\f:(T->T) x:T. f x) (\\y:T. y)" `shouldHaveType` "T -> T"++  describe "runTypecheckText" $ do+    let tc :: Text -> Either LambdaException (Ty Text)+        tc input = fst <$> runTypecheckText input globals'++        globals' = fromList [("x", TypedExpr (Var "x") (TyVar "A"))]++    it "typechecks simple text" $ do+      tc "x" `shouldHaveType` "A"+      tc "\\x:T. x" `shouldHaveType` "T -> T"+      tc "\\X. x" `shouldHaveType` "forall X. A"+      tc "(\\x:T. x) y:T" `shouldHaveType` "T"+      tc "(\\f:(T->T) x:T. f x) (\\y:T. y)" `shouldHaveType` "T -> T"++  describe "execTypecheckText" $ do+    let tc :: Text -> Either LambdaException (Ty Text)+        tc input = execTypecheckText input globals'++        globals' = fromList [("x", TypedExpr (Var "x") (TyVar "A"))]++    it "typechecks simple text" $ do+      tc "x" `shouldHaveType` "A"+      tc "\\x:T. x" `shouldHaveType` "T -> T"+      tc "\\X. x" `shouldHaveType` "forall X. A"+      tc "(\\x:T. x) y:T" `shouldHaveType` "T"+      tc "(\\f:(T->T) x:T. f x) (\\y:T. y)" `shouldHaveType` "T -> T"++  describe "unsafeExecTypecheckText" $ do+    let tc :: Text -> Ty Text+        tc input = unsafeExecTypecheckText input globals'++        globals' = fromList [("x", TypedExpr (Var "x") (TyVar "A"))]++    it "typechecks simple text" $ do+      Right (tc "x") `shouldHaveType` "A"+      Right (tc "\\x:T. x") `shouldHaveType` "T -> T"+      Right (tc "\\X. x") `shouldHaveType` "forall X. A"+      Right (tc "(\\x:T. x) y:T") `shouldHaveType` "T"+      Right (tc "(\\f:(T->T) x:T. f x) (\\y:T. y)") `shouldHaveType` "T -> T"

@@ -7,8 +7,6 @@  import Language.Lambda.Shared.Errors import Language.Lambda.Untyped-import Language.Lambda.Untyped.Eval-import Language.Lambda.Untyped.State  spec :: Spec spec = do@@ -97,6 +95,14 @@       let e1 = Abs "x" (Abs "x" (Var "x"))           e2 = Var "z"       betaReduce' e1 e2 `shouldBe` Abs "x" (Var "x")++    it "avoids captures" $ do+      let beta :: LambdaExpr Text -> LambdaExpr Text -> LambdaExpr Text+          beta e1 e2 = unsafeExecEval (betaReduce e1 e2) (mkEvalState ["z"])+      +      let e1 = Abs "f" $ Abs "x" $ App (Var "f") (Var "x")+          e2 = Abs "f" $ Var "x"+      beta e1 e2 `shouldBe` Abs "z" (Var "x")    describe "alphaConvert" $ do     let alphaConvert' :: [Text] -> [Text] -> LambdaExpr Text -> LambdaExpr Text

@@ -1,4 +1,3 @@-{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-} module Language.Lambda.Untyped.Examples.BoolSpec where  import RIO

@@ -1,4 +1,3 @@-{-# LANGUAGE NoImplicitPrelude, OverloadedStrings #-} module Language.Lambda.Untyped.Examples.NatSpec where  import RIO

@@ -1,4 +1,3 @@-{-# LANGUAGE NoImplicitPrelude #-} module Language.Lambda.Untyped.HspecUtils where  import RIO