Kind2/example/example.kind2

// Bool
// ----

Bool : Type
True : Bool
False : Bool

Bool.not (a: Bool) : Bool
Bool.not True  = False
Bool.not False = True

Bool.and (a: Bool) (b: Bool) : Bool
Bool.and True  True  = True
Bool.and True  False = False
Bool.and False True  = False
Bool.and False False = False

Bool.not_not_theorem (a: Bool) : (Equal Bool a (Bool.not (Bool.not a)))
Bool.not_not_theorem True  = (Refl Bool True)
Bool.not_not_theorem False = (Refl Bool False)

// Nat
// ---

Nat : Type
Zero : Nat
Succ (pred: Nat) : Nat

Nat.double (x: Nat) : Nat
Nat.double (Succ x) = (Succ (Succ (Nat.double x)))
Nat.double (Zero)   = (Zero)

Nat.add (a: Nat) (b: Nat) : Nat
Nat.add (Succ a) b = (Succ (Nat.add a b))
Nat.add Zero     b = b

Nat.comm.a (a: Nat) : (Equal Nat a (Nat.add a Zero))
Nat.comm.a Zero     = Refl
Nat.comm.a (Succ a) = (Equal.apply @x(Succ x) (Nat.comm.a a))

Nat.comm.b (a: Nat) (b: Nat): (Equal Nat (Nat.add a (Succ b)) (Succ (Nat.add a b)))
Nat.comm.b Zero     b = Refl
Nat.comm.b (Succ a) b = (Equal.apply @x(Succ x) (Nat.comm.b a b))

Nat.comm (a: Nat) (b: Nat) : (Equal Nat (Nat.add a b) (Nat.add b a))
Nat.comm Zero     b = (Nat.comm.a b)
Nat.comm (Succ a) b =
  let e0 = (Equal.apply @x(Succ x) (Nat.comm a b))
  let e1 = (Equal.mirror (Nat.comm.b b a))
  (Equal.chain e0 e1)
  
// List
// ----

List (a: Type) : Type
Nil <a> : (List a)
Cons <a> (x: a) (xs: (List a)) : (List a)

List.negate (xs: (List Bool)) : (List Bool)
List.negate (Cons Bool x xs) = (Cons Bool (Bool.not x) (List.negate xs))
List.negate (Nil Bool)       = (Nil Bool)

List.tail <a> (xs: (List a)) : (List a)
List.tail a (Cons t x xs) = xs

List.map <a> <b> (x: (List a)) (f: (x: a) b) : (List b)
List.map a b (Nil t)       f = (Nil b)
List.map a b (Cons t x xs) f = (Cons b (f x) (List.map a b xs f))

List.concat <a> (xs: (List a)) (ys: (List a)) : (List a)
List.concat a (Cons u x xs) ys = (Cons u x (List.concat a xs ys))
List.concat a (Nil u)       ys = ys

List.flatten <a> (xs: (List (List a))) : (List a)
List.flatten a (Cons u x xs) = (List.concat x (List.flatten xs))
List.flatten a (Nil u)       = Nil

List.bind <a: Type> <b: Type> (xs: (List a)) (f: a -> (List b)) : (List b)
List.bind a b xs f = (List.flatten b (List.map xs f))

// Equal
// -----

Equal <t> (a: t) (b: t) : Type
Refl <t> <a: t> : (Equal t a a)

Equal.mirror <t> <a: t> <b: t> (e: (Equal t a b)) : (Equal t b a)
Equal.mirror t a b (Refl u k) = (Refl u k)

Equal.apply <t> <u> <a: t> <b: t> (f: t -> t) (e: (Equal t a b)) : (Equal t (f a) (f b))
Equal.apply t u a b f (Refl v k) = (Refl v (f k))

Equal.rewrite <t> (a: t) (b: t) (e: (Equal t a b)) (p: t -> Type) (x: (p a)) : (p b)
Equal.rewrite t a b (Refl u k) p x = {x :: (p k)}

Equal.chain <t> <a: t> <b: t> <c: t> (e0: (Equal t a b)) (e1: (Equal t b c)) : (Equal t a c)
Equal.chain t a b c e0 (Refl u x) = {e0 :: (Equal t a x)}

// Monad
// -----

Monad (f: Type -> Type) : Type
Monad.new (f: Type -> Type)
  (pure: (a: Type) (x: a) (Monad (f a)))
  (bind: (a: Type) (b: Type) (x: (Monad a)) (y: a -> (Monad b)) (Monad b))
  : (Monad f)

// Examples
// --------

// Generates combinations!
// - Run   with : `kind2 run   example.kind2`
// - Check with : `kind2 check example.kind2
Main : (List U60) {
  (List.bind (Cons #1 (Cons #2 (Cons #3 Nil))) @x
  (List.bind (Cons #10 (Cons #20 (Cons #30 Nil))) @y
  (List.bind (Cons #100 (Cons #200 (Cons #300 Nil))) @z
  (Cons (+ x (+ y z)) Nil))))
}