94 lines
2.2 KiB
Agda
94 lines
2.2 KiB
Agda
module Zoo4eg
|
|
|
|
id : {A : U} -> A -> A
|
|
id = \x => x -- elaborated to \{A} x. x
|
|
|
|
-- implicit arg types can be omitted
|
|
const : {A B : U} -> A -> B -> A
|
|
const = \x y => x
|
|
|
|
-- function arguments can be grouped:
|
|
group1 : {A B : U}(x y z : A) -> B -> B
|
|
group1 = \x y z b => b
|
|
|
|
group2 : {A B : U}(x y z : A) -> B -> B
|
|
group2 = \x y z b => b
|
|
|
|
-- explicit id function used for annotation as in Idris
|
|
the : (A : _) -> A -> A
|
|
the = \_ x => x
|
|
|
|
-- implicit args can be explicitly given
|
|
-- NB kovacs left off the type (different syntax), so I put a hole in there
|
|
argTest1 : _
|
|
argTest1 = const {U} {U} U
|
|
|
|
-- I've decided not to do = in the {} for now.
|
|
-- let argTest2 = const {B = U} U; -- only give B, the second implicit arg
|
|
|
|
-- again no type, this hits a lambda in infer.
|
|
-- I think we need to create two metas and make a pi of them.
|
|
insert2 : _
|
|
insert2 = (\{A} x => the A x) U -- (\{A} x => the A x) {U} U
|
|
|
|
Bool : U
|
|
Bool = (B : _) -> B -> B -> B
|
|
|
|
true : Bool
|
|
true = \B t f => t
|
|
|
|
false : Bool
|
|
false = \B t f => f
|
|
|
|
List : U -> U
|
|
List = \A => (L : _) -> (A -> L -> L) -> L -> L
|
|
|
|
nil : {A : U} -> List A
|
|
nil = \L cons nil => nil
|
|
|
|
cons : {A : U} -> A -> List A -> List A
|
|
cons = \ x xs L cons nil => cons x (xs L cons nil)
|
|
|
|
map : {A B : U} -> (A -> B) -> List A -> List B
|
|
map = \{A} {B} f xs L c n => xs L (\a => c (f a)) n
|
|
|
|
list1 : List Bool
|
|
list1 = cons true (cons false (cons true nil))
|
|
|
|
-- dependent function composition
|
|
comp : {A : U} {B : A -> U} {C : {a : A} -> B a -> U}
|
|
(f : {a : A} (b : B a) -> C b)
|
|
(g : (a : A) -> B a)
|
|
(a : A)
|
|
-> C (g a)
|
|
comp = \f g a => f (g a)
|
|
|
|
-- TODO unsolved metas in dependent function composition
|
|
-- compExample : List Bool
|
|
-- compExample = comp (cons true) (cons false) nil
|
|
|
|
Nat : U
|
|
Nat = (N : U) -> (N -> N) -> N -> N
|
|
|
|
mul : Nat -> Nat -> Nat
|
|
mul = \a b N s z => a _ (b _ s) z
|
|
|
|
ten : Nat
|
|
ten = \N s z => (s (s (s (s (s (s (s (s (s (s z))))))))))
|
|
|
|
hundred : _
|
|
hundred = mul ten ten
|
|
|
|
-- Leibniz equality
|
|
Eq : {A: U} -> A -> A -> U
|
|
Eq = \{A} x y => (P : A -> U) -> P x -> P y
|
|
|
|
refl : {A : U} {x : A} -> Eq x x
|
|
refl = \_ px => px
|
|
|
|
sym : {A x y : _} -> Eq {A} x y -> Eq y x
|
|
sym = \p => p (\y => Eq y x) refl
|
|
|
|
eqtest : Eq (mul ten ten) hundred
|
|
eqtest = refl
|