goal.txt

system zero - a total dependently-typed functional programming language

bool : data.
true : bool.
false : bool.
if : bool -> forall (r : data) -> r -> r -> r.

bool = forall (r : data) -> r -> r -> r.
true r x _ = x.
false r _ y = y.
if b = b.

and : bool -> bool -> bool.
and x y = if x bool y false.

or : bool -> bool -> bool.
or x y = if x bool true y.

xor : bool -> bool -> bool.
xor x y = if x bool (not y) y.

-- normalize identity on int
(forall (a : data) -> (x : a) -> x) int 1

(forall (int : data) -> (x : int) -> x) 1
((x : int) -> x) 1

((1 : int) -> 1)
1

-- try again?

what is the type of data? of codata? if they are different types?

-- helpful things?
id : forall (a : data) -> a -> a.
id = \(a : data) -> \(va : a) -> va.
id (a : data) (va : a) = va.
id (a : data) (va : a) : a = va.
id (a : data) (va : a) -> a = va.
id a va = va.

-- types to implement, in rough order of priority?
bool : data.
nat : data.
list a : data -> data.
stream a : data -> codata.
tuple n : nat -> data.
vec n a : nat -> data -> data.

algebra?
f-algebra
f-coalgebra

how to convert algebraic data types into f-algebra and f-coalgebra?

strictly positive

recursion
corecursion
structure of codata (http://www.tac-tics.net/blog/data-vs-codata)

http://lambda-the-ultimate.org/node/4373
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.46.5169&rep=rep1&type=pdf
http://www.cs.nott.ac.uk/~psztxa/talks/types04.pdf
https://brianmckenna.org/blog/evenodd_agda_idris_haskell_scala
http://blog.sigfpe.com/2007/07/data-and-codata.html

-- the below types may be useful
forall a. a -> a.
exists b. b -> b.

forall a. free f a

list : (a : data) -> data.
nil : list a.
cons : a -> list a -> list a.

head : cons a (list a) -> a.
tail : cons a (list a) -> list a.

map : (a -> b) -> list a -> list b.
zip : (a -> b -> c) -> list a -> list b -> list c.
foldr : (a -> b -> b) -> b -> list a -> b.
foldl : (b -> a -> b) -> b -> list a -> b.

stream : (a : data) -> codata.
nil : stream a.
cons : a -> stream a -> stream a.

algebra f a : f a -> a.
coalgebra f a : a -> f a.

stream : data -> codata.