transformed record type checker in haskell

haskell/src/ProductTypes/Base.hs

+module ProductTypes.Base where
+
+import Prelude hiding ((>=), (<=), lookup)
+import Data.List(find)
+import Data.Map (Map)
+import qualified Data.Map as Map (lookup)
+
+import ProductTypes.Language
+import Util.ErrorMessages
+
+type Error = String
+
+data Infer a
+  = Inferred a
+  | NotInferred Error deriving (Eq, Show)
+
+type Check = Infer ()
+
+instance Functor Infer where
+  fmap _ (NotInferred err) = NotInferred err
+  fmap f (Inferred ty) = Inferred $ f ty
+
+instance Applicative Infer where
+  pure = Inferred
+  (NotInferred err) <*> _ = NotInferred err
+  (Inferred a) <*> something = fmap a something
+
+instance Monad Infer where
+  return = Inferred
+  (Inferred ty) >>= f = f ty
+  (NotInferred err) >>= _ = NotInferred err
+  fail = NotInferred
+
+-- matching functions that extract the inner types if possible
+-- one problem is that we do not get as good error messages, because term is not known in these functions
+matchNat :: Type -> String -> Check
+matchNat Nat _ = return ()
+matchNat ty err = fail $ natError ty err
+
+matchFun :: Type -> String -> Infer (Type, Type)
+matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
+matchFun ty err = fail $ funError ty err
+
+matchProd :: Type -> String -> Infer (Type, Type)
+matchProd (Prod ty1 ty2) _ = return (ty1, ty2)
+matchProd ty err = fail $ prodError ty err
+
+matchType :: Type -> Type -> String -> Check
+matchType ty1 ty2 _
+  | ty1 == ty2 = return ()
+matchType ty1 ty2 err = fail $ generalError (show ty1) ty2 err
+
+matchRecord :: Type -> String -> Infer (Map Name Type)
+matchRecord (Record pairs) _ = return pairs
+matchRecord ty err = fail $ recordError ty err
+
+
+liftMaybe :: Monad m => Maybe a -> String -> m a
+liftMaybe (Just a) _ = return a
+liftMaybe Nothing err = fail err
+
+lookup :: Ctx -> Name -> Infer Type
+lookup Empty x = fail $ "Unbound variable " ++ show x
+lookup (Bind c x t) y
+  | x == y = return t
+  | otherwise = lookup c y
+
+inferType :: Ctx -> Term -> Infer Type
+inferType _ (Zero _) = return Nat
+inferType ctx (Succ t _) = do
+  checkType ctx t Nat
+  return Nat
+inferType ctx (Add t1 t2 _) = do
+  checkType ctx t1 Nat
+  checkType ctx t2 Nat
+  return Nat
+inferType ctx (Mult t1 t2 _) = do
+  checkType ctx t1 Nat
+  checkType ctx t2 Nat
+  return Nat
+inferType ctx (Var name _) = lookup ctx name
+inferType ctx (Let name t body _) = do
+  tyt <- inferType ctx t
+  inferType (Bind ctx name tyt) body
+inferType ctx (Anno term ty _) = do
+  checkType ctx term ty
+  return ty
+inferType ctx (App t1 t2 _) = do
+  ty <- inferType ctx t1
+  (ty1, ty2) <- matchFun ty (show t1)
+  checkType ctx t2 ty1
+  return ty2
+inferType ctx (Fst t _) = do
+  ty <- inferType ctx t
+  (ty1, _) <- matchProd ty (show t)
+  return ty1
+inferType ctx (Snd t _) = do
+  ty <- inferType ctx t
+  (_, ty2) <- matchProd ty (show t)
+  return ty2
+inferType ctx (Sel n t _) = do
+  ty <- inferType ctx t
+  typairs <- matchRecord ty (show t)
+  liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
+inferType _ t = fail $ "Cannot infer type of term " ++ show t
+
+checkType :: Ctx -> Term -> Type -> Check
+checkType ctx p@(Lam name t _) ty = do
+  (ty1, ty2) <- matchFun ty (show p)
+  checkType (Bind ctx name ty1) t ty2
+checkType ctx p@(Pair t1 t2 _) ty = do
+  (ty1, ty2) <- matchProd ty (show p)
+  checkType ctx t1 ty1
+  checkType ctx t2 ty2
+checkType ctx p@(Rec tpairs _) ty = do
+  typairs <- matchRecord ty (show p)
+  if length tpairs == length typairs
+  then do
+    let subresults = map (\(tl, t) -> do
+          lty <- liftMaybe (Map.lookup tl typairs) ""
+          checkType ctx t lty
+          ) tpairs
+    foldl (>>) (return ()) subresults
+  else
+    fail "Length of term labels and type labels does not match"
+
+checkType ctx t ty = do
+  ty' <- inferType ctx t
+  matchType ty ty' (show t)

