An implementation of a predicative polymorphic language with bidirectional type inference and algebraic data types

Overview

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

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

References

You might also like...
A typemap for a set of known types optionally without heap allocation, and supporting iterating by traits

fixed_typemap docs.rs GitHub Sponsors Implements typemaps that support a lot of extra funcctionality using procedural macros. docs.rs has a lot more t

An expression based data notation, aimed at transpiling itself to any cascaded data notation.

Lala An expression oriented data notation, aimed at transpiling itself to any cascaded data notation. Lala is separated into three components: Nana, L

Custom deserialization for fields that can be specified as multiple types.

serde-this-or-that Custom deserialization for fields that can be specified as multiple types. This crate works with Cargo with a Cargo.toml like: [dep

Seamless Higher-Kinded Types in Rust

Seamless Higher-Kinded Types in Rust This is actual working code: pub trait FunctorA : HKT1 { fn mapB, F: FnMut(A) - B(self, f: F) - Self::W

Idiomatic Rust implementations for various Windows string types (like UNICODE_STRING)
Idiomatic Rust implementations for various Windows string types (like UNICODE_STRING)

nt-string by Colin Finck [email protected] Provides idiomatic Rust implementations for various Windows string types: NtUnicodeString (with NtUnicode

Create custom ID types that are guaranteed to be valid `RecordID` in SurrealDB

surreal-id The surreal-id crate offers a standardized way to create and validate IDs in your application for usage with SurrealDB. Using the NewId tra

A repository for showcasing my knowledge of the Rust programming language, and continuing to learn the language.

Learning Rust I started learning the Rust programming language before using GitHub, but increased its usage afterwards. I have found it to be a fast a

Nyah is a programming language runtime built for high performance and comes with a scripting language.

🐱 Nyah ( Unfinished ) Nyah is a programming language runtime built for high performance and comes with a scripting language. 🎖️ Status Nyah is not c

Mewl, program in cats' language; A just-for-fun language
Mewl, program in cats' language; A just-for-fun language

Mewl The programming language of cats' with the taste of lisp 🤔 What,Why? Well, 2 years ago in 2020, I created a esoteric programming language called

Owner
Zehao Chen
who am i
Zehao Chen
A statically-typed, interpreted programming language, with generics and type inference

Glide A programming language. Currently, this includes: Static typing Generics, with monomorphization Type inference on function calls func identity<T

Patrick Gu 1 Apr 10, 2022
Messing around with delimited continuations, fibers, and algebraic effects

A Simple Virtual Machine with Effects Each thread of execution in this VM is called a Fiber. A Fiber is unique, can be sent between threads, but can n

Isaac Clayton 8 Jun 23, 2022
Build database expression type checker and vectorized runtime executor in type-safe Rust

Typed Type Exercise in Rust Build database expression type checker and vectorized runtime executor in type-safe Rust. This project is highly inspired

Andy Lok 89 Dec 27, 2022
Type erased vector. All elements have the same type.

Type erased vector. All elements have the same type. Designed to be type-erased as far as possible - most of the operations does not know about concre

null 7 Dec 3, 2022
A simple and convenient way to bundle owned data with a borrowing type.

A simple and convenient way to bundle owned data with a borrowing type. The Problem One of the main selling points of Rust is its borrow checker, whic

Dmitry Zamkov 20 Dec 21, 2022
A library for transcoding between bytes in Astro Notation Format and Native Rust data types.

Rust Astro Notation A library for transcoding between hexadecimal strings in Astro Notation Format and Native Rust data types. Usage In your Cargo.tom

Stelar Software 1 Feb 4, 2022
A special rope, designed to work with any data type that is not String

AnyRope AnyRope is an arbitrary data type rope for Rust, designed for similar operations that a rope would do, but targeted at data types that are not

ahoyiski 27 Mar 22, 2023
A type-safe, high speed programming language for scalable systems

A type-safe, high speed programming language for scalable systems! (featuring a cheesy logo!) note: the compiler is unfinished and probably buggy. if

Hail 0 Sep 14, 2022
A Rust trait to convert numbers of any type and size to their English representation.

num2english This Rust crate provides the NumberToEnglish trait which can be used to convert any* number to its string representation in English. It us

Travis A. Wagner 6 Mar 8, 2023