define types within the language

haskell/src/FORecursiveTypes/Base.hs

@@ -54,8 +54,14 @@ matchVariant :: Type -> String -> Infer (Map.Map Name Type)
 matchVariant (Variant types) _ = return types
 matchVariant ty err = fail $ variantError ty err
 
+lookupTypeVar :: TypeMap -> Name -> Infer Type
+lookupTypeVar Empty x = fail $ "Unbound type variable " ++ show x
+lookupTypeVar (Bind c x t) y
+  | x == y = return t
+  | otherwise = lookup c y
+
 matchTypeVar :: TypeMap -> Type -> Infer Type
-matchTypeVar tymap (TypeVar x) = liftMaybe (Map.lookup x tymap) $ "Could not found type definition " ++ show x
+matchTypeVar tymap (TypeVar x) = lookupTypeVar tymap x
 matchTypeVar _ ty = return ty
 
 liftMaybe :: Monad m => Maybe a -> String -> m a
@@ -96,9 +102,9 @@ inferType ctx tymap (App t1 t2 _) = do
   (ty1, ty2) <- matchFun rty (show t1)
   checkType ctx tymap t2 ty1
   return ty2
+inferType ctx tymap (LetType n ty t _) = inferType ctx (Bind tymap n ty) t
 inferType _ _ t = fail $ "Cannot infer type of term " ++ show t
 
-
 checkType :: Ctx -> TypeMap -> Term -> Type -> Check
 checkType ctx tymap p@(Lam name t _) ty = do
   rty <- matchTypeVar tymap ty

haskell/src/FORecursiveTypes/ErrorList.hs

@@ -54,8 +54,14 @@ matchVariant :: Type -> String -> Infer (Map.Map Name Type)
 matchVariant (Variant types) _ = return types
 matchVariant ty err = fail $ variantError ty err
 
+lookupTypeVar :: TypeMap -> Name -> Infer Type
+lookupTypeVar Empty x = fail $ "Unbound type variable " ++ show x
+lookupTypeVar (Bind c x t) y
+  | x == y = return t
+  | otherwise = lookup c y
+
 matchTypeVar :: TypeMap -> Type -> Infer Type
-matchTypeVar tymap (TypeVar x) = liftMaybe (Map.lookup x tymap) $ "Could not found type definition " ++ show x
+matchTypeVar tymap (TypeVar x) = lookupTypeVar tymap x
 matchTypeVar _ ty = return ty
 
 liftMaybe :: Monad m => Maybe a -> String -> m a
@@ -96,9 +102,9 @@ inferType ctx tymap (App t1 t2 _) = do
   (ty1, ty2) <- matchFun rty (show t1)
   checkType ctx tymap t2 ty1
   return ty2
+inferType ctx tymap (LetType n ty t _) = inferType ctx (Bind tymap n ty) t
 inferType _ _ t = fail $ "Cannot infer type of term " ++ show t
 
-
 checkType :: Ctx -> TypeMap -> Term -> Type -> Check
 checkType ctx tymap p@(Lam name t _) ty = do
   rty <- matchTypeVar tymap ty

haskell/src/FORecursiveTypes/Language.hs

@@ -28,7 +28,10 @@ data Term =
     -- variant types
     Tag Name Term Parent |
     Match Term [(Name, Name, Term)] Parent |
-    Unit Parent
+    -- unit type
+    Unit Parent |
+    -- type def
+    LetType Name Type Term Parent
 
 
 instance Eq Term where
@@ -47,6 +50,7 @@ instance Eq Term where
   (Tag n1 t1 _) == (Tag n2 t2 _) = n1 == n2 && t1 == t2
   (Match m1 cases1 _) == (Match m2 cases2 _) = m1 == m2 && (all (\((l1, x1, t1),(l2, x2, t2)) -> l1 == l2 && x1 == x2 && t1 == t2) (zip cases1 cases2))
   (Unit _) == (Unit _) = True
