Add monomorphic type annotations.

app/Main.hs

@@ -114,8 +114,8 @@ commandParser = do
 
 class MonadState AppState m => MonadApp m where
   parsed        :: Either ParseError a -> m a
-  typecheckDecl :: Text -> CheckExpr -> m (Maybe Scheme)
+  typecheckDecl :: Maybe Type -> Text -> CheckExpr -> m (Maybe Scheme)
-  typecheckExpr ::         CheckExpr -> m (Maybe Scheme)
+  typecheckExpr ::                       CheckExpr -> m (Maybe Scheme)
   execute       :: CheckExpr -> m EvalExpr
 
 type AppM = ExceptT Text (StateT AppState (InputT IO))
@@ -127,8 +127,8 @@ instance MonadApp AppM where
   parsed (Left err) = throwError $ T.pack $ show err
   parsed (Right ok) = pure ok
 
-  typecheckDecl = typecheck . Just
+  typecheckDecl ty = typecheck ty    . Just
-  typecheckExpr = typecheck Nothing
+  typecheckExpr    = typecheck Nothing Nothing
 
   execute checkExpr = do
     defs <- gets definitions
@@ -148,10 +148,10 @@ instance MonadApp AppM where
         liftInput $ mapM_ (outputTextLn . unparseEval) trace
         pure value
 
-typecheck :: Maybe Text -> CheckExpr -> AppM (Maybe Scheme)
+typecheck :: Maybe Type -> Maybe Text -> CheckExpr -> AppM (Maybe Scheme)
-typecheck decl expr = do
+typecheck tann decl expr = do
   defs <- gets definitions
-  let type_ = infer $ substitute defs expr
+  let type_ = maybe infer check tann $ substitute defs expr
   checkOpts <- gets checkOptions
   if shouldTypecheck checkOpts
     then case type_ of
