## Base interfaces & classes
(jvm;interface Function
               (: apply (-> [java.lang.Object] java.lang.Object)))

(jvm;class Tuple0 java.lang.Object
           [])
(jvm;class Tuple1 java.lang.Object
           [[java.lang.Object _0]])
(jvm;class Tuple2 java.lang.Object
           [[java.lang.Object _0] [java.lang.Object _1]])
(jvm;class Tuple3 java.lang.Object
           [[java.lang.Object _0] [java.lang.Object _1]
            [java.lang.Object _2]])
(jvm;class Tuple4 java.lang.Object
           [[java.lang.Object _0] [java.lang.Object _1]
            [java.lang.Object _2] [java.lang.Object _3]])
(jvm;class Tuple5 java.lang.Object
           [[java.lang.Object _0] [java.lang.Object _1]
            [java.lang.Object _2] [java.lang.Object _3]
            [java.lang.Object _4]])
(jvm;class Tuple6 java.lang.Object
           [[java.lang.Object _0] [java.lang.Object _1]
            [java.lang.Object _2] [java.lang.Object _3]
            [java.lang.Object _4] [java.lang.Object _5]])
(jvm;class Tuple7 java.lang.Object
           [[java.lang.Object _0] [java.lang.Object _1]
            [java.lang.Object _2] [java.lang.Object _3]
            [java.lang.Object _4] [java.lang.Object _5]
            [java.lang.Object _6]])
(jvm;class Tuple8 java.lang.Object
           [[java.lang.Object _0] [java.lang.Object _1]
            [java.lang.Object _2] [java.lang.Object _3]
            [java.lang.Object _4] [java.lang.Object _5]
            [java.lang.Object _6] [java.lang.Object _7]])

(jvm;class Variant java.lang.Object
           [[java.lang.String tag] [java.lang.Object value]])

