Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Error with idiom brackets in equality type
module Lambda
%default total
infixr 8 ==>
data T : Type where
U : T
NAT : T
(*) : T -> T -> T
(+) : T -> T -> T
(==>) : T -> T -> T
el : T -> Type
el U = ()
el NAT = Nat
el (t1 * t2) = (el t1, el t2)
el (t1 + t2) = Either (el t1) (el t2)
el (t1 ==> t2) = el t1 -> el t2
Context : (n : Nat) -> Type
Context n = Vect n T
data Term : (n : Nat) -> Context n -> T -> Type where
Var : (i : Fin n) -> Term n g (index i g)
Lam : Term (S n) (t :: g) t' -> Term n g (t ==> t')
App : (Term n g (t1 ==> t2)) -> Term n g t1 -> Term n g t2
Unit : Term n g U
Zero : Term n g NAT
Succ : Term n g NAT -> Term n g NAT
NatRec : Term n g NAT -> Term n g t -> (Term n g (NAT ==> t ==> t)) -> Term n g t
{-
Pair : Term n g t1 -> Term n g t2 -> Term n g (t1 * t2)
Fst : Term n g (t1 * t2) -> Term n g t1
Snd : Term n g (t1 * t2) -> Term n g t2
Inl : Term n g t1 -> Term n g (t1 + t2)
Inr : Term n g t2 -> Term n g (t1 + t2)
Case : Term n g (t1 + t2) -> Term n g (t1 ==> tr) -> Term n g (t2 ==> tr) -> Term n g tr
-}
data Stack : Context n -> Type where
Nil : Stack []
(::) : {n : Nat} -> {g : Context n} ->
(el t) -> Stack g -> Stack (t::g)
val : {n : Nat} -> {g : Context n} ->
(i : Fin n) -> Stack g -> el (index i g)
val fZ (v :: vs) = v
val (fS i) (v :: vs) = val i vs
interp : Term n g t -> Stack g -> el t
interp (Var i) s = val i s
interp {t=t1==>t2} (Lam b) s = \x : el t1 => interp b (x :: s)
interp (App e1 e2) s = (interp e1 s) (interp e2 s)
interp Unit s = ()
interp Zero _ = Z
interp (Succ n) s = S (interp n s)
interp (NatRec n base step) s = natrec (interp n s) (interp base s) (interp step s)
where natrec : Nat -> a -> (Nat -> a -> a) -> a
natrec Z base _ = base
natrec (S n') base step = step n' (natrec n' base step)
{-
interp (Pair e1 e2) s = (interp e1 s, interp e2 s)
interp (Fst e) s = fst (interp e s)
interp (Snd e) s = snd (interp e s)
interp (Inl e) s = Left (interp e s)
interp (Inr e) s = Right (interp e s)
interp (Case e l r) s =
case interp e s of
Left x => interp l s x
Right y => interp r s y
-}
idNat : Term 0 [] (NAT ==> NAT)
idNat = Lam (Var 0)
plus : Term 0 [] (NAT ==> NAT ==> NAT)
plus = Lam (Lam (NatRec (Var 1) (Var 0) (Lam (Lam (Succ (Var 0))))))
five : Term 0 [] NAT
five = App (App plus (Succ (Succ Zero))) (Succ (Succ (Succ Zero)))
---------------------
dsl stlc
lambda = Lam
variable = Var
index_first = fZ
index_next = fS
-- nice!
idNat' : Term 0 [] (NAT ==> NAT)
idNat' = stlc (\x => x)
-- nice!
plus' : Term 0 [] (NAT ==> NAT ==> NAT)
plus' = stlc (\n, m => NatRec n m (\x, y => Succ y))
-- still ugly...
five' : Term 0 [] NAT
five' = App (App plus' (Succ (Succ Zero))) (Succ (Succ (Succ Zero)))
-- NB: this is <*>, not fmap
(<$>) : Term n g (t1 ==> t2) -> Term n g t1 -> Term n g t2
(<$>) e1 e2 = App e1 e2
pure : Term n g t -> Term n g t
pure x = x
-- much better!
five'' : Term 0 [] NAT
five'' = [| plus' (Succ (Succ Zero)) (Succ (Succ (Succ Zero))) |]
-- Nat syntax
%assert_total
fromInteger : Integer -> Term n g NAT
fromInteger n = if n > 0 then Succ (fromInteger (n - 1)) else Zero
five''' : Term 0 [] NAT
five''' = [| plus' 2 3 |]
------------------
-- Provisional definitions and tactic proofs
-----------------
fromNat : Nat -> Term n g NAT
fromNat Z = Zero
fromNat (S n) = Succ (fromNat n)
plusComm : (n, m : Nat) -> (interp [| plus' (fromNat n) (fromNat m) |] []) = (interp [| plus' (fromNat m) (fromNat n) |] [])
plusComm Z m = ?p
plusComm (S n) m = ?q
*Lambda> :r
Type checking ./Lambda.idr
Lambda.idr:140:INTERNAL ERROR: "Something's gone wrong. Did you miss a semi-colon somewhere?"
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/edwinb/Idris-dev/issues
*Lambda>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.