lambda-calculator 1.1.1 → 2.0.0

raw patch · 6 files changed

+230/−8 lines, 6 filesdep +containersdep ~basedep ~optparse-applicativePVP ok

version bump matches the API change (PVP)

Dependencies added: containers

Dependency ranges changed: base, optparse-applicative

API changes (from Hackage documentation)

Files

• app/Main.hs +1/−0
• lambda-calculator.cabal +11/−7
• src/Language/SystemF/Expression.hs +10/−1
• src/Language/SystemF/TypeCheck.hs +119/−0
• test/Language/SystemF/ExpressionSpec.hs +14/−0
• test/Language/SystemF/TypeCheckSpec.hs +75/−0

@@ -2,6 +2,7 @@  import Data.Version +import Data.Semigroup import Options.Applicative hiding (ParseError) import System.Console.Shell import System.Console.Shell.ShellMonad

@@ -1,5 +1,5 @@ name:                lambda-calculator-version:             1.1.1+version:             2.0.0 synopsis:            A lambda calculus interpreter description:         Please see README.md homepage:            https://github.com/sgillespie/lambda-calculus#readme@@ -24,8 +24,10 @@                         Language.SystemF,                        Language.SystemF.Expression,-                       Language.SystemF.Parser-  build-depends:       base <= 5,+                       Language.SystemF.Parser,+                       Language.SystemF.TypeCheck+  build-depends:       base >= 4.9 && < 5,+                       containers,                        parsec   default-language:    Haskell2010 @@ -34,9 +36,9 @@   main-is:             Main.hs   other-modules:       Paths_lambda_calculator   ghc-options:         -threaded -rtsopts -with-rtsopts=-N-  build-depends:       base,+  build-depends:       base >= 4.9,                        lambda-calculator,-                       optparse-applicative < 0.13,+                       optparse-applicative >= 0.13,                        Shellac,                        Shellac-readline   default-language:    Haskell2010@@ -58,9 +60,11 @@                         Language.SystemFSpec,                        Language.SystemF.ExpressionSpec,-                       Language.SystemF.ParserSpec-  build-depends:       base <= 5,+                       Language.SystemF.ParserSpec,+                       Language.SystemF.TypeCheckSpec+  build-depends:       base < 5,                        lambda-calculator,+                       containers,                        hspec,                        HUnit   ghc-options:         -threaded -rtsopts -with-rtsopts=-N