+  (LetType n ty t _) == (LetType n' ty' t' _) = n == n' && ty == ty' && t == t'
   _ == _ = False
 
 type Parent = Maybe Term
@@ -66,6 +70,8 @@ parent (InR _ p) = p
 parent (Case _ _ _ _ _ p) = p
 parent (Tag _ _ p) = p
 parent (Match _ _ p) = p
+parent (Unit p) = p
+parent (LetType _ _ _ p) = p
 
 
 -- DSL for constructing terms
@@ -91,7 +97,6 @@ app = cons2 App
 lam n = cons1 (Lam n)
 anno ty = cons1 (flip Anno ty)
 
-unit = cons0 Unit
 zero = cons0 Zero
 succ = cons1 Succ
 add = cons2 Add
@@ -112,6 +117,8 @@ match1 m (l1, x1, t1) p = let res = Match (m (Just res)) [(l1, x1, t1 (Just res)
 match2 m (l1, x1, t1) (l2, x2, t2) p = let res = Match (m (Just res)) [(l1, x1, t1 (Just res)), (l2, x2, t2 (Just res))] p in res
 match3 m (l1, x1, t1) (l2, x2, t2) (l3, x3, t3) p = let res = Match (m (Just res)) [(l1, x1, t1 (Just res)), (l2, x2, t2 (Just res)), (l3, x3, t3 (Just res))] p in res
 
+unit = cons0 Unit
+type' n ty = cons1 (LetType n ty)
 
 
 instance Show Term where
@@ -136,11 +143,12 @@ instance Show Term where
   showsPrec p (Tag n t _) = showString "Tag " . showString n . showsPrec (p + 1) t
   showsPrec p (Match n cases _) = showString "Match"
   showsPrec p (Unit _) = showString "unit"
+  showsPrec p (LetType n ty t _) =
+    showString "let type " . showString n . showString " = " . showsPrec (p + 1) ty . showString " in " . showsPrec (p + 1) t
 
 data Type = UnitT | Nat | Fun Type Type | Sum Type Type | Variant (Map Name Type) | TypeVar Name | AnyType
   deriving (Show, Eq)
 
-type TypeMap = Map.Map Name Type
 
 instance PO.PartialOrd Type where
   _ <= AnyType = True
@@ -151,3 +159,5 @@ instance PO.PartialOrd Type where
 
 data Ctx = Empty | Bind Ctx Name Type
   deriving (Show, Eq)
+
+type TypeMap = Ctx

haskell/test/FORecursiveTypes/BaseSpec.hs

@@ -15,8 +15,5 @@ instance ConvertToBInfer B.Infer where
 main :: IO ()
 main = hspec spec
 
-typeMap :: TypeMap
-typeMap = fromList [("Nat", Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")]))]
-
 spec :: Spec
-spec = sharedSpec $ B.inferType Empty typeMap
+spec = sharedSpec $ B.inferType Empty Empty

haskell/test/FORecursiveTypes/ErrorListSpec.hs

@@ -19,9 +19,6 @@ instance ConvertToBInfer E.Infer where
 main :: IO ()
 main = hspec spec
 
-typeMap :: TypeMap
-typeMap = fromList [("Nat", Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")]))]
-
 spec :: Spec
-spec = sharedSpec $ E.inferType Empty typeMap
+spec = sharedSpec $ E.inferType Empty Empty
 

haskell/test/FORecursiveTypes/TestCases.hs

@@ -49,7 +49,7 @@ tFailMatchNotVariant = root $ (anno Nat (match1 (anno Nat zero) ("a", "x", succ
 
 tFailMatchUnequalTypesForCases = root $ (anno Nat (match2 (anno (Variant (fromList [("a", Nat), ("b", (Fun Nat Nat))])) (tag "b" (lam "x" (var "x")))) ("a", "x", succ $ var "x") ("b", "x", (var "x") )))
 
-tOkZeroRecNatType = root $ (anno (TypeVar "Nat") (tag "zero" unit))
-tOkNestedSuccRecNatType = root $ (anno (TypeVar "Nat") (tag "succ" (tag "succ" (tag "succ" (tag "zero" unit)))))
+tOkZeroRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (anno (TypeVar "Nat") (tag "zero" unit)))
+tOkNestedSuccRecNatType = root $ (type' "Nat" (Variant (fromList [("zero", UnitT), ("succ", TypeVar "Nat")])) (anno (TypeVar "Nat") (tag "succ" (tag "succ" (tag "succ" (tag "zero" unit))))))
 
 tFailRecTypeNotDefined = root $ (anno (TypeVar "Int") zero)