-- V ::= [C] | 0 | V + V' | 1 | V * V'
-- C ::= {V} | V -> C | top | C & C'

neg : [ int -> {int} ]
add : [ int -> int -> {int} ]

abs : [ int -> {int} ]
abs = [ \ n: int.
          if n < 0
            then {0 - n}
            else {n}
      ]

add : [ int -> {int} ]
add = [ \ (x: int) (y: int) . { x + y } ]

data List a where
  Nil  :                List a
  Cons : a -o List a -o List a

nums : List Int
nums = Cons(1, Cons(2, Cons(3, Nil)))

-- fn name arg1 arg2 ... argn = blah
--   ==>
-- name = [ \ arg1 arg2 ... argn . blah ]

sumlist : [ List Int -> {Int} ]
fn sumlist (Cons x xs) = let y <- sumlist xs in { x + y }
   sumlist Nil         = { 0 }

data Tree where
  Leaf : Int -o Tree
  Node : Tree * Tree -o Tree

codata Stream a where
  .head : {a}
  .tail : Stream

ones : Stream Int
ones = rec this
  this.head <- {1}
  this.tail <- this