SProp sketch

SPropSketch.hs

{-# LANGUAGE PatternSynonyms #-}

type Ix = Int
type Lvl = Int
type ULvl = Int

data Sort = Type ULvl | Prop
  deriving (Show, Eq)

data SortType = SType | SProp
  deriving (Show, Eq)

data Proj = Fst | Snd
  deriving (Eq)

instance Show Proj where
  show Fst = "fst"
  show Snd = "snd"

data Tm
  = Var Ix
  | Let Tm Tm Tm

  | Lam SortType Tm
  | App Tm Tm SortType
  | Pi Tm SortType Tm

  | Pair Tm SortType Tm SortType
  | Proj Proj Tm
  | Sigma Tm SortType Tm

  | Sort Sort

  | Bot
  | Exfalso Tm

  | Id Tm SortType Tm Tm
  | Refl

instance Show Tm where
  show (Var i) = show i
  show (Let ty val body) = "(let " ++ show ty ++ " = " ++ show val ++ "; " ++ show body ++ ")"
  show (Lam _ body) = "(\\" ++ show body ++ ")"
  show (App fn arg _) = "(" ++ show fn ++ " " ++ show arg ++ ")"
  show (Pi ty _ body) = "(" ++ show ty ++ " -> " ++ show body ++ ")"
  show (Pair a _ b _) = "(" ++ show a ++ ", " ++ show b ++ ")"
  show (Proj p t) = "(" ++ show p ++ " " ++ show t ++ ")"
  show (Sigma ty _ body) = "(" ++ show ty ++ " ** " ++ show body ++ ")"
  show (Sort sort) = show sort
  show Bot = "Bot"
  show (Exfalso tm) = "(exfalso " ++ show tm ++ ")"
  show (Id _ _ a b) = "(" ++ show a ++ " = " ++ show b ++ ")"
  show Refl = "Refl"

umax :: Sort -> Sort -> Sort
umax _ Prop = Prop
umax Prop (Type i) = Type i
umax (Type i) (Type j) = Type (max i j)

-- values
type Env = [Val]
data Clos = Clos Tm Env

data Elim
  = EApp Val SortType
  | EProj Proj
  | EExfalso
type Sp = [Elim]

data Val
  = VNe Lvl Sp
  | VLam SortType Clos
  | VPi Val SortType Clos
  | VPair Val SortType Val SortType
  | VSigma Val SortType Clos
  | VSort Sort
  | VBot
  | VId Val SortType Val Val
  | VRefl

pattern VVar l = VNe l []

-- evaluation
vinst :: Clos -> Val -> Val
vinst (Clos tm vs) v = eval (v : vs) tm

vapp :: Val -> Val -> SortType -> Val
vapp (VLam _ c) v s = vinst c v
vapp (VNe h sp) v s = VNe h (EApp v s : sp)
vapp _ _ _ = error "vapp"

vproj :: Proj -> Val -> Val
vproj Fst (VPair v _ _ _) = v
vproj Snd (VPair _ _ v _) = v
vproj p (VNe h s) = VNe h (EProj p : s)
vproj _ _ = error "vproj"

vexfalso :: Val -> Val
vexfalso (VNe h s) = VNe h (EExfalso : s)
vexfalso _ = error "vexfalso"

eval :: Env -> Tm -> Val
eval vs (Var i) = vs !! i
eval vs (Let _ v b) = eval (eval vs v : vs) b
eval vs (Lam s b) = VLam s (Clos b vs)
eval vs (App a b s) = vapp (eval vs a) (eval vs b) s
eval vs (Pi t s b) = VPi (eval vs t) s (Clos b vs)
eval vs (Pair a s b s') = VPair (eval vs a) s (eval vs b) s'
eval vs (Proj p t) = vproj p (eval vs t)
eval vs (Sigma t s b) = VSigma (eval vs t) s (Clos b vs)
eval vs (Sort s) = VSort s
eval vs Bot = VBot
eval vs (Exfalso tm) = vexfalso (eval vs tm)
eval vs (Id ty s a b) = VId (eval vs ty) s (eval vs a) (eval vs b)
eval vs Refl = VRefl

quoteElim :: Lvl -> Elim -> Tm -> Tm
quoteElim l (EApp v s) t = App t (quote l v) s
quoteElim l (EProj p) t = Proj p t
quoteElim l EExfalso t = Exfalso t

quote :: Lvl -> Val -> Tm
quote l (VNe hd sp) = foldr (quoteElim l) (Var (l - hd - 1)) sp
quote l (VLam s c) = Lam s (quote (l + 1) $ vinst c (VVar l))
quote l (VPi ty s c) = Pi (quote l ty) s (quote (l + 1) $ vinst c (VVar l))
quote l (VPair a s b s') = Pair (quote l a) s (quote l b) s'
quote l (VSigma ty s c) = Sigma (quote l ty) s (quote (l + 1) $ vinst c (VVar l))
quote _ (VSort s) = Sort s
quote _ VBot = Bot
quote l (VId ty s a b) = Id (quote l ty) s (quote l a) (quote l b)
quote l VRefl = Refl

nf :: Tm -> Tm
nf = quote 0 . eval []

-- conversion
convSp :: Lvl -> Sp -> Sp -> Bool
convSp l [] [] = True
convSp l (EApp v s : sp) (EApp v' _ : sp') = convSp l sp sp' && conv l s v v'
convSp l (EProj p : sp) (EProj p' : sp') = convSp l sp sp' && p == p'
convSp l (EExfalso : sp) (EExfalso : sp') = convSp l sp sp'
convSp _ _ _ = False

conv :: Lvl -> SortType -> Val -> Val -> Bool
conv _ SProp _ _ = True
conv l _ (VSort s) (VSort s') = s == s'
conv l _ VBot VBot = True
conv l _ VRefl _ = True
conv l _ _ VRefl = True
conv l _ (VId ty s a b) (VId ty' s' a' b') = s == s' && conv l SType ty ty' && conv l s a a' && conv l s b b'
conv l ss (VLam s c) (VLam _ c') = let v = VVar l in conv (l + 1) ss (vinst c v) (vinst c' v)
conv l ss (VLam s c) w = let v = VVar l in conv (l + 1) ss (vinst c v) (vapp w v s)
conv l ss w (VLam s c) = let v = VVar l in conv (l + 1) ss (vapp w v s) (vinst c v)
conv l _ (VPair a s b s') (VPair a' _ b' _) = conv l s a a' && conv l s' b b'
conv l _ (VPair a s b s') v = conv l s a (vproj Fst v) && conv l s' b (vproj Snd v)
conv l _ v (VPair a s b s') = conv l s (vproj Fst v) a && conv l s' (vproj Snd v) b
conv l ss (VPi ty s c) (VPi ty' s' c') = s == s' && conv l s ty ty' && (let v = VVar l in conv (l + 1) ss (vinst c v) (vinst c' v))
conv l ss (VSigma ty s c) (VSigma ty' s' c') = s == s' && conv l s ty ty' && (let v = VVar l in conv (l + 1) ss (vinst c v) (vinst c' v))
conv l _ (VNe hd sp) (VNe hd' sp') = hd == hd' && convSp l sp sp'
conv l _ _ _ = False

convTypes :: Lvl -> Val -> Val -> Bool
convTypes l a b = conv l SType a b

-- context
data Ctx = Ctx { lvl :: Lvl, vs :: [Val], ts :: [Val] }

emptyCtx :: Ctx
emptyCtx = Ctx 0 [] []

bind :: Ctx -> Val -> Ctx
bind (Ctx lvl vs ts) ty = Ctx (lvl + 1) (VVar lvl : vs) (ty : ts)

define :: Ctx -> Val -> Val -> Ctx
define (Ctx lvl vs ts) ty val = Ctx (lvl + 1) (val : vs) (ty : ts)

-- typechecking
type TC t = Either String t

check :: Ctx -> Tm -> Val -> TC ()
check ctx (Lam _ b) (VPi ty _ c) = check (bind ctx ty) b (vinst c (VVar (lvl ctx)))
check ctx (Pair a _ b _) (VSigma ty _ c) = do
  check ctx a ty
  check ctx b (vinst c (eval (vs ctx) a))
check ctx (Let ty val b) ty' = do
  _ <- inferSort ctx ty
  let vt = eval (vs ctx) ty
  check ctx val vt
  check (define ctx vt (eval (vs ctx) val)) b ty'
check ctx (Exfalso tm) ty = check ctx tm VBot
check ctx Refl idty@(VId ty s a b) =
  if conv (lvl ctx) s a b then
    return ()
  else
    Left $ "refl failed: " ++ show (quote (lvl ctx) idty)
check ctx tm ty = do
  ty' <- infer ctx tm
  if convTypes (lvl ctx) ty' ty then
    return ()
  else
    Left $ "check failed (" ++ show tm ++ " : " ++ show (quote (lvl ctx) ty) ++ "), got " ++ show (quote (lvl ctx) ty') 

inferSort :: Ctx -> Tm -> TC Sort
inferSort ctx ty = do
  ty' <- infer ctx ty
  case ty' of
    VSort s -> return s
    _ -> Left $ "expected sort for " ++ show ty ++ " but got " ++ show (quote (lvl ctx) ty')

infer :: Ctx -> Tm -> TC Val
infer ctx (Var i) =
  if i < lvl ctx then
    return $ (ts ctx) !! i
  else
    Left $ "undefined var " ++ show i
infer ctx (Let ty val b) = do
  _ <- inferSort ctx ty
  let vt = eval (vs ctx) ty
  check ctx val vt
  infer (define ctx vt (eval (vs ctx) val)) b
infer ctx tm@(App a b _) = do
  ft <- infer ctx a
  case ft of
    VPi ty _ c -> do
      check ctx b ty
      return $ vinst c (eval (vs ctx) b)
    _ -> Left $ "expected pi in " ++ show tm ++ " but got " ++ show (quote (lvl ctx) ft)
infer ctx tm@(Proj p t) = do
  pt <- infer ctx t
  case pt of
    VSigma ty _ c ->
      case p of
        Fst -> return ty
        Snd -> return $ vinst c (vproj Fst $ eval (vs ctx) t)    
    _ -> Left $ "expected sigma in " ++ show tm ++ " but got " ++ show (quote (lvl ctx) pt)
infer ctx (Pi ty _ b) = do
  s <- inferSort ctx ty
  s' <- inferSort (bind ctx (eval (vs ctx) ty)) b
  return $ VSort (umax s s')
infer ctx (Sigma ty _ b) = do
  s <- inferSort ctx ty
  s' <- inferSort (bind ctx (eval (vs ctx) ty)) b
  return $ VSort (umax s s')
infer ctx (Id ty _ a b) = do
  _ <- inferSort ctx ty
  let vty = eval (vs ctx) ty
  check ctx a vty
  check ctx b vty
  return $ VSort Prop
infer ctx (Sort Prop) = return $ VSort (Type 0)
infer ctx (Sort (Type l)) = return $ VSort (Type (l + 1))
infer ctx Bot = return $ VSort Prop
infer ctx tm = Left $ "cannot infer " ++ show tm

typecheck :: Tm -> TC Tm
typecheck tm = do
  ty <- infer emptyCtx tm
  return $ quote (lvl emptyCtx) ty

-- testing
top :: Tm
top = Pi Bot SProp Bot

tt :: Tm
tt = Let top (Lam SProp (Var 0)) (Var 0)

-- let x : (a b : Bot) -> (a = b) = \a b. Refl; x
example :: Tm
example = Let (Pi Bot SProp $ Pi Bot SProp $ Id Bot SProp (Var 1) (Var 0)) (Lam SProp $ Lam SProp Refl) (Var 0)

-- let k : (ty : Type 0) (a b : ty) (q q' : a = b) -> q = q' = \ty a b q q'. Refl; k
example2 :: Tm
example2 =
  Let (Pi (Sort $ Type 0) SType $ Pi (Var 0) SType $ Pi (Var 1) SType $ Pi (Id (Var 2) SType (Var 1) (Var 0)) SProp $ Pi (Id (Var 3) SType (Var 2) (Var 1)) SProp $ Id ((Id (Var 4) SType (Var 3) (Var 2))) SProp (Var 1) (Var 0)) (Lam SType $ Lam SType $ Lam SType $ Lam SProp $ Lam SProp $ Refl) (Var 0)

-- let topeta : (x : Top) -> Id Top x tt = \_. Refl; topeta
example3 :: Tm
example3 = Let (Pi top SProp $ Id top SProp (Var 0) tt) (Lam SProp Refl) (Var 0)

main :: IO ()
main = do
  let e = example3
  putStrLn $ show e
  case typecheck e of
    Right ty -> do
      putStrLn $ show ty
      putStrLn $ show $ nf e
    Left err -> putStrLn $ show err