Types           A, B, C   ::= T A1...An | a | ∀a.A | A → B
Monotypes       τ, σ      ::= T τ1...τn | a | τ → σ

Data Type       T         ::= T
Constructor     K         ::= K
Declaration     D         ::= data T a1...at = K1 τ1...τm | ... | Kn σ1...σn .
Pattern         p         ::= K x1...xn

Expressions     e, f      ::=   x                                     -- variable
                              | K                                     -- constructor
                              | case e of {pi → ei}                   -- case
                              | λx.e                                  -- implicit λ
                              | λx : A.e                              -- annotated λ
                              | e1 e2                                 -- application
                              | e : A                                 -- annotation
                              | let x = e1 in e2                      -- let binding
                              | let x : A = e1 in e2                  -- annotated let binding
                              | let rec f : A = e1 in e2              -- recursive binding (sugar)
                              | fix e                                 -- fixpoint
                              | e @ A                                 -- type application

Program         P         ::= D P | e

data Unit = Unit.

-- Can you belive that
-- type `a` and `∀r. ((a → r) → r)` are isomorphic?

let cont : ∀a. a → ∀r. ((a → r) → r) =
  λ x . λ callback . callback x
in

let runCont : ∀a. (∀r. (a → r) → r) → a =
  λ f . (let callback = λ x . x in f callback)
in

-- should output Unit
runCont (cont Unit)

cabal run example/cont.vn

Type:
Unit

Result:
Unit

data Bool = False | True.
data List a = Nil | Cons a (List a).


let rec map : ∀a. ∀b. (a → b) → (List a) → (List b) =
  λ f. λ xs. case xs of {
      Nil → Nil,
      Cons y ys → Cons (f y) (map f ys)
    }
in

let not : Bool → Bool =
  λb. case b of {False → True, True → False}
in

let xs = Cons True (Cons False Nil) in

map not xs

$ cabal run example/map.vn

Type:
List Bool

Result:
Cons False (Cons True Nil)

data Nat = Zero | Succ Nat.
data Prod a b = Prod a b.

-- add can be defined by `fixpoint`
let add : Nat → Nat → Nat =
  fix (λf. λx : Nat . λy : Nat. case x of {Zero → y, Succ a → Succ (f a y)})
in

-- or `let rec`
let rec add2 : Nat → Nat → Nat =
  λ x . λ y . case x of {Zero → y, Succ a → Succ (add2 a y)}
in

let two = Succ (Succ Zero) in
let three = Succ two in

-- 3 + 2 = 5
Prod (add three two) (add2 three two)

$ cabal run example/add.vn

Type:
Prod Nat Nat

Result:
Prod (Succ (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ (Succ (Succ Zero)))))

data Nat = Zero | Succ Nat.
data Bool = False | True.
data Prod a b = Prod a b.

let evenodd : Prod (Nat → Bool) (Nat → Bool) =
  fix (λ eo .
    let e = λ n : Nat . case n of { Zero → True, Succ x → (case eo of {Prod e o → o}) x } in
    let o = λ n : Nat . case n of { Zero → False, Succ x → (case eo of {Prod e o → e}) x } in
    (Prod e o))
in

let even = (case evenodd of {Prod e o → e}) in
let odd = (case evenodd of {Prod e o → o}) in

let five = Succ(Succ(Succ(Succ(Succ(Zero))))) in

Prod (even five) (odd five)

Type:
Prod Bool Bool

Result:
Prod False True

let id : Nat → Nat =
  (λx . x)
in
  id ()

Typecheck error:
cannot establish subtyping with Unit <: Nat

$ cabal test
...
Running 1 test suites...
Test suite vanilla-test: RUNNING...
Test suite vanilla-test: PASS
...