System F

0readme.md

bash-3.2$ ghc T.hs && ./T
[1 of 2] Compiling Main             ( T.hs, T.o ) [Source file changed]
[2 of 2] Linking T [Objects changed]
(a) -> (a)
Bool
Bool
Type error
CallStack (from HasCallStack):
  error, called at T.hs:126:16 in main:Main
Missing poly type: a
CallStack (from HasCallStack):
  error, called at T.hs:110:9 in main:Main

system_f.hs

-- original from <https://www.cs.ox.ac.uk/projects/gip/school/tc.hs> but URLs don't last long in academia
--
{-# LANGUAGE ExistentialQuantification,GADTs #-}

-- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)
-- demonstrates that it's possible to write functions of type
--    tc :: String -> Term a
-- where Term a is our strongly-typed GADT.
-- That is, generate a typed term from an untyped source; Lennart
-- Augustsson set this as a challenge.
--
-- In fact the main function goes
--    tc :: UTerm -> exists ty. (Ty ty, Term ty)
-- so the type checker returns a pair of an expression and its type,
-- wrapped, of course, in an existential.

module Main where

import Control.Concurrent
import Control.Exception
import Data.Void

-- Untyped world --------------------------------------------
data UTerm = UVar String
       | ULam String UType UTerm
       | UApp UTerm UTerm
       | UConBool Bool
       | UIf UTerm UTerm UTerm
       | UAppT UTerm UType

data UType = UBool | UArr UType UType | UType | UPoly String | UMeta String

-- Typed world -----------------------------------------------
data Ty t where
  Bool :: Ty Bool
  Arr  :: Ty a -> Ty b -> Ty (a -> b)
  Poly :: String -> Ty Type
  TypeType :: Ty Type

data Term g t where
  Var :: Var g t -> Term g t
  Lam :: Ty a -> Term (g,a) b -> Term g (a->b)
  App :: Term g (s -> t) -> Term g s -> Term g t
  ConBool :: Bool -> Term g Bool
  If :: Term g Bool -> Term g a -> Term g a -> Term g a
  Type :: Term g b -> Term g Type

data a :-> b
data Type

data Var g t where
  ZVar :: Var (h,t) t
  SVar :: Var h t -> Var (h,s) t

data Typed thing = forall ty. Typed (Ty ty) (thing ty)

-- Typechecking types
data ExType = forall t. ExType (Ty t)

tcType :: TyEnv g -> UType -> ExType
tcType _ UType = ExType TypeType
tcType _ UBool = ExType Bool
tcType g (UPoly s) = ExType (Poly s)
tcType g (UMeta s) = case lookupVar s g of
  Typed ty thing -> ExType ty
tcType g (UArr t1 t2) = case tcType g t1 of { ExType t1' ->
              case tcType g t2 of { ExType t2' ->
              ExType (Arr t1' t2') }}

-- The type environment and lookup
data TyEnv g where
  Nil  :: TyEnv g
  Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t)

lookupVar :: String -> TyEnv g -> Typed (Var g)
lookupVar s Nil = error $ "Variable not found: " ++ s
lookupVar v (Cons s ty e)
  | v==s      = Typed ty ZVar
  | otherwise = case lookupVar v e of
           Typed ty v -> Typed ty (SVar v)

data Equal a b where
  Equal :: Equal c c

cmpTy :: Ty a -> Ty b -> Maybe (Equal a b)
cmpTy TypeType TypeType = Just Equal
cmpTy TypeType _ = Nothing
cmpTy _ TypeType = Nothing
-- poly type unifies only with itself
cmpTy (Poly s) (Poly t) | s == t = Just Equal
cmpTy Poly{} _ = Nothing
cmpTy _ Poly{} = Nothing

cmpTy Bool Bool = Just Equal
cmpTy (Arr a1 a2) (Arr b1 b2)
  = do    { Equal <- cmpTy a1 b1
    ; Equal <- cmpTy a2 b2
    ; return Equal }

-- Typechecking terms
tc :: UTerm -> TyEnv g -> Typed (Term g)
tc (UVar v) env = case lookupVar v env of
            Typed ty v -> Typed ty (Var v)
tc (UConBool b) env
  = Typed Bool (ConBool b)
tc (ULam s ty body) env
  = case tcType env ty of { ExType bndr_ty' ->
    case bndr_ty' of
      TypeType ->
        error $ "Missing poly type: " ++ s
      _ ->
        case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' ->
        Typed (Arr bndr_ty' body_ty')
          (Lam bndr_ty' body') }}
tc (UApp e1 e2) env
  = case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' ->
    case tc e2 env of { Typed arg_ty e2' ->
    case cmpTy arg_ty bndr_ty of
    Nothing -> error "Type error"
    Just Equal -> Typed body_ty (App e1' e2') }}
tc (UIf e1 e2 e3) env
  = case tc e1 env of { Typed Bool e1' ->
    case tc e2 env of { Typed t2   e2' ->
    case tc e3 env of { Typed t3   e3' ->
    case cmpTy t2 t3 of
    Nothing -> error "Type error"
    Just Equal -> Typed t2 (If e1' e2' e3') }}}
tc (UAppT (ULam name UType uterm) utype) env =
  tc (substitute uterm name utype) env

substitute :: UTerm -> String -> UType -> UTerm
substitute uterm name utype = go uterm where
  go (ULam name' utype' body') =
    ULam name' (substituteT utype' name utype) (go body')
  go (UApp t1 t2) = UApp (go t1) (go t2)
  go (UIf t1 t2 t3) = UIf (go t1) (go t2) (go t3)
  go s@UConBool{} = s
  go s@UVar{} = s

substituteT :: UType -> String -> UType -> UType
substituteT utype name newutype = go utype where
  go (UMeta s) | s == name = newutype
  go UBool = UBool
  go (UArr t1 t2) = UArr (go t1) (go t2)

showType :: Ty a -> String
showType Bool = "Bool"
showType TypeType = "Type"
showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")"
showType (Poly s) = s

uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True))

uId = ULam "a" UType (ULam "x" (UMeta "a") (UVar "x"))

uId_error = ULam "a" UType (ULam "x" (UMeta "a") (UIf (UConBool True) (UVar "x") (UConBool False)))

main = do
 putStrLn (case tc (UAppT uId (UPoly "a")) Nil of
            Typed ty _ -> showType ty
        )
 putStrLn (case tc (UApp uNot (UConBool True)) Nil of
            Typed ty _ -> showType ty
        )
 putStrLn (case tc (UApp uNot (UApp (UAppT uId UBool) (UConBool True))) Nil of
            Typed ty _ -> showType ty
        )
 ok $ putStrLn (case tc (UAppT uId_error (UPoly "a")) Nil of
            Typed ty _ -> showType ty
        )
 ok $ putStrLn (case tc uId Nil of
            Typed ty _ -> showType ty
        )

  where ok m = catch (m >> pure ()) (\(SomeException e) -> print e)