From e3c74503ee767155cc4fa41d9a56d33f204a81bb Mon Sep 17 00:00:00 2001 From: depsterr Date: Thu, 21 Jul 2022 19:51:55 +0200 Subject: [PATCH] added let ... in ... --- README.md | 11 ++++++-- src/Check.idr | 23 +++++++++++++-- src/Convert.idr | 71 ++++++++++++++++++++--------------------------- src/Misc.idr | 41 ++++----------------------- src/Normalize.idr | 9 +++++- src/Term.idr | 16 +++++++---- src/Tests.idr | 54 +++++++++++++++++++++++++++++------ 7 files changed, 128 insertions(+), 97 deletions(-) diff --git a/README.md b/README.md index b250bf0..177bb99 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,8 @@ A dependently typed system * pi types * type of types +* let ... in ... + * Unit type * Empty type @@ -20,21 +22,26 @@ A dependently typed system # TODO -* Let ... in ... - * Parser * Fun types * Id +* Repl + * Universes +* Performence optimisation + * Memoize normalisation and conversion somehow? + * Implicit arguments * (indexed) inductive datatypes * Write down the rules (I'll not get this far) +* Compile to scheme + # References Some of the material I found helpful in groking dependent type checking: diff --git a/src/Check.idr b/src/Check.idr index b438257..bf32bdf 100644 --- a/src/Check.idr +++ b/src/Check.idr @@ -15,6 +15,14 @@ import Convert %default total +-- extend environment, used to ensure environment is always in normal form +extV : Ctx n -> Value -> PI (Ctx (S n)) +extV ctx val = whnf val >>= pure . (`Data.Vect.(::)` ctx) + +-- to extend, closure env, term +extT : Ctx m -> Ctx n -> Term n -> PI (Ctx (S m)) +extT ctx env = extV ctx . VClos env + mutual public export -- terms types expected term @@ -25,7 +33,7 @@ mutual TLam sc => case xpt of VClos env (TPi a b) => do v <- VGen <$> fresh - check (v :: trs) (VClos env a :: tys) (VClos (v :: env) b) sc + check (v :: trs) !(extT tys env a) (VClos (v :: env) b) sc _ => oops "expected pi" -- pi and sigma could be inferred /shrug @@ -33,7 +41,7 @@ mutual VType => do v <- VGen <$> fresh guardS "Pi a" =<< check trs tys VType a - check (v :: trs) (VClos trs a :: tys) VType b + check (v :: trs) !(extT tys trs a) VType b _ => oops "expected type" TSigma a b => case xpt of @@ -49,6 +57,10 @@ mutual check trs tys (VClos env b `VApp` VClos trs x) y _ => oops "expected sigma" + TLet ty tr tri => do + guardS "let" =<< check trs tys (VClos trs ty) tr + check !(extT trs trs tr) !(extT tys trs ty) xpt tri + _ => convert xpt =<< infer trs tys tr -- terms types term @@ -59,7 +71,8 @@ mutual \case VClos env (TPi a b) => do guardS "app x" =<< check trs tys (VClos env a) x - pure (VClos (VClos trs x :: env) b) + tr <- whnf (VClos trs x) + pure (VClos (tr :: env) b) _ => oops "expected infer pi" @@ -99,6 +112,10 @@ mutual pure (VClos trs (TPi (TSigma a b) (weakTr c `TApp` TVar 0))) + infer trs tys (TLet ty tr tri) = do + guardS "let infer" =<< check trs tys (VClos trs ty) tr + infer !(extT trs trs tr) !(extT tys trs ty) tri + infer trs tys x = oops ("cannot infer type" ++ show x) public export diff --git a/src/Convert.idr b/src/Convert.idr index 07ce672..cbe3013 100644 --- a/src/Convert.idr +++ b/src/Convert.idr @@ -14,8 +14,6 @@ import Data.Vect %default total -{- TODO: I should throw eval, eval, convert into a helper sometime -} - public export convert : Value -> Value -> PI Bool convert u1 u2 = do @@ -45,54 +43,45 @@ convert u1 u2 = do (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do v <- VGen <$> fresh - guard =<< convert (VClos env1 a1) (VClos env2 a2) + + s1 <- case headM env1 of + Nothing => pure "" + Just x => pure (show x) + + s2 <- case headM env2 of + Nothing => pure "" + Just x => pure (show x) + + guardS (s1 ++ " | " ++ s2) =<< convert (VClos env1 a1) (VClos env2 a2) convert (VClos (v :: env1) b1) (VClos (v :: env2) b2) (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do - c1' <- eval env1 c1 - c2' <- eval env2 c2 - guard =<< convert c1' c2' - st1' <- eval env1 st1 - st2' <- eval env2 st2 - convert st1' st2' + termGuard env1 env2 c1 c2 + termConv env1 env2 st1 st2 - (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => do - c1' <- eval env1 c1 - c2' <- eval env2 c2 - convert c1' c2' + (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => termConv env1 env2 c1 c2 - -- lmao (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do - c1' <- eval env1 c1 - c2' <- eval env2 c2 - guard =<< convert c1' c2' - z1' <- eval env1 z1 - z2' <- eval env2 z2 - guard =<< convert z1' z2' - s1' <- eval env1 s1 - s2' <- eval env2 s2 - convert s1' s2' + termGuard env1 env2 c1 c2 + termGuard env1 env2 z1 z2 + termConv env1 env2 s1 s2 (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do - a1' <- eval env1 a1 - a2' <- eval env2 a2 - guard =<< convert a1' a2' - b1' <- eval env1 b1 - b2' <- eval env2 b2 - convert b1' b2' + termGuard env1 env2 a1 a2 + termConv env1 env2 b1 b2 (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do - a1' <- eval env1 a1 - a2' <- eval env2 a2 - guard =<< convert a1' a2' - b1' <- eval env1 b1 - b2' <- eval env2 b2 - guard =<< convert b1' b2' - c1' <- eval env1 c1 - c2' <- eval env2 c2 - guard =<< convert c1' c2' - f1' <- eval env1 f1 - f2' <- eval env2 f2 - convert f1' f2' + termGuard env1 env2 a1 a2 + termGuard env1 env2 b1 b2 + termGuard env1 env2 c1 c2 + termConv env1 env2 f1 f2 _ => pure False + where + termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool + termConv env1 env2 a1 a2 = do + a1' <- eval env1 a1 + a2' <- eval env2 a2 + convert a1' a2' + termGuard : Ctx n -> Ctx m -> Term n -> Term m -> PI () + termGuard env1 env2 a1 a2 = guardS "termGuard" =<< termConv env1 env2 a1 a2 diff --git a/src/Misc.idr b/src/Misc.idr index 9eb9b59..1d2e4af 100644 --- a/src/Misc.idr +++ b/src/Misc.idr @@ -5,6 +5,7 @@ import Control.Monad.Identity import Control.Monad.Either import Data.Nat +import Data.Vect %default total @@ -45,41 +46,9 @@ fresh = do public export logS : String -> PI () -logS = tell . (:: []) +logS = tell . (`Prelude.(::)` []) public export -lteTransp : LTE a b -> a = c -> b = d -> LTE c d -lteTransp p Refl Refl = p - -public export -lteS : {n : _} -> LTE n (S n) -lteS {n = Z} = LTEZero -lteS {n = S n} = LTESucc lteS - -public export -lteSplit : {m : _} -> LTE n m -> Either (n = m) (LT n m) -lteSplit {m = Z} LTEZero = Left Refl -lteSplit {m = S m} LTEZero = Right (LTESucc LTEZero) -lteSplit {m = S m} (LTESucc p) = case lteSplit p of - Left p2 => Left (cong S p2) - Right p2 => Right (LTESucc p2) - -public export -minusLte : {m,n : _} -> LTE (minus n (S m)) n -minusLte {n = Z} = LTEZero -minusLte {n = S n} {m = Z} = rewrite minusZeroRight n in lteSuccRight reflexive -minusLte {n = S n} {m = S m} = lteSuccRight (minusLte {n = n} {m = m}) - -public export -prevEq : (i, j : Nat) -> S i = S j -> i = j -prevEq Z Z Refl = Refl -prevEq (S i) (S _) Refl = Refl - -public export -natEqDecid : (n, m : Nat) -> Either (Not (n = m)) (n = m) -natEqDecid Z Z = Right Refl -natEqDecid (S _) Z = Left absurd -natEqDecid Z (S _) = Left absurd -natEqDecid (S n) (S m) = case natEqDecid n m of - Right p => Right (cong S p) - Left p => Left (p . prevEq n m) +headM : Vect n a -> Maybe a +headM [] = Nothing +headM (x :: _) = Just x diff --git a/src/Normalize.idr b/src/Normalize.idr index ee3505b..f4c3cf4 100644 --- a/src/Normalize.idr +++ b/src/Normalize.idr @@ -15,7 +15,6 @@ import Data.Vect mutual public export - -- no computational rule for ⊥ app : Value -> Value -> PI Value app (VClos env (TLam sc)) x = eval (x :: env) sc @@ -74,6 +73,10 @@ mutual b' <- eval env b pure (VPair a' b') + eval env (TLet ty tr tri) = do + tr' <- eval env tr + eval (tr' :: env) tri + eval env tr = pure (VClos env tr) public export @@ -82,5 +85,9 @@ whnf (VApp f x) = do f' <- whnf f x' <- whnf x app f' x' +whnf (VPair a b) = do + a' <- whnf a + b' <- whnf b + pure (VPair a' b') whnf (VClos env tr) = eval env tr whnf v = pure v diff --git a/src/Term.idr b/src/Term.idr index c128b1d..18e665c 100644 --- a/src/Term.idr +++ b/src/Term.idr @@ -30,6 +30,8 @@ data Term : (_ : Index) -> Type where TPair : Term n -> Term n -> Term n -- Sum constructor _,_ TSigInd : Term n -> Term n -> Term n -> Term n -> Term n -- A B C f : (x : Σ _ : A , B _) → C x + TLet : Term n -> Term n -> Term (S n) -> Term n -- let _ : #0 := #1 in #2 + TLam : Term (S n) -> Term n -- Lambda abstraction (λ _ . Scope) TPi : Term n -> Term (S n) -> Term n -- Pi type (∏ _ : A . B _ ) @@ -54,15 +56,16 @@ Show (Term n) where show (TSuc n) = "suc (" ++ show n ++ ")" show (TNatInd c z s) = "ℕ-ind (" ++ show c ++ ") (" ++ show z ++ ") (" ++ show s ++ ")" - show (TSigma a b) = "TSigma (" ++ show a ++ ") (" ++ show b ++ ")" - show (TPair a b) = "TPair (" ++ show a ++ ") (" ++ show b ++ ")" + show (TSigma a b) = "Σ (" ++ show a ++ ") (" ++ show b ++ ")" + show (TPair a b) = "Pair (" ++ show a ++ ") (" ++ show b ++ ")" show (TSigInd a b c f) = "Σ-ind (" ++ show a ++ ") (" ++ show b ++ ") (" ++ show c ++ ") (" ++ show f ++ ")" + show (TLet ty tr itr) = "let : (" ++ show ty ++ ") := (" ++ show tr ++ ") in (" ++ show itr ++ ")" - show (TLam sc) = "TLam (" ++ show sc ++ ")" - show (TPi ty sc) = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")" + show (TLam sc) = "λ (" ++ show sc ++ ")" + show (TPi ty sc) = "Π (" ++ show ty ++ ") (" ++ show sc ++ ")" - show (TApp f x) = "TApp (" ++ show f ++ ") (" ++ show x ++ ")" - show (TVar i) = "TVar " ++ show i + show (TApp f x) = "(" ++ show f ++ ") TApp (" ++ show x ++ ")" + show (TVar i) = "Var " ++ show i public export weakTr : Term n -> Term (S n) @@ -82,6 +85,7 @@ weakTr = go 0 go n (TSigma a b) = TSigma (go n a) (go n b) go n (TPair a b) = TPair (go n a) (go n b) go n (TSigInd a b c f) = TSigInd (go n a) (go n b) (go n c) (go n f) + go n (TLet ty tr itr) = TLet (go n ty) (go n tr) (go (FS n) itr) go n (TLam sc) = TLam (go (FS n) sc) go n (TPi ty sc) = TPi (go n ty) (go (FS n) sc) go n (TApp f x) = TApp (go n f) (go n x) diff --git a/src/Tests.idr b/src/Tests.idr index 37abb8e..8b415d3 100644 --- a/src/Tests.idr +++ b/src/Tests.idr @@ -43,12 +43,18 @@ addition = TNatInd (TLam (TPi TNat TNat)) (TLam (TVar 0)) (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TVar 1 `TApp` TVar 0))))) -addition_type : Either String (Bool, List String) -addition_type = typecheck addition (TPi TNat (TPi TNat TNat)) +additionty : Term 0 +additionty = TPi TNat (TPi TNat TNat) + +additionty_test : Either String (Bool, List String) +additionty_test = typecheck additionty TType + +addition_test : Either String (Bool, List String) +addition_test = typecheck addition additionty {- 2 + 1 = 3 -} -add_test : Either String (Bool, List String) -add_test = resolve action +addition_compute_test : Either String (Bool, List String) +addition_compute_test = resolve action where action : PI Bool action = do @@ -61,12 +67,18 @@ multi = TNatInd (TLam (TPi TNat TNat)) (TLam TZero) (TLam {-n-} (TLam {-n*-} (TLam {-m-} (weakTr3 addition `TApp` TVar 0 `TApp` (TVar 1 `TApp` TVar 0))))) -multi_type : Either String (Bool, List String) -multi_type = typecheck multi (TPi TNat (TPi TNat TNat)) +multity : Term 0 +multity = TPi TNat (TPi TNat TNat) + +multity_test : Either String (Bool, List String) +multity_test = typecheck multity TType + +multi_test : Either String (Bool, List String) +multi_test = typecheck multi multity {- 2 * 3 = 6 -} -multi_test : Either String (Bool, List String) -multi_test = resolve action +multi_compute_test : Either String (Bool, List String) +multi_compute_test = resolve action where action : PI Bool action = do @@ -92,6 +104,9 @@ pr1 = TLam {- A : Type -} (TLam {- B : A → Type -} (TSigInd (TVar 1) (TVar 0) (TLam {-ΣAB-} (TVar 2)) (TLam (TLam (TVar 1))))) +pr1ty_test : Either String (Bool, List String) +pr1ty_test = typecheck pr1ty TType + pr1_test : Either String (Bool, List String) pr1_test = typecheck pr1 pr1ty @@ -115,3 +130,26 @@ pr2ty_test = typecheck pr2ty TType pr2_test : Either String (Bool, List String) pr2_test = typecheck pr2 pr2ty + +pr2ty_let : Term 0 +pr2ty_let = TLet pr1ty pr1 {- pr1 : pr1ty -} + (TPi TType {- A : Type -} + (TPi (TPi (TVar 0) TType) {- B : A → Type -} + (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -} + (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0))))) + +pr2_let : Term 0 +pr2_let = TLet pr1ty pr1 {- pr1 : pr1ty -} + (TLam {- A : Type -} + (TLam {- B : A → Type -} + (TSigInd (TVar 1) + (TVar 0) + (TLam {-ΣAB-} + (TVar 1 `TApp` (TVar 3 `TApp` TVar 2 `TApp` TVar 1 `TApp` TVar 0))) + (TLam (TLam (TVar 0)))))) + +pr2ty_let_test : Either String (Bool, List String) +pr2ty_let_test = typecheck pr2ty_let TType + +pr2_let_test : Either String (Bool, List String) +pr2_let_test = typecheck pr2_let pr2ty_let