module Idris09 import Data.Vect -- Show definition of Void, Not. doubleNeg : a -> Not (Not a) doubleNeg x = \f => f x -- deMorgan1, deMorgan2 deMorgan1 : Not (Either a b) -> (Not a, Not b) deMorgan1 f = ((\x => f (Left x)) , (\x => f (Right x))) -- deMorgan2 : Not (a , b) -> Either (Not a) (Not b) -- deMorgan2 x = ?deMorgan2_rhs ------------------------------------------------------------ -- natFold. Dependent version. (replicateV, expand type) -- lists. natFold : a -> (a -> a) -> Nat -> a natFold z s Z = z natFold z s (S k) = s (natFold z s k) -- replicate : (n : Nat) -> a -> Vect n a -- Doesn't work. -- replicate n x = natFold [] (x::) n -- Dependent version of natFold? natFold' : (A : Type) -> A -> (A -> A) -> Nat -> A natFold' _ z s Z = z natFold' _ z s (S k) = s (natFold' _ z s k) natFoldDep : (P : Nat -> Type) -> P 0 -> ((m : Nat) -> P m -> P (S m)) -> (n : Nat) -> P n natFoldDep _ z s Z = z natFoldDep _ z s (S k) = s k (natFoldDep _ z s k) -- Holy #\$%& this is just induction! -- Induction is just a dependently typed fold. replicate : (n : Nat) -> a -> Vect n a replicate n x = natFoldDep (\n => Vect n a) [] ((\_ => (x ::))) n -------------------------------------------------- listFold : (A : Type) -> (B : Type) -> B -> (A -> B -> B) -> List A -> B listFold A B n c [] = n listFold A B n c (x :: xs) = c x (listFold _ _ n c xs) total listInd : (A : Type) -> (P : List A -> Type) -> P [] -> ((x : A) -> (ys : List A) -> P ys -> P (x :: ys)) -> (xs : List A) -> P xs listInd _ _ n c [] = n listInd _ _ n c (x :: xs) = c x xs (listInd _ _ n c xs) -------------------------------------------------- -- STLC. infixr 5 :->: data Ty : Type where NAT : Ty (:->:) : Ty -> Ty -> Ty data Ctx : Nat -> Type where Nil : Ctx 0 Snoc : Ctx n -> Ty -> Ctx (S n) lookup : Fin n -> Ctx n -> Ty lookup FZ (Snoc g x) = x lookup (FS i) (Snoc g _) = lookup i g -- de Bruijn ("de Brown") indices: -- use natural numbers to represent variables. -- e.g. -- -- \x.\y.x (\z. (x y) z) -- -- will be represented as -- -- λ.λ.1 (λ. (2 1) 0) -- -- The variable i refers to the ith enclosing lambda. -- How to represent only valid variable indices? -- One idea: -- Index n represents numbers 0..n-1. Index : Nat -> Type Index n = (i ** LT i n) -- This works but is somewhat unwieldy. -- Better: use 'Fin'. -- data Fin : Nat -> Type where -- FZ : Fin (S k) -- FS : Fin k -> Fin (S k) -- There are exactly n different values -- of type Fin n. e.g. -- -- FZ, FS FZ, FS (FS FZ) : Fin 3. -- a : Term Γ τ if and only if -- Γ ⊢ a : τ. -- -- For each kind of term, we encode its -- STLC typing rule in the Idris type -- of its constructor. data Term : Ctx n -> Ty -> Type where Lit : Nat -> Term g NAT Plus : Term g NAT -> Term g NAT -> Term g NAT Var : (i : Fin n) -> Term g (lookup i g) App : Term g (s :->: t) -> Term g s -> Term g t Lam : (s : Ty) -> Term (Snoc g s) t -> Term g (s :->: t) ex1 : Term Nil NAT ex1 = Lit 3 ex2 : Term Nil (NAT :->: NAT) ex2 = Lam NAT (Plus (Lit 2) (Var FZ)) -- \f. (\x. (f (x x))) (\x. (f (x x))) -- ex3 : Term Nil ((NAT :->: NAT) :->: NAT) -- ex3 = Lam (NAT :->: NAT) (App (Lam NAT (App (Var (FS FZ)) (App (Var FZ) (Var FZ)))) (Lam NAT (App (Var (FS FZ)) (App (Var FZ) (Var FZ))))) -- doesn't type check, whew. -- Next, an STLC interpreter! -- First, a function to interpret STLC types in Idris: interpTy : Ty -> Type interpTy NAT = Nat interpTy (s :->: t) = interpTy s -> interpTy t -- interp : Term Nil t -> interpTy t -- interp (Lit k) = k -- interp (Plus x y) = interp x + interp y -- interp (Var FZ) impossible -- interp (Var (FS _)) impossible -- interp (App x y) = (interp x) (interp y) -- interp (Lam s x) = ?interp_rhs_5 -- Need to generalize to interpret terms -- with a non-empty context. Hence we also -- need to keep track of values of free -- variables. data Env : Ctx n -> Type where ENil : Env Nil ESnoc : Env g -> interpTy t -> Env (Snoc g t) elookup : (i : Fin n) -> {g : Ctx n} -> Env g -> interpTy (lookup i g) elookup FZ (ESnoc e x) = x elookup (FS n) (ESnoc e _) = elookup n e interp' : Env g -> Term g t -> interpTy t interp' e (Lit k) = k interp' e (Plus x y) = interp' e x + interp' e y interp' e (Var i) = elookup i e interp' e (App x y) = (interp' e x) (interp' e y) interp' e (Lam s b) = \x => interp' (ESnoc e x) b interp : Term Nil t -> interpTy t interp x = interp' ENil x