(* Axiom: all extant Latka programs without functions should continue
 * to work the same way, e.g. *)

cons  = $(p t k w h)
vowel = $(a e i o u) (4: "" | "")
syll  = 4: cons vowel | vowel
puts syll (rep.6.syll)

(* We can now define rep in-language as
 * rep (fixed n : Nat) (s : String) : String =
     case n of
       0 . ""
       1 . s
       _ . s (rep.(pred.n).s)
  *)

(* It is acceptable that all arguments must be explicitly specified. *)

fact (fixed n : Nat) : Nat=
  case n of
    0 . 0
    _ . mul.n.(fact.(pred.n))

(* We have both labeled sums and records, where the records are closer to
 * the ML style than the Haskell style. `alias` is Haskell's `type` *)

alias Person =
  { name : String
  , age  : Nat
  }

data Character =
  Character Person

(* Type variables work as in Haskell *)

data List a = Nil | Cons a (List a)

map (f : a -> b) (ls : List a) =
  case ls of
    Cons x xs . Cons.(f.x).xs
    _         . Nil

(* We can explicitly indicate a subtyping (convertibility)
 * relationship, so long as our conv instances form a DAG. *)

data TaggedList a = TNil | TCons a String (List a)

conv TaggedList a <: List a where
  coerce ls = case ls of
    TCons x _ xs . Cons x xs
    TNil         . Nil

(* Among other things, this is used in variadic functions parameters. *)

appendAll (lsts : Variadic (List a)) : List a =
  let go ls = case ls of
        []      . []
        (x::xs) . append.x.(go.xs)
  in go lsts

puts cat.(appendAll.(["x","y"], TCons "z" TNil))