@@ -1,4 +1,3 @@-{-# LANGUAGE FlexibleInstances #-} module Language.SystemF.Expression where  import Data.Monoid@@ -19,6 +18,7 @@ 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)  -- Pretty printing@@ -94,6 +94,7 @@       -> PDoc String pprTy pdoc space (TyVar n) = prettyPrint n `add` pdoc pprTy pdoc space (TyArrow a b) = pprTyArrow pdoc space a b+pprTy pdoc _     (TyForAll n t) =  pprTyForAll pdoc n t  pprTyArrow :: PrettyPrint n            => PDoc String@@ -113,6 +114,14 @@ pprTyArrow' space a b = a <> arrow <> b   where arrow | space     = " -> " `add` empty               | otherwise = "->" `add` empty++pprTyForAll :: PrettyPrint n+            => PDoc String+            -> n+            -> Ty n+            -> PDoc String+pprTyForAll pdoc n t = prefix <> prettyPrint t `add` pdoc+  where prefix = between (prettyPrint n `add` empty) "forall " ". " empty  -- Pretty print a type abstraction pprTAbs :: (PrettyPrint n, PrettyPrint t)

@@ -0,0 +1,119 @@+module Language.SystemF.TypeCheck where++import Data.Map+import Prelude hiding (lookup)++import Language.Lambda.Util.PrettyPrint+import Language.SystemF.Expression++type UniqueSupply n = [n]+type Context n t = Map n t++typecheck :: (Ord n, Eq n, PrettyPrint n)+          => UniqueSupply n +          -> Context n (Ty n)+          -> SystemFExpr n n +          -> Either String (Ty n)+typecheck uniqs ctx (Var v)        = tcVar uniqs ctx v+typecheck uniqs ctx (Abs n t body) = tcAbs uniqs ctx n t body+typecheck uniqs ctx (App e1 e2)    = tcApp uniqs ctx e1 e2+typecheck uniqs ctx (TyAbs t body) = tcTyAbs uniqs ctx t body+typecheck uniqs ctx (TyApp e ty)   = tcTyApp uniqs ctx e ty++tcVar :: (Ord n, Eq n, PrettyPrint n)+      => UniqueSupply n+      -> Context n (Ty n)+      -> n+      -> Either String (Ty n)+tcVar uniqs ctx var = maybe (TyVar <$> unique uniqs) return (lookup var ctx)++tcAbs :: (Ord n, Eq n, PrettyPrint n)+      => UniqueSupply n+      -> Context n (Ty n)+      -> n+      -> Ty n+      -> SystemFExpr n n+      -> Either String (Ty n)+tcAbs uniqs ctx name ty body = TyArrow ty <$> typecheck uniqs ctx' body+  where ctx' = insert name ty ctx++tcApp :: (Ord n, Eq n, PrettyPrint n)+      => UniqueSupply n+      -> Context n (Ty n)+      -> SystemFExpr n n+      -> SystemFExpr n n+      -> Either String (Ty n)+tcApp uniqs ctx e1 e2 = do+    t1 <- typecheck uniqs ctx e1+    t2 <- typecheck uniqs ctx e2++    -- Unwrap t1; Should be (t2 -> *)+    (t2', t3) <- either genMismatchVar return (arrow t1)++    if t2' == t2+      then return t3+      else Left $ tyMismatchMsg (TyArrow t2 t3) (TyArrow t1 t3)++  where genMismatchVar expected = tyMismatchMsg expected <$> unique uniqs >>= Left+        arrow (TyArrow t1 t2) = return (t1, t2)+        arrow t               = Left t++tcTyAbs :: (Ord n, Eq n, PrettyPrint n)+        => UniqueSupply n+        -> Context n (Ty n)+        -> n+        -> SystemFExpr n n+        -> Either String (Ty n)+tcTyAbs uniqs ctx ty body = TyForAll ty <$> typecheck uniqs ctx' body+  where ctx' = insert ty (TyVar ty) ctx++tcTyApp :: (Ord n, Eq n, PrettyPrint n)+        => UniqueSupply n+        -> Context n (Ty n)+        -> SystemFExpr n n+        -> Ty n+        -> Either String (Ty n)+tcTyApp uniqs ctx (TyAbs t expr) ty = typecheck uniqs ctx expr'+  where expr' = sub t ty expr+tcTyApp uniqs ctx expr ty = typecheck uniqs ctx expr++-- Utilities+unique :: UniqueSupply t+       -> Either String t+unique (u:_) = return u+unique _     = fail "Unique supply ran out"++sub :: Eq n+    => n+    -> Ty n+    -> SystemFExpr n n+    -> SystemFExpr n n+sub name ty (App e1 e2)   = App (sub name ty e1) (sub name ty e2)+sub name ty (Abs n ty' e) = Abs n (subTy name ty ty') (sub name ty e)+sub name ty (TyAbs ty' e) = TyAbs ty' (sub name ty e) +sub name ty (TyApp e ty') = TyApp (sub name ty e) (subTy name ty ty')+sub name ty expr = expr++subTy :: Eq n+      => n+      -> Ty n+      -> Ty n+      -> Ty n+subTy name ty (TyArrow t1 t2) +  = TyArrow (subTy name ty t1) (subTy name ty t2)+subTy name ty ty'@(TyVar name') +  | name == name' = ty+  | otherwise     = ty'+subTy name t1 t2@(TyForAll name' t2') +  | name == name' = t2+  | otherwise     = TyForAll name' (subTy name t2 t2')+++tyMismatchMsg :: (PrettyPrint t, PrettyPrint t')+              => t+              -> t'+              -> String+tyMismatchMsg expected actual = "Couldn't match expected type " +++                                prettyPrint expected +++                                " with actual type " +++                                prettyPrint actual

@@ -58,6 +58,9 @@   it "print simple arrow types" $     prettyPrint (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B" +  it "prints simple forall types" $+    prettyPrint (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"+   it "prints chained arrow types" $     prettyPrint (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))       `shouldBe` "X -> Y -> Z"@@ -65,3 +68,14 @@   it "prints nested arrow types" $     prettyPrint (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))       `shouldBe` "(T -> U) -> V"++  it "prints complex forall types" $+    prettyPrint (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))+      `shouldBe` "forall A. A -> A"++  it "prints nested forall types" $+    prettyPrint (TyForAll "W" +                  (TyForAll "X" +                    (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))+      `shouldBe` "forall W. forall X. W -> X -> Y"+

@@ -0,0 +1,75 @@+module Language.SystemF.TypeCheckSpec (spec) where++import Data.Either+import Data.Map++import Test.Hspec++import Language.Lambda.Util.PrettyPrint+import Language.SystemF.Expression+import Language.SystemF.TypeCheck++tc :: (Ord n, Eq n, PrettyPrint n)+          => UniqueSupply n +          -> [(n, Ty n)]+          -> SystemFExpr n n +          -> Either String (Ty n)+tc uniqs ctx = typecheck uniqs (fromList ctx)++spec :: Spec+spec = describe "typecheck" $ do+  it "typechecks simple variables in context" $+    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")++  it "typechecks simple variables not in context" $ +    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")++  it "typechecks simple abstractions" $+    tc [] [] (Abs "x" (TyVar "A") (Var "x")) +      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))++  it "typechecks simple applications" $ do+    let ctx = [+          ("f", TyArrow (TyVar "T") (TyVar "U")),+          ("a", TyVar "T")+          ]++    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")++  it "apply variable to variable fails" $ do+    let ctx = [+          ("a", TyVar "A"),+          ("b", TyVar "B")+          ]++    tc ["C"] ctx (App (Var "a") (Var "b")) +      `shouldSatisfy` isLeft++  it "apply arrow to variable of wrong type fails" $ do+    let ctx = [+          ("f", TyArrow (TyVar "F") (TyVar "G")),+          ("b", TyVar "B")+          ]++    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft++  it "typechecks simple type abstractions" $+    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))++  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 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")++  it "typechecks simple type applications" $+    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))+      `shouldBe` Right (TyVar "A")++  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"))