Add example from youtube, allow unicode type names

playground/samples/Combinatory.newt

@@ -0,0 +1,102 @@
+module Combinatory
+
+-- "A correct-by-construction conversion from lambda calculus to combinatory logic", Wouter Swierstra
+
+-- This does not fully typecheck in newt yet, but is adopted from a working Idris file. It
+-- seems to do a good job exposing bugs.
+
+data Unit : U where
+  MkUnit : Unit
+
+infixr 7 _::_
+data List : U -> U where
+  Nil : {A : U} -> List A
+  _::_ : {A : U} -> A -> List A -> List A
+
+-- prj/menagerie/papers/combinatory
+
+infixr 6 _~>_
+data Type : U where
+  ι : Type
+  _~>_ : Type -> Type -> Type
+
+A : U
+A = Unit
+
+Val : Type -> U
+Val ι = A
+Val (x ~> y) = Val x -> Val y
+
+Ctx : U
+Ctx = List Type
+
+data Ref : Type -> Ctx -> U where
+  Here : {σ : Type} {Γ : Ctx} -> Ref σ (σ :: Γ)
+  There : {σ τ : Type} {Γ : Ctx} -> Ref σ Γ -> Ref σ (τ :: Γ)
+
+data Term : Ctx -> Type -> U where
+  App : {Γ : Ctx} {σ τ : Type} -> Term Γ (σ ~> τ) -> Term Γ σ -> Term Γ τ
+  Lam : {Γ : Ctx} {σ τ : Type} -> Term (σ :: Γ) τ -> Term Γ (σ ~> τ)
+  Var : {Γ : Ctx} {σ : Type} -> Ref σ Γ → Term Γ σ
+
+-- FIXME, I wasn't getting an error when I had Nil shadowing Nil
+infixr 7 _:::_
+data Env : Ctx -> U where
+  ENil : Env Nil
+  _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
+
+-- TODO there is a problem here with coverage checking
+-- I suspect something is being split before it's ready
+
+-- lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
+-- lookup Here (x ::: y) = x
+-- lookup (There i) (x ::: env) = lookup i env
+
+lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ
+lookup2 (x ::: y) Here = x
+lookup2 (x ::: env) (There i) = lookup2 env i
+
+-- TODO MixFix - this was ⟦_⟧
+eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
+-- there was a unification error in direct application
+eval (App t u) env = (eval t env) (eval u env)
+eval (Lam t) env = \ x => eval t (x ::: env)
+eval (Var i) env = lookup2 env i
+
+data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
+  S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
+  K : {Γ : Ctx} {σ τ : Type} → Comb Γ (σ ~> (τ ~> σ)) (\ env => \ x y => x)
+  I : {Γ : Ctx} {σ : Type} → Comb Γ (σ ~> σ) (\ env => \ x => x)
+  B : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => f (g x))
+  C : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> τ ~> (σ ~> τ')) (\ env => \ f g x => (f x) g)
+  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup2 env i)
+  CApp : {Γ : Ctx} {σ τ : Type} {f : _} {x : _} → Comb Γ (σ ~> τ) f → Comb Γ σ x → Comb Γ τ (\ env => (f env) (x env))
+
+sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
+  Comb Γ (σ ~> τ ~> ρ) f →
+  Comb Γ (σ ~> τ) x →
+  Comb Γ (σ ~> ρ) (\ env y => (f env y) (x env y))
+sapp (CApp K t) I = t
+sapp (CApp K t) (CApp K u) = CApp K (CApp t u)
+-- was out of pattern because of unexpanded lets.
+sapp (CApp K t) u = CApp (CApp B t) u
+-- TODO unsolved meta, out of pattern fragment
+sapp t (CApp K u) = ? -- CApp (CApp C t) u
+-- TODO unsolved meta, out of pattern fragment
+sapp t u = ? -- CApp (CApp S t) u
+
+abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env))
+abs S = CApp K S
+abs K = CApp K K
+abs I = CApp K I
+abs B = CApp K B
+abs C = CApp K C
+abs (CApp t u) = sapp (abs t) (abs u)
+-- lookup2 was getting stuck, needed to bounce the types in a rewritten env.
+abs (CVar Here) = I
+abs (CVar (There i)) = CApp K (CVar i)
+
+translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ (eval tm)
+translate (App t u) = CApp (translate t) (translate u)
+translate (Lam t) = abs (translate t)
+translate (Var i) = CVar i

