# Commits

committed c6c94aa

Change ty to return Just Term, add tyof to find the type of a typeable term, add inhabits to demonstrate a term inhabits a type, add proof that 1+1=2

# DTLC.hs

` cTy "Refl" = Forall (Star 0) (Forall (Var 0) (Const "Eq" `App` Var 1 `App` Var 0 `App` Var 0))`
` cTy _ = error "Undefined constant"`
` `
`-ty :: Term -> Term    `
`+ty :: Term -> Maybe Term    `
` ty = ty' []`
` `
`-ty' :: Ctx -> Term -> Term`
`-ty' ctx (Star n) = Star (n+1)`
`-ty' ctx (Lam t b) = `
`-    let ctx' = t : ctx in`
`-    Forall t (ty' ctx' b)`
`-ty' ctx (Forall t b) = `
`-    let ctx' = t : ctx in`
`-    let Star tn = ty' ctx t in`
`-    let Star bn = ty' ctx' b in`
`-    if tn == bn then Star tn else error "Mismatched universes"`
`-ty' ctx (Var i) = ctx !! i`
`-ty' ctx (App f a) = `
`-    let Forall t b = ty' ctx f in`
`-    let t' = ty' ctx a in`
`-    if t `eq` t' then norm (sub 0 a b) else error "Invalid argument to function"`
`-ty' ctx (Const name) = cTy name`
`+ty' :: Ctx -> Term -> Maybe Term`
`+ty' ctx (Star n) = Just \$ Star (n+1)`
`+ty' ctx (Lam t b) = do`
`+    let ctx' = t : ctx `
`+    bt <- ty' ctx' b`
`+    Just \$ Forall t bt`
`+ty' ctx (Forall t b) = do`
`+    let ctx' = t : ctx `
`+    case ty' ctx t of`
`+        Just (Star tn) -> case ty' ctx' b of`
`+            Just (Star bn) -> if tn == bn then Just \$ Star tn else Nothing`
`+            otherwise -> Nothing`
`+        otherwise -> Nothing`
`+ty' ctx (Var i) = if i < length ctx then Just \$ ctx !! i else Nothing`
`+ty' ctx (App f a) = do`
`+    ft <- ty' ctx f`
`+    case norm ft of `
`+        Forall t b -> do`
`+                t' <- ty' ctx a`
`+                if norm t `eq` norm t' then Just \$ sub 0 a b else Nothing`
`+        otherwise -> Nothing`
`+`
`+ty' ctx (Const name) = Just \$ cTy name`
`+`
`+tyof x = let Just r = ty x in r`
` `
` star = Star 0`
` idStar = Lam star (Var 0)`
` `
` p :: Term -> String`
` p term = case ty term of`
`-    Const "Nat" -> show \$ toInt \$ norm term`
`-    otherwise -> "<" ++ show (ty \$ norm term) ++ ">"`
`+    Nothing -> error "Typecheck failure"`
`+    Just (Const "Nat") -> show \$ toInt \$ norm term`
`+    otherwise -> let Just t = ty term  in "<" ++ show t ++ ">"`
` `
` toInt :: Term -> Int`
` toInt t = `
`                 `
` toNat :: Int -> Term`
` toNat 0 = Const "Zero"`
`-toNat n = App (Const "Succ") \$ toNat (n -1)`
`+toNat n = App (Const "Succ") \$ toNat (n -1)`
`+`
`+inhabits :: Term -> Term -> Bool `
`+inhabits e t = `
`+    let Just et = ty e in`
`+    let Just _ = ty t in -- error if it doesn't typecheck`
`+    norm et == norm t`
`+`
`+one = _succ `App` _zero`
`+two = _succ `App` one`
`+three = _succ `App` two`
`+`
`+onePlusOne = plus `App` (_succ `App` _zero) `App` (_succ `App` _zero) `
`+onePlusOneEqualsTwo = Const "Eq" `App` Const "Nat" `App` onePlusOne `App` two`
`+proofThatOnePlusOneEqualsTwo = Const "Refl" `App` Const "Nat" `App` two`
`+`
`+onePlusOneEqualsThree = Const "Eq" `App` Const "Nat" `App` onePlusOne `App` three`