# Vinilla Lang

Vanilla is a pure functional programming language based on System F, a classic but powerful type system.

## Merits

Simple as it is, Vanilla contains many features that most main-stream languages don't have:

- Higher-rank polymorphism
- It allows using polymorphic functions as arguments of higher-order functions

- Strong type inference
- Only polymorphic and recursive bindings need annotations

- Algebraic data types
- Simplicity
- Only foralls
`∀`

and arrows`→`

are built-in types - All regular types such as
`Unit`

and`Bool`

can be declared as ADT and eliminated by`case`

expression

- Only foralls

## Defects

- No module system
- For simplicity, this programming language only supports type checking and evaluation on closed terms.

## Grammar

```
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
```

A valid Vanilla program consists of several ADT declarations followed by a main expression.

ADT declarations are similar to ones in Haskell, except that they end with a dot for easy parsing.

Haskell-style comments (`--`

and `{- -}`

) are also supported.

## Usage

First of all, `ghc`

and `cabal-install`

should be installed in your `$PATH`

## Examples

### Higher-rank Polymorphism

Given `example/cont.vn`

:

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

Run

```
cabal run example/cont.vn
```

It should output:

```
Type:
Unit
Result:
Unit
```

### Map for Lists

Given `example/map.vn`

:

```
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
```

Run

```
$ cabal run example/map.vn
```

It should output:

```
Type:
List Bool
Result:
Cons False (Cons True Nil)
```

### Add operator for Natural Numbers

Given `example/add.vn`

:

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

Run

```
$ cabal run example/add.vn
```

It should output the inferred type and evaluated value of this program:

```
Type:
Prod Nat Nat
Result:
Prod (Succ (Succ (Succ (Succ (Succ Zero))))) (Succ (Succ (Succ (Succ (Succ Zero)))))
```

### Mutual Recursion

Mutual recursive functions can be easily defined with the fixpoint and projections.

Given `example/evenodd.vn`

:

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

It reports:

```
Type:
Prod Bool Bool
Result:
Prod False True
```

### Ill-typed Program

Given `example/illtypedid.vn`

:

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

It reports typechecking error:

```
Typecheck error:
cannot establish subtyping with Unit <: Nat
```

### Unit tests

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

## Features

- Static semantic
- Higher-rank polymorphism
- Type inference
- Dynamic semantic
- Both annotated and implicit λ
- Examples
- Unit tests
- Let Binding
- Algebraic data types
- Declarations
- Introductions and eliminations
- Well-formedness checking

- Type application
- Fixpoint for general recursion
- Let rec
- Parser
- Pretty printing