( 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))