@@ -184,10 +184,10 @@ define name expr = modify \appState ->
   in appState { definitions = HM.insert name expr' $ definitions appState }
 
 runDeclOrExpr :: MonadApp m => DeclOrExprAST -> m ()
-runDeclOrExpr (Left (name, exprAST)) = do
+runDeclOrExpr (Left (name, ty, exprAST)) = do
   defs <- gets definitions
   let expr = substitute defs $ ast2check exprAST
-  _ <- typecheckDecl name expr
+  _ <- typecheckDecl ty name expr
   define name expr
 runDeclOrExpr (Right exprAST) = do
   defs <- gets definitions

package.yaml

@@ -14,6 +14,7 @@ extra-source-files:
 
 default-extensions:
 - BlockArguments
+- ConstraintKinds
 - DefaultSignatures
 - EmptyCase
 - EmptyDataDeriving

src/Ivo/Evaluator.hs

@@ -14,7 +14,7 @@ import Control.Monad.Loops (iterateM_)
 import Control.Monad.State (MonadState, evalState, modify', state, put, gets)
 import Control.Monad.Writer (runWriterT, tell)
 import Data.HashMap.Strict qualified as HM
-import Data.Void (Void, absurd)
+import Data.Void (absurd)
 
 isReducible :: EvalExpr -> Bool
 -- Applications of function type constructors

src/Ivo/Evaluator/Base.hs

@@ -1,5 +1,5 @@
 module Ivo.Evaluator.Base
-  ( Identity (..)
+  ( Identity (..), Void
   , Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text
   , substitute, substitute1, rename, rename1, free, bound, used
   , Eval, EvalExpr, EvalExprF, EvalX, EvalXF (..)
@@ -17,6 +17,7 @@ import Data.Functor.Identity (Identity (..))
 import Data.Functor.Foldable (embed, cata, para)
 import Data.HashMap.Strict qualified as HM
 import Data.Traversable (for)
+import Data.Void (Void)
 
 data Eval
 type EvalExpr = Expr Eval
@@ -24,6 +25,7 @@ type instance AppArgs Eval = EvalExpr
 type instance AbsArgs Eval = Text
 type instance LetArgs Eval = VoidF EvalExpr
 type instance CtrArgs Eval = UnitF EvalExpr
+type instance AnnX    Eval = Void
 type instance XExpr   Eval = EvalX
 
 type EvalX = EvalXF EvalExpr

src/Ivo/Expression.hs

@@ -1,5 +1,6 @@
 module Ivo.Expression
   ( Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), DefF (..), VoidF, UnitF (..), Text
+  , Type (..), TypeF (..), Scheme (..), tapp
   , substitute, substitute1, rename, free, bound, used
   , Eval, EvalExpr, EvalX, EvalXF (..), Identity (..)
   , pattern AppFE, pattern CtrE, pattern CtrFE,
@@ -10,7 +11,6 @@ module Ivo.Expression
   , Check, CheckExpr, CheckExprF, CheckX, CheckXF (..)
   , pattern AppFC, pattern CtrC, pattern CtrFC, pattern CallCCC, pattern CallCCFC
   , pattern FixC, pattern FixFC, pattern HoleC, pattern HoleFC
-  , Type (..), TypeF (..), Scheme (..), tapp
   , ast2check, ast2eval, check2eval, check2ast, eval2ast
   , builtins
   ) where
@@ -41,6 +41,7 @@ ast2check = substitute builtins . cata \case
   LetRecFP (nx, ex) e -> App (Abs nx e) (App FixC (Abs nx ex))
   CtrF ctr es -> foldl' App (CtrC ctr) es
   CaseF ps -> Case ps
+  AnnF () e t -> Ann () e t
   PNatF n -> int2ast n
   PListF es -> mkList es
   PStrF s -> mkList $ map (App (CtrC CChar) . int2ast . fromEnum) $ unpack s
@@ -63,6 +64,7 @@ check2eval = cata \case
   LetF (Def nx ex) e -> App (Abs nx e) ex
   CtrFC ctr -> CtrE ctr
   CaseF ps -> Case ps
+  AnnF () e _ -> e
   CallCCFC -> CallCCE
   FixFC -> z
   HoleFC -> omega
@@ -88,6 +90,7 @@ check2ast = hoist go . rename (HM.keysSet builtins)
       LetF (Def nx ex) e -> LetFP ((nx, ex) :| []) e
       CtrFC ctr -> CtrF ctr []
       CaseF ps -> CaseF ps
+      AnnF () e t -> AnnF () e t
       CallCCFC-> VarF "callcc"
       FixFC -> VarF "fix"
       HoleFC -> HoleFP

src/Ivo/Expression/Base.hs

@@ -1,9 +1,11 @@
-{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 module Ivo.Expression.Base
   ( Text, VoidF, UnitF (..), absurd'
-  , Expr (..), Ctr (..), Pat, Def, AppArgs, AbsArgs, LetArgs, CtrArgs, XExpr
+  , Expr (..), Ctr (..), Pat, Def, AppArgs, AbsArgs, LetArgs, CtrArgs, AnnX, XExpr
   , ExprF (..), PatF (..), DefF (..), AppArgsF, LetArgsF, CtrArgsF, XExprF
+  , Type (..), TypeF (..), Scheme (..), tapp
   , RecursivePhase, projectAppArgs, projectLetArgs, projectCtrArgs, projectXExpr, projectDef
   , embedAppArgs, embedLetArgs, embedCtrArgs, embedXExpr, embedDef
   , Substitutable, free, bound, used, collectVars, rename, rename1
@@ -15,30 +17,34 @@ import Control.Monad.Reader (MonadReader, Reader, runReader, asks, local)
 import Control.Monad.State (MonadState, StateT, evalStateT, state)
 import Control.Monad.Zip (MonadZip, mzipWith)
 import Data.Foldable (fold)
-import Data.Functor.Foldable (Base, Recursive, Corecursive, project, embed)
+import Data.Functor.Foldable (Base, Recursive, Corecursive, project, embed, cata)
+import Data.Functor.Foldable.TH (makeBaseFunctor)
 import Data.HashMap.Strict (HashMap)
 import Data.HashMap.Strict qualified as HM
 import Data.HashSet (HashSet)
 import Data.HashSet qualified as HS
-import Data.Kind (Type)
+import Data.Kind qualified as Kind
+import Data.List (foldl1')
 import Data.Stream qualified as S
 import Data.Text (Text)
 import Data.Text qualified as T
 
 data Expr phase
-  -- | A variable: `x`.
+  -- | A variable: @x@.
   = Var !Text
-  -- | Function application: `f x_0 ... x_n`.
+  -- | Function application: @f x_0 ... x_n@.
   | App !(Expr phase) !(AppArgs phase)
-  -- | Lambda abstraction: `λx_0 ... x_n. e`.
+  -- | Lambda abstraction: @λx_0 ... x_n. e@.
   | Abs !(AbsArgs phase) !(Expr phase)
-  -- | Let expression: `let x_0 = v_0 ... ; x_n = v_n in e`.
+  -- | Let expression: @let x_0 = v_0 ... ; x_n = v_n in e@.
   | Let !(LetArgs phase) !(Expr phase)
-  -- | Data constructor, e.g. `(x, y)` or `Left`.
+  -- | Data constructor, e.g. @(x, y)@ or @Left@.
   | Ctr !Ctr !(CtrArgs phase)
   -- | Case expression to pattern match against a value,
-  -- e.g. `case { Left x1 -> e1 ; Right x2 -> e2 }`.
+  -- e.g. @case { Left x1 -> e1 ; Right x2 -> e2 }@.
   | Case ![Pat phase]
+  -- | Type annotations: @expr : type@.
+  | Ann !(AnnX phase) !(Expr phase) Type
   -- | Additional phase-specific constructors.
   | ExprX !(XExpr phase)
 
@@ -46,23 +52,30 @@ type family AppArgs phase
 type family AbsArgs phase
 type family LetArgs phase
 type family CtrArgs phase
+type family AnnX    phase
 type family XExpr phase
 
-deriving instance
+class
-  ( Eq (AppArgs phase)
+  ( c (AppArgs phase)
-  , Eq (AbsArgs phase)
+  , c (AbsArgs phase)
-  , Eq (LetArgs phase)
+  , c (LetArgs phase)
-  , Eq (CtrArgs phase)
+  , c (CtrArgs phase)
-  , Eq (XExpr   phase)
+  , c (AnnX    phase)
-  ) => Eq (Expr phase)
+  , c (XExpr   phase)
+  ) => ForallX c phase
 
-deriving instance
+instance
-  ( Show (AppArgs phase)
+  ( c (AppArgs phase)
-  , Show (AbsArgs phase)
+  , c (AbsArgs phase)
-  , Show (LetArgs phase)
+  , c (LetArgs phase)
-  , Show (CtrArgs phase)
+  , c (CtrArgs phase)
-  , Show (XExpr   phase)
+  , c (AnnX    phase)
-  ) => Show (Expr phase)
+  , c (XExpr   phase)
+  ) => ForallX c phase
+
+deriving instance ForallX Eq phase  => Eq (Expr phase)
+
+deriving instance ForallX Show phase => Show (Expr phase)
 
 -- | Data constructors (used in pattern matching and literals).
 data Ctr
@@ -94,6 +107,41 @@ data PatF r = Pat { patCtr :: !Ctr, patNames :: ![Text], patBody :: !r }
 -- | A definition, mapping a name to a value.
 type Def phase = (Text, Expr phase)
 
+-- | A monomorphic type.
+data Type
+  -- | Type variable.
+  = TVar Text
+  -- | Type application.
+  | TApp Type Type
+  -- | The function type.
+  | TAbs
+  -- | The product type.
+  | TProd
+  -- | The sum type.
+  | TSum
+  -- | The unit type.
+  | TUnit
+  -- | The empty type.
+  | TVoid
+  -- | The type of natural numbers.
+  | TNat
+  -- | The type of lists.
+  | TList
+  -- | The type of characters.
+  | TChar
+  deriving (Eq, Show)
+
+tapp :: [Type] -> Type
+tapp []  = error "Empty type applications are not permitted"
+tapp [t] = t
+tapp ts  = foldl1' TApp ts
+
+-- | A polymorphic type.
+data Scheme
+  -- | Universally quantified type variables.
+  = TForall [Text] Type
+  deriving (Eq, Show)
+
 ---
 --- Base functor boilerplate for recursion-schemes
 ---
@@ -105,14 +153,29 @@ data ExprF phase r
   | LetF !(LetArgsF phase r) r
   | CtrF Ctr (CtrArgsF phase r)
   | CaseF [PatF r]
+  | AnnF !(AnnX phase) r Type
   | ExprXF !(XExprF phase r)
 
 type instance Base (Expr phase) = ExprF phase
 
-type family AppArgsF phase :: Type -> Type
+type family AppArgsF phase :: Kind.Type -> Kind.Type
-type family LetArgsF phase :: Type -> Type
+type family LetArgsF phase :: Kind.Type -> Kind.Type
-type family CtrArgsF phase :: Type -> Type
+type family CtrArgsF phase :: Kind.Type -> Kind.Type
-type family XExprF phase :: Type -> Type
+type family XExprF   phase :: Kind.Type -> Kind.Type
+
+class
+  ( c (AppArgsF phase)
+  , c (LetArgsF phase)
+  , c (CtrArgsF phase)
+  , c (XExprF   phase)
+  ) => ForallXF c phase
+
+instance
+  ( c (AppArgsF phase)
+  , c (LetArgsF phase)
+  , c (CtrArgsF phase)
+  , c (XExprF   phase)
+  ) => ForallXF c phase
 
 data DefF r = Def !Text !r
   deriving (Eq, Functor, Foldable, Traversable, Show)
@@ -128,12 +191,7 @@ data VoidF a
 absurd' :: VoidF a -> b
 absurd' x = case x of {}
 
-instance
+instance ForallXF Functor phase  => Functor (ExprF phase) where
-  ( Functor (AppArgsF phase)
-  , Functor (LetArgsF phase)
-  , Functor (CtrArgsF phase)
-  , Functor (XExprF phase)
-  ) => Functor (ExprF phase) where
   fmap f = \case
     VarF n -> VarF n
     AppF ef exs -> AppF (f ef) (fmap f exs)
@@ -141,14 +199,10 @@ instance
     LetF ds e -> LetF (fmap f ds) (f e)
     CtrF c es -> CtrF c (fmap f es)
     CaseF ps -> CaseF (fmap (fmap f) ps)
+    AnnF x e t -> AnnF x (f e) t
     ExprXF q -> ExprXF (fmap f q)
 
-instance
+instance ForallXF Foldable phase => Foldable (ExprF phase) where
-  ( Foldable (AppArgsF phase)
-  , Foldable (LetArgsF phase)
-  , Foldable (CtrArgsF phase)
-  , Foldable (XExprF   phase)
-  ) => Foldable (ExprF phase) where
   foldMap f = \case
     VarF _ -> mempty
     AppF ef exs -> f ef <> foldMap f exs
@@ -156,14 +210,10 @@ instance
     LetF ds e -> foldMap f ds <> f e
     CtrF _ es -> foldMap f es
     CaseF ps -> foldMap (foldMap f) ps
+    AnnF _ e _ -> f e
     ExprXF q -> foldMap f q
 
-instance
+instance ForallXF Traversable phase => Traversable (ExprF phase) where
-  ( Traversable (AppArgsF phase)
-  , Traversable (LetArgsF phase)
-  , Traversable (CtrArgsF phase)
-  , Traversable (XExprF   phase)
-  ) => Traversable (ExprF phase) where
   traverse f = \case
     VarF n -> pure $ VarF n
     AppF ef exs -> AppF <$> f ef <*> traverse f exs
@@ -171,6 +221,7 @@ instance
     LetF ds e -> LetF <$> traverse f ds <*> f e
     CtrF c es -> CtrF c <$> traverse f es
     CaseF ps -> CaseF <$> traverse (traverse f) ps
+    AnnF x e t -> (\e' -> AnnF x e' t) <$> f e
     ExprXF q -> ExprXF <$> traverse f q
 
 class Functor (ExprF phase) => RecursivePhase phase where
@@ -226,6 +277,7 @@ instance RecursivePhase phase => Recursive (Expr phase) where
     Let ds e -> LetF (projectLetArgs ds) e
     Ctr c es -> CtrF c (projectCtrArgs es)
     Case ps -> CaseF ps
+    Ann x e t -> AnnF x e t
     ExprX q -> ExprXF (projectXExpr q)
 
 instance RecursivePhase phase => Corecursive (Expr phase) where
@@ -236,8 +288,11 @@ instance RecursivePhase phase => Corecursive (Expr phase) where
     LetF ds e -> Let (embedLetArgs ds) e
     CtrF c es -> Ctr c (embedCtrArgs es)
     CaseF ps -> Case ps
+    AnnF x e t -> Ann x e t
     ExprXF q -> ExprX (embedXExpr q)
 
+makeBaseFunctor ''Type
+
 ---
 --- End base functor boilerplate.
 ---
@@ -283,6 +338,34 @@ class Substitutable e where
   unsafeSubstitute1 :: Text -> e -> e -> e
   unsafeSubstitute1 n e = unsafeSubstitute (HM.singleton n e)
 
+instance Substitutable Type where
+  collectVars withVar _ = cata \case
+    TVarF n -> withVar n
+    t -> fold t
+
+  -- /All/ variables in a monomorphic type are free.
+  rename _ t = t
+
+  -- No renaming step is necessary.
+  substitute substs = cata \case
+    TVarF n -> HM.findWithDefault (TVar n) n substs
+    e -> embed e
+
+  unsafeSubstitute = substitute
+
+instance Substitutable Scheme where
+  collectVars withVar withBinder (TForall names t) =
+    foldMap withBinder names $ collectVars withVar withBinder t
+
+  rename = runRenamer \badNames (TForall names t) ->
+    uncurry TForall <$> replaceNames badNames names (pure t)
+
+  -- I took a shot at implementing this but found it to be quite difficult
+  -- because merging the foralls is tricky.
+  -- It's not undoable, but it wasn't worth my further time investment
+  -- seeing as this function isn't currently used anywhere.
+  unsafeSubstitute = error "Substitution for schemes not yet implemented"
+
 --
 -- These primitives are likely to be useful for implementing `rename`.
 -- Ideally, I would like to find a way to move the implementation of `rename` here entirely,

src/Ivo/Syntax/Base.hs

@@ -1,5 +1,6 @@
 module Ivo.Syntax.Base
   ( Expr (..), ExprF (..), Ctr (..), Pat, Def, DefF (..), PatF (..), VoidF, Text, NonEmpty (..)
+  , Type (..), TypeF (..), Scheme (..), tapp
   , substitute, substitute1, rename, rename1, free, bound, used
   , Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..)
   , pattern LetFP, pattern LetRecP, pattern LetRecFP
@@ -36,6 +37,7 @@ type instance AppArgs Parse = NonEmpty AST
 type instance AbsArgs Parse = NonEmpty Text
 type instance LetArgs Parse = NonEmpty (Def Parse)
 type instance CtrArgs Parse = [AST]
+type instance AnnX    Parse = ()
 type instance XExpr   Parse = ASTX
 
 type ASTX = ASTXF AST
@@ -107,10 +109,10 @@ pattern HoleP = ExprX HoleP_
 pattern HoleFP :: ASTF r
 pattern HoleFP = ExprXF HoleP_
 
-{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, ExprXF                               #-}
+{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, AnnF, ExprXF                               #-}
-{-# COMPLETE Var,  App,  Abs,  Let,   Ctr,  Case,  LetRecP,  PNat,  PList,  PChar,  PStr,  HoleP  #-}
+{-# COMPLETE Var,  App,  Abs,  Let,   Ctr,  Case,  Ann,  LetRecP,  PNat,  PList,  PChar,  PStr,  HoleP  #-}
-{-# COMPLETE VarF, AppF, AbsF, LetF , CtrF, CaseF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
+{-# COMPLETE VarF, AppF, AbsF, LetF , CtrF, CaseF, AnnF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
-{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
+{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, AnnF, LetRecFP, PNatF, PListF, PCharF, PStrF, HoleFP #-}
 
 -- TODO: Implement Substitutable for AST.
 

src/Ivo/Syntax/Parser.hs

@@ -1,17 +1,19 @@
 module Ivo.Syntax.Parser
   ( ParseError, parse
-  , DeclOrExprAST, ProgramAST
+  , Declaration, DeclOrExprAST, ProgramAST
   , parseAST, parseDeclOrExpr, parseProgram
-  , astParser, declOrExprParser, programParser
+  , typeParser, schemeParser, astParser, declOrExprParser, programParser
   ) where
 
 import Ivo.Syntax.Base
 
+import Data.Functor.Identity (Identity)
 import Data.List.NonEmpty (fromList)
 import Data.Text qualified as T
 import Prelude hiding (succ, either)
 import Text.Parsec hiding (label, token, spaces)
 import Text.Parsec qualified
+import Text.Parsec.Expr
 import Text.Parsec.Text (Parser)
 
 spaces :: Parser ()
@@ -36,7 +38,7 @@ token :: Char -> Parser ()
 token ch = label [ch] $ char ch *> spaces
 
 keywords :: [Text]
-keywords = ["let", "in", "Left", "Right", "S", "Z", "Char"]
+keywords = ["let", "in", "Left", "Right", "S", "Z", "forall", "Char", "Void", "Unit", "Nat", "Char"]
 
 -- | A keyword is an exact string which is not part of an identifier.
 keyword :: Text -> Parser ()
@@ -56,6 +58,9 @@ identifier = label "identifier" $ do
 variable :: Parser AST
 variable = label "variable" $ Var <$> identifier
 
+tvariable :: Parser Type
+tvariable = label "variable" $ TVar <$> identifier
+
 many1' :: Parser a -> Parser (NonEmpty a)
 many1' p = fromList <$> many1 p
 
@@ -65,22 +70,29 @@ many2 p = (,) <$> p <*> many1' p
 grouping :: Parser AST
 grouping = label "grouping" $ between (token '(') (token ')') ambiguous
 
+tgrouping :: Parser Type
+tgrouping = label "grouping" $ between (token '(') (token ')') tambiguous
+
 application :: Parser AST
-application = uncurry App <$> many2 block
+application = label "application" $ uncurry App <$> many2 block
+
+tapplication :: Parser Type
+tapplication = label "application" $ uncurry tapp' <$> many2 tblock
+  where tapp' t1 (t2 :| ts) = tapp (t1 : t2 : ts)
 
 abstraction :: Parser AST
 abstraction = label "lambda abstraction" $ Abs <$> between lambda (token '.') (many1' identifier) <*> ambiguous
   where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces
 
 definition :: Parser (Def Parse)
-definition = do
+definition = label "definition" $ do
   name <- identifier
   token '='
   value <- ambiguous
   pure (name, value)
 
 let_ :: Parser AST
-let_ = letrecstar <|> letstar
+let_ = label "let expression" $ letrecstar <|> letstar
   where
     letrecstar = LetRecP <$> between (try (keyword "letrec")) (keyword "in") definition <*> ambiguous
     letstar = Let <$> between (keyword "let") (keyword "in") definitions <*> ambiguous
@@ -89,7 +101,7 @@ let_ = letrecstar <|> letstar
     definitions = fromList <$> sepBy1 definition (token ';')
 
 ctr :: Parser AST
-ctr = pair <|> unit <|> either <|> nat <|> list <|> str
+ctr = label "data constructor" $ pair <|> unit <|> either <|> nat <|> list <|> str
   where
     unit, pairCtr, tuple, either, left, right,
       zero, succ, natLit, consCtr, cons, charCtr, charLit, strLit :: Parser AST
@@ -166,9 +178,62 @@ case_ = label "case patterns" $ do
   token '}'
   pure $ Case pats
 
+ann :: Parser AST
+ann = label "type annotation" $ do
+  e <- block
+  token ':'
+  t <- tambiguous
+  pure (Ann () e t)
+
 hole :: Parser AST
 hole = label "hole" $ HoleP <$ token '_'
 
+tlist :: Parser Type
+tlist = between (token '[') (token ']') $ ((TApp TList <$> tambiguous) <|> pure TList)
+
+tinfix :: Parser Type
+tinfix = buildExpressionParser ttable tblock
+  where
+    ttable :: [[Operator Text () Identity Type]]
+    ttable = [ [Infix (binop TAbs  <$ arrSym)    AssocRight]
+             , [Infix (binop TProd <$ token '*') AssocRight]
+             , [Infix (binop TSum  <$ token '+') AssocRight]
+             ]
+
+    arrSym :: Parser ()
+    arrSym = token '→' <|> keyword "->"
+
+    binop :: Type -> Type -> Type -> Type
+    binop c t1 t2 = TApp (TApp c t1) t2
+
+tctr :: Parser Type
+tctr = tlist <|> tunit <|> tvoid <|> tnat <|> tchar
+  where
+    tunit = TUnit <$ (keyword "Unit" <|> keyword "⊤")
+    tvoid = TVoid <$ (keyword "Void" <|> keyword "⊥")
+    tnat  = TNat  <$ (keyword "Nat"  <|> keyword "ℕ")
+    tchar = TChar <$  keyword "Char"
+
+tfinite :: Parser Type
+tfinite = tvariable <|> tlist <|> tctr <|> tgrouping
+
+tblock :: Parser Type
+tblock = tfinite
+
+tambiguous :: Parser Type
+tambiguous = try tinfix <|> try tapplication <|> tblock
+
+tforall :: Parser Scheme
+tforall = do
+  keyword "forall" <|> token '∀'
+  names <- many1 (identifier <* spaces)
+  token '.'
+  ty <- tambiguous
+  pure $ TForall names ty
+
+scheme :: Parser Scheme
+scheme = tforall <|> (TForall [] <$> tambiguous)
+
 -- | Guaranteed to consume a finite amount of input
 finite :: Parser AST
 finite = label "finite expression" $ variable <|> hole <|> ctr <|> case_ <|> grouping
@@ -179,7 +244,13 @@ block = label "block expression" $ abstraction <|> let_ <|> finite
 
 -- | Not guaranteed to consume input at all, may continue until it reaches a terminator
 ambiguous :: Parser AST
-ambiguous = label "any expression" $ try application <|> block
+ambiguous = label "any expression" $ try ann <|> try application <|> block
+
+typeParser :: Parser Type
+typeParser = tambiguous
+
+schemeParser :: Parser Scheme
+schemeParser = scheme
 
 astParser :: Parser AST
 astParser = ambiguous
@@ -187,18 +258,26 @@ astParser = ambiguous
 parseAST :: Text -> Either ParseError AST
 parseAST = parse (spaces *> ambiguous <* eof) "input"
 
-type Declaration = (Text, AST)
+type Declaration = (Text, Maybe Type, AST)
+
+definitionAnn :: Parser Declaration
+definitionAnn = do
+  name <- identifier
+  ty <- optionMaybe $ token ':' *> tambiguous
+  token '='
+  e <- ambiguous
+  pure (name, ty, e)
 
 declaration :: Parser Declaration
 declaration = notFollowedBy (try let_) >> (declrec <|> decl)
   where
     declrec = do
       try $ keyword "letrec"
-      (name, expr) <- definition
+      (name, ty, expr) <- definitionAnn
-      pure (name, LetRecP (name, expr) (Var name))
+      pure (name, ty, LetRecP (name, expr) (Var name))
     decl = do
       keyword "let"
-      definition
+      definitionAnn
 
 -- | A program is a series of declarations and expressions to execute.
 type ProgramAST = [DeclOrExprAST]

src/Ivo/Syntax/Printer.hs

@@ -1,10 +1,11 @@
-module Ivo.Syntax.Printer (unparseAST) where
+module Ivo.Syntax.Printer (unparseAST, unparseType, unparseScheme) where
 
 import Ivo.Syntax.Base
 
 import Data.Functor.Base (NonEmptyF (NonEmptyF))
 import Data.Functor.Foldable (cata)
 import Data.List.NonEmpty (toList)
+import Data.Text qualified as T
 import Data.Text.Lazy (fromStrict, toStrict, intercalate, unwords, singleton)
 import Data.Text.Lazy.Builder (Builder, fromText, fromLazyText, toLazyText, fromString)
 import Prelude hiding (unwords)
@@ -62,6 +63,7 @@ unparseAST = toStrict . toLazyText . snd . cata \case
   CaseF pats ->
     let pats' = fromLazyText $ intercalate "; " $ map (toLazyText . unparsePat) pats
     in tag Finite $ "{ " <> pats' <> " }"
+  AnnF () e t -> tag Ambiguous $ final e <> " : " <> fromText (unparseType t)
   PNatF n -> tag Finite $ fromString $ show n
   PListF es ->
     let es' = fromLazyText $ intercalate ", " $ map (toLazyText . unambiguous) es
@@ -95,3 +97,28 @@ unparseAST = toStrict . toLazyText . snd . cata \case
 
     unparsePat (Pat ctr ns e)
       = unambiguous (unparseCtr ctr (map (tag Finite . fromText) ns)) <> " -> " <> unambiguous e
+
+-- HACK
+pattern TApp2 :: Type -> Type -> Type -> Type
+pattern TApp2 tf tx ty = TApp (TApp tf tx) ty
+
+-- TODO: Improve these printers.
+unparseType :: Type -> Text
+unparseType (TVar name) = name
+unparseType (TApp2 TAbs a b) = "(" <> unparseType a <> " -> " <> unparseType b <> ")"
+unparseType (TApp2 TProd a b) = "(" <> unparseType a <> " * " <> unparseType b <> ")"
+unparseType (TApp2 TSum a b) = "(" <> unparseType a <> " + " <> unparseType b <> ")"
+unparseType (TApp TList a) = "[" <> unparseType a <> "]"
+unparseType (TApp a b) = "(" <> unparseType a <> " " <> unparseType b <> ")"
+unparseType TAbs = "(->)"
+unparseType TProd = "(*)"
+unparseType TSum = "(+)"
+unparseType TUnit = "★"
+unparseType TVoid = "⊥"
+unparseType TNat = "Nat"
+unparseType TList = "[]"
+unparseType TChar = "Char"
+
+unparseScheme :: Scheme -> Text
+unparseScheme (TForall [] t) = unparseType t
+unparseScheme (TForall names t) = "∀" <> T.unwords names <>  ". " <> unparseType t

src/Ivo/Types.hs

@@ -1,8 +1,9 @@
 module Ivo.Types
   ( module Ivo.Types.Base
-  , infer
+  , infer, check
   ) where
 
+import Ivo.Syntax.Printer
 import Ivo.Types.Base
 
 import Control.Applicative ((<|>))
@@ -99,6 +100,10 @@ j (Case ctrs) = do
 j (CtrC ctr) = do
   (t_ret, ts_n) <- ctrTy ctr
   pure $ foldr (\t_a t_r -> tapp [TAbs, t_a, t_r]) t_ret ts_n
+j (Ann () e t_ann) = do
+  t_ret <- j e
+  unify t_ret t_ann
+  pure t_ann
 j CallCCC = do
   t_a <- fresh
   t_b <- fresh
@@ -156,3 +161,13 @@ infer e = do
   s <- solve' c
   let t' = substitute s t
   pure $ runReader (generalize t') HM.empty
+
+check :: Type -> CheckExpr -> Either Text Scheme
+check t_ann e = do
+  (t, c) <- runInferencer do
+    t_ret <- j e
+    unify t_ret t_ann
+    pure t_ann
+  s <- solve' c
+  let t' = substitute s t
+  pure $ runReader (generalize t') HM.empty

src/Ivo/Types/Base.hs

@@ -1,30 +1,26 @@
-{-# LANGUAGE TemplateHaskell #-}
 module Ivo.Types.Base
   ( Identity (..)
   , Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text
+  , Type (..), TypeF (..), Scheme (..), tapp
   , substitute, substitute1, rename, rename1, free, bound, used
   , Check, CheckExpr, CheckExprF, CheckX, CheckXF (..)
   , pattern AppFC, pattern CtrC, pattern CtrFC, pattern CallCCC, pattern CallCCFC
   , pattern FixC, pattern FixFC, pattern HoleC, pattern HoleFC
-  , Type (..), TypeF (..), Scheme (..), tapp
   , Substitution, Context, Constraint
   , MonoSubstitutable, substituteMono, substituteMono1
-  , unparseType, unparseScheme
   ) where
 
+import Ivo.Expression.Base
+
 import Control.Monad (forM)
 import Control.Monad.Reader (asks)
 import Data.Bifunctor (bimap, first)
 import Data.Foldable (fold)
 import Data.Functor.Foldable (embed, cata, para)
-import Data.Functor.Foldable.TH (makeBaseFunctor)
 import Data.Functor.Identity (Identity (..))
 import Data.HashMap.Strict (HashMap)
 import Data.HashMap.Strict qualified as HM
-import Data.List (foldl1')
-import Data.Text qualified as T
 import Data.Traversable (for)
-import Ivo.Expression.Base
 
 data Check
 type CheckExpr = Expr Check
@@ -32,6 +28,7 @@ type instance AppArgs Check = CheckExpr
 type instance AbsArgs Check = Text
 type instance LetArgs Check = (Text, CheckExpr)
 type instance CtrArgs Check = UnitF CheckExpr
+type instance AnnX    Check = ()
 type instance XExpr   Check = CheckX
 
 type CheckX = CheckXF CheckExpr
@@ -79,15 +76,15 @@ pattern HoleC = ExprX HoleC_
 pattern HoleFC :: CheckExprF r
 pattern HoleFC = ExprXF HoleC_
 
-{-# COMPLETE Var,  App,   Abs,  Let,  CtrC,  Case,  ExprX                   #-}
+{-# COMPLETE Var,  App,   Abs,  Let,  CtrC,  Case,  Ann,  ExprX                   #-}
-{-# COMPLETE VarF, AppF,  AbsF, LetF, CtrFC, CaseF, ExprXF                  #-}
+{-# COMPLETE VarF, AppF,  AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF                  #-}
-{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF,  CaseF, ExprXF                  #-}
+{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF,  CaseF, AnnF, ExprXF                  #-}
-{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, ExprXF                  #-}
+{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF                  #-}
-{-# COMPLETE Var,  App,   Abs,  Let,  Ctr,   Case,  CallCCC,  FixC,  HoleC  #-}
+{-# COMPLETE Var,  App,   Abs,  Let,  Ctr,   Case,  Ann,  CallCCC,  FixC,  HoleC  #-}
-{-# COMPLETE Var,  App,   Abs,  Let,  CtrC,  Case,  CallCCC,  FixC,  HoleC  #-}
+{-# COMPLETE Var,  App,   Abs,  Let,  CtrC,  Case,  Ann,  CallCCC,  FixC,  HoleC  #-}
-{-# COMPLETE VarF, AppF,  AbsF, LetF, CtrFC, CaseF, CallCCFC, FixFC, HoleFC #-}
+{-# COMPLETE VarF, AppF,  AbsF, LetF, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-}
-{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF,  CaseF, CallCCFC, FixFC, HoleFC #-}
+{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF,  CaseF, AnnF, CallCCFC, FixFC, HoleFC #-}
-{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, CallCCFC, FixFC, HoleFC #-}
+{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-}
 
 instance RecursivePhase Check where
   projectAppArgs = Identity
@@ -125,66 +122,6 @@ instance Substitutable CheckExpr where
     CaseF pats -> Case <$> for pats \(Pat ctr ns e) -> Pat ctr ns <$> maySubstitute ns e
     e -> embed <$> traverse snd e
 
--- | A monomorphic type.
-data Type
-  -- | Type variable.
-  = TVar Text
-  -- | Type application.
-  | TApp Type Type
-  -- | The function type.
-  | TAbs
-  -- | The product type.
-  | TProd
-  -- | The sum type.
-  | TSum
-  -- | The unit type.
-  | TUnit
-  -- | The empty type.
-  | TVoid
-  -- | The type of natural numbers.
-  | TNat
-  -- | The type of lists.
-  | TList
-  -- | The type of characters.
-  | TChar
-  deriving (Eq, Show)
-
-makeBaseFunctor ''Type
-
-instance Substitutable Type where
-  collectVars withVar _ = cata \case
-    TVarF n -> withVar n
-    t -> fold t
-
-  -- /All/ variables in a monomorphic type are free.
-  rename _ t = t
-
-  -- No renaming step is necessary.
-  substitute substs = cata \case
-    TVarF n -> HM.findWithDefault (TVar n) n substs
-    e -> embed e
-
-  unsafeSubstitute = substitute
-
--- | A polymorphic type.
-data Scheme
-  -- | Universally quantified type variables.
-  = TForall [Text] Type
-  deriving (Eq, Show)
-
-instance Substitutable Scheme where
-  collectVars withVar withBinder (TForall names t) =
-    foldMap withBinder names $ collectVars withVar withBinder t
-
-  rename = runRenamer \badNames (TForall names t) ->
-    uncurry TForall <$> replaceNames badNames names (pure t)
-
-  -- I took a shot at implementing this but found it to be quite difficult
-  -- because merging the foralls is tricky.
-  -- It's not undoable, but it wasn't worth my further time investment
-  -- seeing as this function isn't currently used anywhere.
-  unsafeSubstitute = error "Substitution for schemes not yet implemented"
-
 type Substitution = HashMap Text Type
 type Context = HashMap Text Scheme
 type Constraint = (Type, Type)
@@ -210,33 +147,3 @@ instance MonoSubstitutable t => MonoSubstitutable [t] where
 
 instance MonoSubstitutable t => MonoSubstitutable (HashMap a t) where
   substituteMono = fmap . substituteMono
-
-tapp :: [Type] -> Type
-tapp []  = error "Empty type applications are not permitted"
-tapp [t] = t
-tapp ts  = foldl1' TApp ts
-
--- HACK
-pattern TApp2 :: Type -> Type -> Type -> Type
-pattern TApp2 tf tx ty = TApp (TApp tf tx) ty
-
--- TODO: Improve these printers.
-unparseType :: Type -> Text
-unparseType (TVar name) = name
-unparseType (TApp2 TAbs a b) = "(" <> unparseType a <> " -> " <> unparseType b <> ")"
-unparseType (TApp2 TProd a b) = "(" <> unparseType a <> " * " <> unparseType b <> ")"
-unparseType (TApp2 TSum a b) = "(" <> unparseType a <> " + " <> unparseType b <> ")"
-unparseType (TApp TList a) = "[" <> unparseType a <> "]"
-unparseType (TApp a b) = "(" <> unparseType a <> " " <> unparseType b <> ")"
-unparseType TAbs = "(->)"
-unparseType TProd = "(*)"
-unparseType TSum = "(+)"
-unparseType TUnit = "★"
-unparseType TVoid = "⊥"
-unparseType TNat = "Nat"
-unparseType TList = "[]"
-unparseType TChar = "Char"
-
-unparseScheme :: Scheme -> Text
-unparseScheme (TForall [] t) = unparseType t
-unparseScheme (TForall names t) = "∀" <> T.unwords names <>  ". " <> unparseType t