FunVM.org

-- strict (polymorphic) identity function
id : (a :: *, a) -> a
  = \(a :: *, x : a) -> x

-- lazy constant function
const : (a :: *, b :: *, {a}, {b}) -> a
  = \(a :: *, b :: *, x : {a}, y : {b}) -> |x|

-- function application function, polyvariant in strictness of argument function
app : (s : strictness, a :: *, (a^s -> a), a^s) -> a
  = \(s : strictness, a :: *, f : (a^s -> a), x : a^s) -> f x

-- function application function, type inferred (no automatic generalization)
app' = \(s, a, f : (a^s -> a), x : a^s) -> f x

-- imaginary if function (no data types, yet)
if : (a :: *, Bool, {a}, {a}) -> a
  = \(a :: *, b : Bool, x : {a}, y : {a}) ->
      case b of
        | True   -> |x|
        | False  -> |y|

-- imaginary map function (no data types, yet)
-- note: haskell-style list, all fields are lazy
map : (s : strictness, a :: *, (a^s -> a), List a) -> List a
  = \(s : strictness, a :: *, f : (a^s -> a), xs : List a) ->
      case xs of
        | Nil                            -> Nil
        | Cons (y : {a}, ys : {List a})  -> Cons ({f |y|}, {map (s, a, f, |ys|)})