playground/samples/DSL.newt

@@ -0,0 +1,120 @@
+module DSL
+
+-- https://www.youtube.com/watch?v=sFyy9sssK50
+
+data ℕ : U where
+  Z : ℕ
+  S : ℕ → ℕ
+
+infixl 7 _+_
+infixl 8 _*_
+
+_+_ : ℕ → ℕ → ℕ
+Z + m = m
+(S k) + m = S (k + m)
+
+_*_ : ℕ → ℕ → ℕ
+Z * m = Z
+(S k) * m = m + k * m
+
+infixr 4 _::_
+data Vec : U → ℕ → U where
+  Nil : {a} → Vec a Z
+  _::_ : {a k} → a → Vec a k → Vec a (S k)
+
+infixl 5 _++_
+_++_ : {a n m} → Vec a n → Vec a m → Vec a (n + m)
+Nil ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+map : {a b n} → (a → b) → Vec a n → Vec b n
+map f Nil = Nil
+map f (x :: xs) = f x :: map f xs
+
+data E : U where
+  Zero : E
+  One : E
+  Add : E → E → E
+  Mul : E → E → E
+
+two : E
+two = Add One One
+
+four : E
+four = Mul two two
+
+card : E → ℕ
+card Zero = Z
+card One = S Z
+card (Add x y) = card x + card y
+card (Mul x y) = card x * card y
+
+data Empty : U where
+
+data Unit : U where
+  -- unit accepted but case building thinks its a var
+  unit : Unit
+
+data Either : U -> U -> U where
+  Left : {A B} → A → Either A B
+  Right : {A B} → B → Either A B
+
+infixr 4 _,_
+data Both : U → U → U where
+  _,_ : {A B} → A → B → Both A B
+
+typ : E → U
+typ Zero = Empty
+typ One = Unit
+typ (Add x y) = Either (typ x) (typ y)
+typ (Mul x y) = Both (typ x) (typ y)
+
+Bool : U
+Bool = typ two
+
+false : Bool
+false = Left unit
+
+true : Bool
+true = Right unit
+
+BothBoolBool : U
+BothBoolBool = typ four
+
+ex1 : BothBoolBool
+ex1 = (false, true)
+
+enumAdd : {a b m n} → Vec a m → Vec b n → Vec (Either a b) (m + n)
+enumAdd xs ys = map Left xs ++ map Right ys
+
+-- for this I followed the shape of _*_, the lecture was slightly different
+enumMul : {a b m n} → Vec a m → Vec b n → Vec (Both a b) (m * n)
+enumMul Nil ys = Nil
+enumMul (x :: xs) ys = map (_,_ x) ys ++ enumMul xs ys
+
+enumerate : (t : E) → Vec (typ t) (card t)
+enumerate Zero = Nil
+enumerate One = unit :: Nil
+enumerate (Add x y) = enumAdd (enumerate x) (enumerate y)
+enumerate (Mul x y) = enumMul (enumerate x) (enumerate y)
+
+test2 : Vec (typ two) (card two)
+test2 = enumerate two
+
+test4 : Vec (typ four) (card four)
+test4 = enumerate four
+
+-- TODO I need to add #eval, like Lean
+-- #eval enumerate two
+
+-- for now, I'll define ≡ to check
+
+infixl 2 _≡_
+data _≡_ : {A} → A → A → U where
+  Refl : {A} {a : A} → a ≡ a
+
+test2' : test2 ≡ false :: true :: Nil
+test2' = Refl
+
+test4' : test4 ≡ (false, false) :: (false, true) :: (true, false) :: (true, true) :: Nil
+test4' = Refl