## Base functions & macros
(def' let'
  (lambda' _ tokens
      (lambda' _ state
          (case' tokens
                 (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
                 [(#Cons [(#Form (#Cons [(#Ident "case'") (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])]))
                          #Nil])
                  state])
          )))
(declare-macro let')

(def' lambda
  (lambda' _ tokens
      (lambda' _ state
          (let' output (case' tokens
                              (#Cons [(#Form (#Cons [self (#Cons [arg args'])])) (#Cons [body #Nil])])
                              (#Form (#Cons [(#Ident "lambda'")
                                             (#Cons [self
                                                     (#Cons [arg
                                                             (#Cons [(case' args'
                                                                            #Nil
                                                                            body

                                                                            _
                                                                            (#Form (#Cons [(#Ident "lux;lambda")
                                                                                           (#Cons [(#Form (#Cons [(#Ident "_") args']))
                                                                                                   (#Cons [body #Nil])])])))
                                                                     #Nil])])])])))
                [(#Cons [output #Nil]) state])
          )))
(declare-macro lambda)

## (def' lambda
##   (lambda' _ tokens
##       (lambda' _ state
##           (let' output (case' tokens
##                               (#Cons [(#Form (#Cons [self (#Cons [arg args'])])) (#Cons [body #Nil])])
##                               (#Form (#Cons [(#Ident "lambda'")
##                                              (#Cons [self
##                                                      (#Cons [arg
##                                                              (#Cons [(case' args'
##                                                                             #Nil
##                                                                             body

##                                                                             _
##                                                                             (#Form (#Cons [(#Ident "lux;lambda")
##                                                                                            (#Cons [(#Form (#Cons [(#Ident "_") args']))
##                                                                                                    (#Cons [body #Nil])])])))
##                                                                      #Nil])])])])))
##                 [(#Cons [output #Nil]) state])
##           )))


## (def' lambda
##   (lambda' _ tokens
##       (lambda' _ state
##           (let' output (case' tokens
##                               (#Cons [(#Form (#Cons [self (#Cons [arg args'])])) (#Cons [body #Nil])])
##                               (#Form (#Cons [(#Ident "lambda'")
##                                              (#Cons [self
##                                                      (#Cons [arg
##                                                              (#Cons [(case args'
##                                                                        #Nil
##                                                                        body

##                                                                        _
##                                                                        (#Form (#Cons [(#Ident "lux;lambda")
##                                                                                       (#Cons [(#Form (#Cons [(#Ident "_") args']))
##                                                                                               (#Cons [body #Nil])])])))
##                                                                      #Nil])])])])))
##                 [(#Cons output #Nil) state])
##           )))

## (def' def
##   (lambda (_ tokens state)
##     (let' output (case' tokens
##                         (#Cons (#Ident name) (#Cons body #Nil))
##                         (#Form (#Cons (#Ident "def'")
##                                       (#Cons (#Ident name)
##                                              (#Cons body #Nil))))

##                         (#Cons (#Form (#Cons (#Ident name) args))
##                                (#Cons body #Nil))
##                         (#Form (#Cons (#Ident "def'")
##                                       (#Cons (#Ident name)
##                                              (#Cons (#Form (#Cons (#Ident "lux:lambda")
##                                                                   (#Cons (#Form (#Cons (#Ident name) args))
##                                                                          (#Cons body #Nil))))
##                                                     #Nil)))))
##           [(#Cons output #Nil) state])))
## (declare-macro def)

## (def (comment tokens state)
##   [#Nil state])
## (declare-macro comment)

## (def (+ x y)
##   (jvm;iadd x y))

## (def (id x)
##   x)

## (def (print x)
##   (jvm;invokevirtual java.io.PrintStream "print" [Object]
##                      (jvm;getstatic System out) [x]))

## (def (println x)
##   (jvm;invokevirtual java.io.PrintStream "println" [Object]
##                      (jvm;getstatic System out) [x]))

## (def (fold f init xs)
##   (do (print "fold ") (print init) (print " ") (println xs)
##       (case' xs
##              #Nil
##              init
             
##              (#Cons x xs')
##              (let' init' (f init x)
##                    (do (print "init': ") (println init')
##                        (fold f init' xs')))
##              #((fold f (f init x) xs'))#
##              )))

## (def (reverse list)
##   (do (print "reverse ") (println list)
##       (let' reversed (fold (lambda [tail head]
##                              (do (print "reverse/0 ") (print "tail: ") (print tail) (print " head: ") (println head)
##                                  (#Cons head tail)))
##                            #Nil
##                            list)
##             (do (print "!reversed ") (println reversed)
##                 reversed))))

## (def (list xs state)
##   (let' xs' (reverse xs)
##         (let' output (fold (lambda [tail head]
##                              (do (print "tail: ") (print tail) (print " head: ") (println head)
##                                  (#Form (#Cons (#Tag "Cons")
##                                                (#Cons head
##                                                       (#Cons tail #Nil))))))
##                            (#Tag "Nil")
##                            (do (print "REVERSED: ") (println xs')
##                                xs'))
##               (do (print "output: ") (println output)
##                   [(#Cons output #Nil) state]))))
## (declare-macro list)

## (def (list+ xs state)
##   (case' (reverse xs)
##     #Nil
##     [#Nil state]

##     (#Cons last init')
##     (let' output (fold (lambda [tail head]
##                          (#Form (#Cons (#Tag "Cons")
##                                        (#Cons head tail))))
##                        last
##                        init')
##           [(#Cons output #Nil) state])))
## (declare-macro list+)

## (def (->pairs xs)
##   (case' xs
##     (#Cons x (#Cons y xs'))
##     (#Cons [x y] (->pairs xs'))

##     _
##     #Nil))

## (def (let tokens state)
##   (case' tokens
##          (#Cons (#Tuple bindings) (#Cons body #Nil))
##          (let' output (fold (lambda [body binding]
##                               (case binding
##                                 [label value]
##                                 (#Form (list (#Ident "let'") label value body))))
##                             body
##                             (reverse (->pairs bindings)))
##                [(list output) state])))
## (declare-macro let)

## (def (++-list xs ys)
##   (case' xs
##     #Nil
##     ys

##     (#Cons x xs*)
##     (#Cons x (++-list xs* ys))))

## (def (map-list f xs)
##   (case' xs
##          #Nil
##          #Nil

##          (#Cons x xs*)
##          (#Cons (f x) (map-list f xs*))))

#(
(def (untemplate-list untemplate tokens)
(case tokens
#Nil
(#Tag "Nil")

(#Cons token tokens')
(#Form (list (#Tag "Cons") (untemplate token) (untemplate-list untemplate tokens')))))

(def (untemplate token)
(case token
(#Bool elem)
(#Form (list (#Tag "Bool") (#Bool elem)))

(#Int elem)
(#Form (list (#Tag "Int") (#Int elem)))

(#Real elem)
(#Form (list (#Tag "Real") (#Real elem)))

(#Char elem)
(#Form (list (#Tag "Char") (#Char elem)))

(#Text elem)
(#Form (list (#Tag "Text") (#Text elem)))

(#Tag elem)
(#Form (list (#Tag "Tag") (#Text elem)))

(#Ident elem)
(#Form (list (#Tag "Ident") (#Text elem)))

(#Form (#Cons (#Ident "~") (#Cons unquoted #Nil)))
unquoted

(#Tuple elems)
(#Form (list (#Tag "Tuple") (untemplate-list untemplate elems)))

(#Form elems)
(#Form (list (#Tag "Form") (untemplate-list untemplate elems)))
))


## I/O
(def (print x)
(jvm;invokevirtual java.io.PrintStream "print" [Object]
(jvm;getstatic System out) [x]))

(def (println x)
(jvm;invokevirtual java.io.PrintStream "println" [Object]
(jvm;getstatic System out) [x]))

(def (' form)
(case form
(#Cons token #Nil)
(untemplate token)))
(declare-macro ')

(def (+ x y)
(jvm;iadd x y))

(def inc (+ 1))

(def length (fold (lambda' l (lambda' x (inc l))) 0))

(def (rem dividend divisor)
(jvm;irem dividend divisor))

(def (= x y)
(jvm;invokevirtual Object "equals" [Object]
x [y]))

(def (pairs list)
(case list
(#Cons x (#Cons y list*))
(#Cons [x y] (pairs list*))

_
#Nil))

(def (show x)
(jvm;invokevirtual Object "toString" []
x []))

(def (concat t1 t2)
(jvm;invokevirtual String "concat" [String]
t1 [t2]))

(def (range from to)
(if (= from to)
#Nil
(#Cons from (range (inc from) to))))

(def (text->list text)
(let' length (jvm;invokevirtual String "length" []
text [])
(map (lambda' idx
(jvm;invokevirtual String "charAt" [int]
text [idx]))
(range 0 length))))

(def (enumerate list)
(case (fold (lambda' state
(lambda' x
(case state
[idx list']
[(inc idx) (#Cons [idx x] list')])))
[0 #Nil]
list)
[_ list']
(reverse list')))

(def list-map #Nil)

(def (put key val map)
(case map
#Nil
(#Cons [key val] map)

(#Cons [?key ?val] map')
(if (= key ?key)
(#Cons [?key val] map')
(#Cons [?key ?val] (put key val map')))))

(def (get key map)
(case map
#Nil
#None

(#Cons [?key ?val] map')
(if (= key ?key)
(#Some ?val)
(get key map'))))

(def (show-kv kv)
(case kv
[?key ?val]
(fold concat "" (list "#" ?key " " (show ?val)))))

(def (interpose elem list)
(case list
(#Cons x (#Cons y list'))
(list+ x elem y (interpose elem list'))

_
list))

(def (show-list xs)
(case xs
#Nil
"#Nil"

(#Cons x xs')
(fold concat "" (list "(#Cons " (show x) " " (show-list xs') ")"))))

(defsig (Equal x)
(: = (-> x x Bool)))

(deftype Equal (All [x r] {#= (-> x x Bool) & r}))
(deftype Equal (All [x] {#= (-> x x Bool)}))
(deftype Equal (All [x] (Exists [r] {#= (-> x x Bool) & r})))

(defimpl (Equal Bool)
(def (= x y)
(case [x y]
[ true  true] true
[false false] true
_             false)))

(def Equal_Bool
(struct {#= [(-> Bool Bool Bool)
(lambda [x y] ...)]}))

(: (~ g!Equal) (Equal Bool))
(: (~ g!Equal) {#= (-> Bool Bool Bool)})
(def (~ g!Equal)
{#= (lambda [x y] ...)})

(def Equal_List
(lambda [Equal_x]
(struct {#= })))

(: Equal_List
(All [x] (-> (Equal x) (Equal (List x)))))

(defimpl (All [x]
(=> [(Equal x)]
(Equal (List x))))
(def (= xs1 xs2)
(case [xs1 xs2]
[#Nil #Nil]
true

[(#Cons x1 xs1') (#Cons x2 xs2')]
(and (Equal_x x1 x2) (= xs1' xs2')))))

(All [x]
(-> (Equal x) (Equal (List x))))

(EqualList EqualBool) => {#= ...}

(: ops (List (Exists [a] [(-> Text a) (-> a [])])))
(def ops (list [(lambda [_] 10) (lambda [_] [])]
[(lambda [_] "") (lambda [_] [])]))

(case ops
#Nil
[]

(#Cons [f1 f2] ops')
(f2 (f1 "E")))

(defsig (Add x)
(: + (-> x x x)))

(defimpl AddInt (Add Int)
#defs
(def (+ x y)
(jvm;ladd x y)))

(defimpl (Add Int)
(def (+ x y)
(jvm;ladd x y)))

(: adder (All [x] (=> [(Add x)]
(-> x (-> x x)))))
(def (adder by)
(lambda [x] (+ by x)))

(adder AddInt 1) -> (lambda [x] ((get@ #+ AddInt) 1 x))
adder == (lambda [impl]
(case impl
{#+ +}
(lambda [x] (+ by x))))

(: calc (All [v]
(-> (-> v Int)
(| (#Add Int Int) (#Mul Int Int) & v)
Int)))
(def (calc backup expr)
(case expr
(#Add x y) (+ x y)
(#Mul x y) (* x y)
else       (backup else)))

(defsig Yolo
(: lol? (-> Text Bool))
(: foo Int))

(defimpl Meme [Yolo]
(def (lol? _) true)
(def foo 10))

(defimpl Nyan [Yolo]
Meme
(def foo 20))

(list 1 2 3) == (#Cons 1 (#Cons 2 (#Cons 3 #Nil)))
(list+ 1 2 (list 3))

(defsig (Monoid a)
(: empty a)
(: ++ (BinaryOp a)))

(: concat (All [a]
(=> [(Monoid a)]
(-> (List a) a))))
(def (concat mon
xs)
(fold (:: mon #++) (:: mon #empty) xs))

(defstruct (Monoid Text)
(def empty "")
(def (++ x y)
...))

(defstruct (All [a]
(Monoid (List a)))
(def empty (list))
(def (++ xs ys)
(case xs
#Nil
ys

(#Cons x xs')
(#Cons x (++ xs' ys)))))

(: map (All [a b] (-> (-> a b) (List a) (List b))))

(defsig (Collection c)
(: add    (All [x] (-> x (c x) (c x))))
(: length (All [x] (-> (c x) Int))))

(defclass (Stack s)
(: push (All [x] (-> x (s x) (s x))))
(: pop  (All [x] (-> (s x) (s x))))
(: peek (All [x] (-> (s x) (Maybe x)))))

(deftype (BinaryOp t)
(-> t t t))

(defclass (Number n)
(: + (BinaryOp n))
(: - (BinaryOp n))
(: * (BinaryOp n))
(: / (BinaryOp n)))

(def (flip f)
(lambda [x y]
(f y x)))

(def (concat' xss)
(case (reverse xss)
#Nil
#Nil

(#Cons xs xss')
(fold (flip ++) xs xss')))

n + n*m

(with [AddInt]
(+ 10 20))

(:: AddInt (+ 10 20)) == ((get@ AddInt #=) 10 20)

(defimpl (Stack List)
(def (push x xs)
(#Cons x xs))

(def (pop xs)
(case xs
#Nil          #Nil
(#Cons _ xs') xs'))

(def (peek xs)
(case xs
#Nil        #None
(#Cons x _) (#Some x))))

(defsig (Functor f)
(: map (All [a b] (-> (-> a b) (f a) (f b)))))

(def (Functor f)
{#map  (All [a b] (-> (-> a b) (f a) (f b)))})

(defimpl ListFunctor (Functor List)
(def (map func fa)
(case fa
#Nil
#Nil

(list a fa')
(list (func a) (map func fa')))))

(implicit ListFunctor
(map inc (list 1 2 3)))

(defsig (=> [(Functor m)]
(Monad m))
(: return (All [x] (-> x (m x))))
(: bind (All [a b] (-> (m a) (-> a (m b)) (m b)))))



(#User {#name Text #age Int})
(deftype User {#name Text #age Int})
(deftype User (& (#name Text)
(#age Int)))
(deftype User (All [r]
(& (#name Text)
(#age Int)
++ r)))
(def User (#Record (list ["name" Text] ["age" Int])))

(let [thunk (... (+ 5 6))]
(! thunk))

(Thunk Int)


(deftype Int&Bool [Int Bool])

(deftype (List a)
(| #Nil
(#Cons a (List a))))

(defclass (Equal a)
(: = (-> a a Bool)))
==
(deftype (Equal a)
{#= (-> a a Bool)})

(def Equals
(All [a] {#= (-> a a Bool)}))

(defimpl EqualBool [(Equal Bool)]
(def (= x y)
(if x
y
(not y))))

(def ... {#= (lambda [x y] (if x
y
(not y)))})

(def Class (All [I]
(Exists [S] (& (#state S)
(#methods (I S))))))

(definterface Vector
(: translate (BinaryOp Vector)))

(def Vector (Some [Vector]
(& (#translate (BinaryOp v)))))

(defclass Vector2D
{#x Real, #y Real}
(def (new-Vector2D x y)
{#x x, #y y})
Vector
(def (translate self offset)
(-> self
(update@ #x + (get@ offset #x))
(update@ #y + (get@ offset #y)))))

(def Vector2D
{#translate (: (lambda [self offset]
(-> self
(update@ #x +real (get@ offset #x))
(update@ #y +real (get@ offset #y))))
(BinaryOp {#x Real, #y Real}))})

(: new-Vector2D (-> Real Real [{#x Real, #y Real} (@class Vector2D)]))
(def (new-Vector2D x y)
[{#x x, #y y} Vector2D])

(defsig (Vector v)
(: translate (BinaryOp v))
(: scale (BinaryOp v)))

(def Vector (All Vector [v]
(& (#translate (BinaryOp v))
(#scale (BinaryOp v)))))

(defstruct Vector2D (Vector [Real Real])
(def (translate [x1 y1] [x2 y2])
[(+ x1 x2) (+ y1 y2)])
(def (scale [x1 y1] [x2 y2])
[(* x1 x2) (* y1 y2)]))

(def Vector2D (: {#translate (lambda [[x1 y1] [x2 y2]]
[(+real x1 x2) (+real y1 y2)])
#scale (lambda [[x1 y1] [x2 y2]]
[(*real x1 x2) (*real y1 y2)])}
(Vector [Real Real])))

(deftype (Stream a)
(| (#Cons a (Thunk (Stream a)))))

(: iterate (All [a] (-> (-> a a) a (Stream a))))
(def (iterate f init)
(list init (... (iterate f (f init)))))

(def (take n stream)
(if (<= n 0)
#Nil
(case stream
(#Cons x stream')
(#Cons x (take (dec n) stream')))))

(deftype (Stream a)
(All [b] (-> (-> a (Stream a b) b) b)))

(: iterate (All [a] (-> (-> a a) a (Stream a))))
(def (iterate f init)
(lambda [k]
(k init (iterate f (f init)))))

(def (repeat x)
(lambda [k] (k x (repeat x))))

(def (take n stream)
(if (<= n 0)
#Nil
(stream (lambda [x stream']
(#Cons x (take (dec n) stream'))))))

(defsig (Comonad w)
(: extract (All [a] (-> (w a) a)))
(: extend (All [a b] (-> (w a) (-> (w a) b) (w b)))))

(defstruct Stream (Comonad w)
(def (extract stream)
(stream (lambda [x _] x)))
(def (extend w f)
...))

(: fibonacci (Stream Int))
(def fibonacci ((lambda fibonacci [a b]
(lambda [k] (k a (fibonacci b (+ a b)))))
0 1))

(gen fibonacci [a 0 b 1]
(yield a (fibonacci b (+ a b))))

(defgen fibonacci [a 0 b 1]
(yield a (fibonacci b (+ a b))))

(gen fibonacci [a 0 b 1]
(yield a [b (+ a b)]))

## The dual of do-notation should be be-notation

(deftype (Stream a)
(| (#Cons a (Thunk (Stream a)))))

(defstruct (Functor Stream)
(def (map f s)
(lambda [k]
(stream (lambda [x stream']
(f s))))))

(deftype (Tape a)
(| (#Index (Thunk (Stream a)) a (Thunk (Stream a)))))

(deftype (Area a)
(| (#Cursor (Tape a) (Surreal a))))

(def (ints offset n)
(#Index (... (iterate (lambda [n'] (- n' offset)) n))
n
(... (iterate (+ offset) n))))

(def (reals offset x)
(#Cursor (ints offset x)
(reals (/ offset 10) 0)))
)#

#(
(deftype (Session i o s)
(All [s' r]
(-> (-> i s' r)
(-> o s [i s'])
r))

(All [s' s''] (-> (-> c s' [p s''])
(-> [] s [c s']) (Session c p s)
[p s'']))
(All [] (-> (-> c s p)
(-> p [])))
(All [r] (-> c (Session r p s) p)))

(Session Int [] (Session Int (Session [] Int <END>)))

(bind (session' [])
(lambda [x session']
(bind (session' [])
(lambda [y session'']
(session'' (+ x y))))))

(defstruct SessionMonad
(Monad Session)
(def (return v)
(lambda [k session]
(k v session)))
(def (bind step m-value)
(lambda [k session]
(let [[v session'] (m-value [] session)]
(k (step v) session')))))

## Not really "do"; but oh, well...

(deftype <NIL>
(| #Nil))

(deftype (HList h t)
(| (#Cons h t)))

(deftype (Session c p s)
(All [r] (-> c (-> p s r) r)))

(deftype (Session c p s)
(-> (-> p s c) c))

(deftype (? r s)
(Session r [] s))

(deftype (! w s)
(Session [] w s))

(deftype #rec <END>
(Session [] [] <END>))

(def <<
(lambda [k session]
(k [] session)))

(def (>> val)
(lambda [k session]
(session val k)))

(<$> << (>> 5))

(def (<$> consumer producer)
(producer [] consumer))

(HList Int (HList Int <NIL>))

(<.> (? Int) (? Int) (! Int) <END>)
(def fn-session
(do [x <<
y <<]
(>> (+ x y))))

(<.> (! Int) (! Int) (? Int) <END>)
(def call-session
(do [_ (>> 5)
_ (>> 10)]
<<))

(<$> fn-session call-session)

(def <<
(lambda [chan]
(chan (lambda []))))

(def (>> value)
(lambda [chan]
(chan value)))
)#

## (defsig (Equal a)
##   (: = (-> a a Bool)))

## (: not= (All [a] (-> (Equal a) a a Bool)))
## (def (not= &Equal
##            x x)
##   (not (:: &Equal (= x x))))

## (defstruct Int
##   []
##   (Equal Int)

##   (def (= x y)
##     (zero? (- x y))))

## (defsig (Show a)
##   (: show (-> a Text)))

## (defstruct (ListShow x)
##   [&show (Show a)]
##   (Show (List a))

##   (def (show xs)
##     (<> "(" (interpose ", " (map (:: &show show) xs)) ")")))

## (def ListShow
##   (: (lambda [&show]
##         {#show (lambda show [xs]
##                   (<> "(" (interpose ", " (map (:: &show show) xs)) ")"))})
##      (-> (Show a) (Show (List a)))))

## (deftype (Identity a) a)

## (deftype (List a)
##   (| #Nil
##      (#Cons a (List a))))

## (def (ListT m)
##   (All [a] (List (m a))))

## (ListT Identity)

## (defsig (Monad m)
##   (: return (All [a] (-> a (m a))))
##   (: bind (All [a b] (-> (-> a (m b)) (m a) (m b)))))

## (def Monad
##   (All [m]
##        (sig (: return (All [a] (-> a (m a))))
##             (: bind (All [a b] (-> (-> a (m b)) (m a) (m b)))))))

## (defstruct Monad<Identity> (Monad Identity)
##   (def (return x)
##     x)
##   (def (bind f x)
##     (f x)))

## (: Monad<Identity> (Monad Identity))
## (def Monad<Identity>
##   (struct
##    (def (return x)
##      x)
##    (def (bind f x)
##      (f x))))

## (defstruct Monad<List> (All [m] (-> (Monad m)
##                                     (Monad (ListT m))))
##   (def (return x)
##     (list x))
##   (def (bind f xs)
##     (case xs
##       #Nil          #Nil
##       (#Cons x xs') (#Cons (f x) (bind f xs')))))

## (deftype #rec Type
##   ($data #Any
##          #Nothing
##          (#Data Text (List Type))
##          (#Lambda Type Type)
##          (#All (List [Text Type]) Text Text Type)
##          (#Exists (List [Text Type]) Text Type)
##          (#Lookup Text)
##          (#Var Int)))