haskell/src/ProductTypes/ContinueAfterCheckFail.hs

+{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+module ProductTypes.ContinueAfterCheckFail where
+
+import Prelude hiding (Monad(..), (>=), (<=), lookup)
+import GHC.Exts (Constraint)
+import Data.List(find)
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import ProductTypes.Language
+import Util.ErrorMessages
+import Util.PartialOrd
+
+-- is needed because we use the RebindableSyntax extension
+ifThenElse :: Bool -> a -> a -> a
+ifThenElse True thn _ = thn
+ifThenElse False _ els = els
+
+type Error = [String]
+data Infer a = Inferred a | NotInferred Error
+
+type Check = Infer ()
+
+instance Functor Infer where
+  fmap _ (NotInferred err) = NotInferred err
+  fmap f (Inferred ty) = Inferred $ f ty
+
+instance Applicative Infer where
+  pure = Inferred
+  (NotInferred err) <*> _ = NotInferred err
+  (Inferred a) <*> something = fmap a something
+
+class WithTop a where
+  top :: a
+
+instance WithTop Type where
+  top = AnyType
+
+instance WithTop () where
+  top = ()
+
+instance (WithTop a, WithTop b) => WithTop (a, b) where
+  top = (top, top)
+
+instance WithTop a => WithTop [a] where
+  top = [top]
+
+instance WithTop a => WithTop (Map Name a) where
+  top = Map.empty
+
+-- Had to define an own monad type class.
+-- It is not possible otherwise to get the type constraint WithTop a.
+-- We use the extension ConstraintKinds to support this.
+-- Could not find a simpler solution for this problem.
+-- The restricted monad problem is common.
+class RMonad m where
+  type RMonadCtx m a :: Constraint
+  return :: RMonadCtx m a => a -> m a
+  (>>=) :: (RMonadCtx m a, RMonadCtx m b) => m a -> (a -> m b) -> m b
+  (>>) :: (RMonadCtx m a, RMonadCtx m b) => m a ->  m b -> m b
+  m >> k = m >>= \_ -> k
+  fail :: [String] -> m a
+
+instance RMonad Infer where
+  type RMonadCtx Infer a = WithTop a
+  return = Inferred
+  (Inferred ty) >>= f = f ty
+  NotInferred err1 >>= f =
+    -- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition
+    case f top of
+      Inferred _ -> fail err1
+      NotInferred err2 -> fail $ err1 ++ err2
+  fail = NotInferred
+
+
+-- matching functions that extract the inner types if possible
+matchNat :: Type -> String -> Check
+matchNat Nat _ =  return ()
+matchNat ty err = fail [natError ty err]
+
+matchFun :: Type -> String -> Infer (Type, Type)
+matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
+matchFun ty err = fail [funError ty err]
+
+matchProd :: Type -> String -> Infer (Type, Type)
+matchProd (Prod ty1 ty2) _ = return (ty1, ty2)
+matchProd ty err = fail [prodError ty err]
+
+matchType :: Type -> Type -> String -> Check
+matchType ty1 ty2 _ | ty1 >= ty2 = return ()
+matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
+
+matchRecord :: Type -> String -> Infer (Map Name Type)
+matchRecord (Record pairs) _ = return pairs
+matchRecord ty err = fail [recordError ty err]
+
+liftMaybe :: WithTop a => Maybe a -> String -> Infer a
+liftMaybe (Just a) _ = return a
+liftMaybe Nothing err = fail [err]
+
+
+lookup :: Ctx -> Name -> Infer Type
+lookup Empty x = fail ["Unbound variable " ++ show x]
+lookup (Bind c x t) y | x == y = return t
+                      | otherwise = lookup c y
+
+inferType :: Ctx -> Term -> Infer Type
+inferType _ (Zero _) = return Nat
+inferType ctx (Succ t _) = do
+  checkType ctx t Nat
+  return Nat
+inferType ctx (Add t1 t2 _) = do
+  checkType ctx t1 Nat
+  checkType ctx t2 Nat
+  return Nat
+inferType ctx (Mult t1 t2 _) = do
+  checkType ctx t1 Nat
+  checkType ctx t2 Nat
+  return Nat
+inferType ctx (Var name _) = lookup ctx name
+inferType ctx (Let name t body _) = do
+  tyt <- inferType ctx t
+  inferType (Bind ctx name tyt) body
+inferType ctx (Anno term ty _) = do
+  checkType ctx term ty
+  return ty
+inferType ctx (App t1 t2 _) = do
+  ty <- inferType ctx t1
+  (ty1, ty2) <- matchFun ty (show t1)
+  checkType ctx t2 ty1
+  return ty2
+inferType ctx (Fst t _) = do
+  ty <- inferType ctx t
+  (ty1, _) <- matchProd ty (show t)
+  return ty1
+inferType ctx (Snd t _) = do
+  ty <- inferType ctx t
+  (_, ty2) <- matchProd ty (show t)
+  return ty2
+inferType ctx (Sel n t _) = do
+  ty <- inferType ctx t
+  typairs <- matchRecord ty (show t)
+  liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
+inferType _ t = fail ["Cannot infer type of term " ++ show t]
+
+checkType :: Ctx -> Term -> Type -> Check
+checkType ctx p@(Lam name t _) ty = do
+  (ty1, ty2) <- matchFun ty (show p)
+  checkType(Bind ctx name ty1) t ty2
+checkType ctx p@(Pair t1 t2 _) ty = do
+  (ty1, ty2) <- matchProd ty (show p)
+  checkType ctx t1 ty1
+  checkType ctx t2 ty2
+checkType ctx p@(Rec tpairs _) ty = do
+  typairs <- matchRecord ty (show p)
+  if length tpairs == length typairs
+  then do
+    let subresults = map (\(tl, t) -> do
+          lty <- liftMaybe (Map.lookup tl typairs) ""
+          checkType ctx t lty
+          ) tpairs
+    foldl (>>) (return ()) subresults
+  else
+    fail ["Length of term labels and type labels does not match"]
+
+checkType ctx t ty = do
+  ty' <- inferType ctx t
+  matchType ty ty' (show t)

haskell/src/ProductTypes/EliminateContextArgument.hs

+{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+module ProductTypes.EliminateContextArgument where
+
+import Prelude hiding (Monad(..), (>=), (<=), lookup)
+import GHC.Exts (Constraint)
+import Data.List(find)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Maybe (isJust, fromJust)
+
+import ProductTypes.Language
+import Util.ErrorMessages
+import Util.PartialOrd
+
+-- is needed because we use the RebindableSyntax extension
+ifThenElse :: Bool -> a -> a -> a
+ifThenElse True thn _ = thn
+ifThenElse False _ els = els
+
+type Error = [String]
+data Infer a = Inferred a | NotInferred Error
+
+type Check = Infer ()
+
+instance Functor Infer where
+  fmap _ (NotInferred err) = NotInferred err
+  fmap f (Inferred ty) = Inferred $ f ty
+
+instance Applicative Infer where
+  pure = Inferred
+  (NotInferred err) <*> _ = NotInferred err
+  (Inferred a) <*> something = fmap a something
+
+class WithTop a where
+  top :: a
+
+instance WithTop Type where
+  top = AnyType
+
+instance WithTop () where
+  top = ()
+
+instance (WithTop a, WithTop b) => WithTop (a, b) where
+  top = (top, top)
+
+instance WithTop Ctx where
+  top = Empty
+
+instance WithTop a => WithTop [a] where
+  top = [top]
+
+instance WithTop a => WithTop (Map Name a) where
+  top = Map.empty
+
+-- Had to define an own monad type class.
+-- It is not possible otherwise to get the type constraint WithTop a.
+-- We use the extension ConstraintKinds to support this.
+-- Could not find a simpler solution for this problem.
+-- The restricted monad problem is common.
+class RMonad m where
+  type RMonadCtx m a :: Constraint
+  return :: RMonadCtx m a => a -> m a
+  (>>=) :: (RMonadCtx m a, RMonadCtx m b) => m a -> (a -> m b) -> m b
+  (>>) :: (RMonadCtx m a, RMonadCtx m b) => m a ->  m b -> m b
+  m >> k = m >>= \_ -> k
+  fail :: [String] -> m a
+
+instance RMonad Infer where
+  type RMonadCtx Infer a = WithTop a
+  return = Inferred
+  (Inferred ty) >>= f = f ty
+  NotInferred err1 >>= f =
+    -- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition
+    case f top of
+      Inferred _ -> fail err1
+      NotInferred err2 -> fail $ err1 ++ err2
+  fail = NotInferred
+
+
+-- matching functions that extract the inner types if possible
+matchNat :: Type -> String -> Infer Type
+matchNat Nat _ = Inferred Nat
+matchNat ty err = NotInferred [natError ty err]
+
+matchFun :: Type -> String -> Infer (Type, Type)
+matchFun (Fun ty1 ty2) _ = Inferred (ty1, ty2)
+matchFun ty err = NotInferred [funError ty err]
+
+matchProd :: Type -> String -> Infer (Type, Type)
+matchProd (Prod ty1 ty2) _ = Inferred (ty1, ty2)
+matchProd ty err = NotInferred [prodError ty err]
+
+matchType :: Type -> Type -> String -> Check
+matchType ty1 ty2 _ | ty1 >= ty2 = Inferred ()
+matchType ty1 ty2 err = NotInferred [generalError (show ty1) ty2 err]
+
+matchRecord :: Type -> String -> Infer (Map Name Type)
+matchRecord (Record pairs) _ = return pairs
+matchRecord ty err = fail [recordError ty err]
+
+liftMaybe :: WithTop a => Maybe a -> String -> Infer a
+liftMaybe (Just a) _ = return a
+liftMaybe Nothing err = fail [err]
+
+
+-- try to inline lookup
+-- assume that ctx != Empty if not otherwise stated because this case was already covered in the previous step
+-- if there is a bind replace lookup definition with it
+-- replace ctx of lookup with argument passed to context
+lookup :: Term -> Name -> Infer Type
+lookup t x = case parent t of
+  Just p@(Succ t _) -> do
+    lookup p x
+  Just p@(Add t1 t2 _) | t == t1 -> do
+    lookup p x
+  Just p@(Add t1 t2 _) | t == t2 -> do
+    lookup p x
+  Just p@(Mult t1 t2 _) | t == t1 -> do
+    lookup p x
+  Just p@(Mult t1 t2 _) | t == t2 -> do
+    lookup p x
+  Just p@(Var name _) -> do
+    lookup p x
+  Just p@(Let name term body _) | t == term -> do
+    lookup p x
+  Just p@(Let name term body _) | t == body ->
+    if name == x
+    then do
+      ty <- inferType term
+      return ty
+    else lookup p x
+  Just p@(Anno term ty _) -> do
+    lookup p x
+  Just p@(App t1 t2 _) | t == t1 -> do
+    lookup p x
+  Just p@(App t1 t2 _) | t == t2 -> do
+    lookup p x
+  Just p@(Fst t _) -> do
+    lookup p x
+  Just p@(Snd t _) -> do
+    lookup p x
+  Just p@(Lam name term _) ->
+    if name == x
+    then do
+      ty <- requiredType p
+      (ty1, ty2) <- matchFun ty (show p)
+      return ty1
+    else lookup p x
+  Just p@(Pair t1 t2 _) | t == t1 -> do
+    lookup p x
+  Just p@(Pair t1 t2 _) | t == t2 -> do
+    lookup p x
+  Just p@(Sel n term _) | t == term -> do
+    lookup p x
+  -- For every term we just call lookup on parent because the contex is not extended
+  -- Thus we have a single case without a guard simply call lookup on parent
+  -- because every entry of list has same parent
+  -- TODO: what would happen if the context is extended in different ways?
+  Just p@(Rec tpairs _) -> do
+    lookup p x
+  Just p -> do
+    lookup p x
+  Nothing -> fail ["Unbound variable " ++ show x]
+
+inferType :: Term -> Infer Type
+inferType (Zero _) = return Nat
+inferType (Succ t _) = do
+  checkType t
+  return Nat
+inferType (Add t1 t2 _) = do
+  checkType t1
+  checkType t2
+  return Nat
+inferType (Mult t1 t2 _) = do
+  checkType t1
+  checkType t2
+  return Nat
+inferType p@(Var name _) = lookup p name
+inferType (Let name t body _) = do
+  tyt <- inferType t
+  inferType body
+inferType (Anno term ty _) = do
+  checkType term
+  return ty
+inferType (App t1 t2 _) = do
+  ty <- inferType t1
+  (ty1, ty2) <- matchFun ty (show t1)
+  checkType t2
+  return ty2
+inferType (Fst t _) = do
+  ty <- inferType t
+  (ty1, _) <- matchProd ty (show t)
+  return ty1
+inferType (Snd t _) = do
+  ty <- inferType t
+  (_, ty2) <- matchProd ty (show t)
+  return ty2
+inferType (Sel n t _) = do
+  ty <- inferType t
+  typairs <- matchRecord ty (show t)
+  liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
+inferType t = fail ["Cannot infer type of term " ++ show t]
+
+checkType :: Term -> Check
+checkType p@(Lam name t _) = do
+  ty <- requiredType p
+  (ty1, ty2) <- matchFun ty (show p)
+  checkType t
+checkType p@(Pair t1 t2 _) = do
+  ty <- requiredType p
+  (ty1, ty2) <- matchProd ty (show p)
+  checkType t1
+  checkType t2
+checkType p@(Rec tpairs _) = do
+  ty <- requiredType p
+  typairs <- matchRecord ty (show p)
+  if length tpairs == length typairs
+  then do
+    let subresults = map (\(tl, t) -> do
+          lty <- liftMaybe (Map.lookup tl typairs) ""
+          checkType t
+          ) tpairs
+    foldl (>>) (return ()) subresults
+  else fail ["Length of term labels and type labels does not match"]
+checkType t = do
+  ty <- requiredType t
+  ty' <- inferType t
+  matchType ty ty' (show t)
+
+requiredType :: Term -> Infer Type
+requiredType t = case parent t of
+  Just (Succ t' _) | t == t' -> return Nat
+  Just (Add t1 t2 _) | t == t1 ->
+    return Nat
+  Just (Add t1 t2 _) | t == t2 ->
+    return Nat
+  Just (Mult t1 t2 _) | t == t1 ->
+    return Nat
+  Just (Mult t1 t2 _) | t == t2 ->
+    return Nat
+  Just (Anno term ty _) | t == term -> return ty
+  Just (App t1 t2 _) | t == t2 -> do
+    ty <- inferType t1
+    (ty1, ty2) <- matchFun ty (show t1)
+    return ty1
+  Just p@(Lam name term _) | t == term -> do
+    ty <- requiredType p
+    (ty1, ty2) <- matchFun ty (show p)
+    return ty2
+  Just p@(Pair t1 t2 _) | t == t1 -> do
+    ty <- requiredType p
+    (ty1, ty2) <- matchProd ty (show p)
+    return ty1
+  Just p@(Pair t1 t2 _) | t == t2 -> do
+    ty <- requiredType p
+    (ty1, ty2) <- matchProd ty (show p)
+    return ty2
+  Just p@(Rec tpairs _) -> do
+    ty <- requiredType p
+    typairs <- matchRecord ty (show p)
+    if length tpairs == length typairs
+    then do
+      -- TODO what happens if two labels have the same term?
+      -- TODO what happens if a label is used twice in a record?
+      let labeledterm = find (\(l, lt) -> lt == t) tpairs
+      if isJust labeledterm
+      then liftMaybe (Map.lookup (fst $ fromJust labeledterm) typairs) ""
+      else fail ["label associated with term not found"]
+    else fail ["Length of term labels and type labels does not match"]
+  _ -> fail ["Wrong arg passed"]
+
+

haskell/src/ProductTypes/EliminateTypeArgumentOfCheck.hs

+{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+module ProductTypes.EliminateTypeArgumentOfCheck where
+
+import Prelude hiding (Monad(..), (>=), (<=), lookup)
+import GHC.Exts (Constraint)
+import Data.List(find)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Maybe (isJust, fromJust)
+
+import ProductTypes.Language
+import Util.ErrorMessages
+import Util.PartialOrd
+
+-- is needed because we use the RebindableSyntax extension
+ifThenElse :: Bool -> a -> a -> a
+ifThenElse True thn _ = thn
+ifThenElse False _ els = els
+
+type Error = [String]
+data Infer a = Inferred a | NotInferred Error
+
+type Check = Infer ()
+
+instance Functor Infer where
+  fmap _ (NotInferred err) = NotInferred err
+  fmap f (Inferred ty) = Inferred $ f ty
+
+instance Applicative Infer where
+  pure = Inferred
+  (NotInferred err) <*> _ = NotInferred err
+  (Inferred a) <*> something = fmap a something
+
+class WithTop a where
+  top :: a
+
+instance WithTop Type where
+  top = AnyType
+
+instance WithTop () where
+  top = ()
+
+instance (WithTop a, WithTop b) => WithTop (a, b) where
+  top = (top, top)
+
+instance WithTop a => WithTop [a] where
+  top = [top]
+
+instance WithTop a => WithTop (Map Name a) where
+  top = Map.empty
+
+-- Had to define an own monad type class.
+-- It is not possible otherwise to get the type constraint WithTop a.
+-- We use the extension ConstraintKinds to support this.
+-- Could not find a simpler solution for this problem.
+-- The restricted monad problem is common.
+class RMonad m where
+  type RMonadCtx m a :: Constraint
+  return :: RMonadCtx m a => a -> m a
+  (>>=) :: (RMonadCtx m a, RMonadCtx m b) => m a -> (a -> m b) -> m b
+  (>>) :: (RMonadCtx m a, RMonadCtx m b) => m a ->  m b -> m b
+  m >> k = m >>= \_ -> k
+  fail :: [String] -> m a
+
+instance RMonad Infer where
+  type RMonadCtx Infer a = WithTop a
+  return = Inferred
+  (Inferred ty) >>= f = f ty
+  NotInferred err1 >>= f =
+    -- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition
+    case f top of
+      Inferred _ -> fail err1
+      NotInferred err2 -> fail $ err1 ++ err2
+  fail = NotInferred
+
+
+-- matching functions that extract the inner types if possible
+matchNat :: Type -> String -> Check
+matchNat Nat _ =  return ()
+matchNat ty err = fail [natError ty err]
+
+matchFun :: Type -> String -> Infer (Type, Type)
+matchFun (Fun ty1 ty2) _ = return (ty1, ty2)
+matchFun ty err = fail [funError ty err]
+
+matchProd :: Type -> String -> Infer (Type, Type)
+matchProd (Prod ty1 ty2) _ = return (ty1, ty2)
+matchProd ty err = fail [prodError ty err]
+
+matchType :: Type -> Type -> String -> Check
+matchType ty1 ty2 _ | ty1 >= ty2 = return ()