Hindley-Milner type inference in Scheme, for Scheme

C# port here, Rust port here.

This is a type inference engine built on the Hindley-Milner algorithm, that analyzes, type-checks and computes the type of expressions written in an extended subset of Scheme.

Supported Scheme constructs

• (let ([name val] ...) body): basic let
• (let* ([name val] ...) body): ordered let (each symbol can access the symbols defined before it)
• (letrec ([name val] ...) body): let with recursion support (symbols can access themselves inside a lambda definition)
• (lambda (a b ...) body): lambda definition
• (f a b ...): procedure application (difference from Scheme: implicit partial application; such that (pair a b) is strictly equivalent to ((pair a) b))

Built-ins

Types:

• int (Scheme number?)
• bool (Scheme boolean?)
• str (Scheme string?)
• unit (void/unit type)
• bottom (Haskell forall a. a, Rust !)

Symbols:

	Name	Signature (n-ary syntax)
Numbers	+, -, *, /, modulo, succ, pred	[int int] -> int
	=	[int int] -> bool
	zero	int -> bool
Booleans	and, or	[bool bool] -> bool
Utilities	error	str -> never
	if	[bool a a] -> a
Pairs	pair	[a b] -> (a * b)
	car	(a * b) -> a
	cdr	(a * b) -> b
Lists	nil	(list a)
	cons	[a (list a)] -> (list a)
	hd	(list a) -> a
	tl	(list a) -> (list a)
	null?	(list a) -> bool
Either	left	a -> (either a b)
	right	b -> (either a b)
	either	[(either a b) (a -> x) (b -> y)] -> (either x y)
Maybe	just	a -> (option a)
	nothing	(option a)
	maybe	[(option a) (a -> x)] -> (option x)

Internals

All functions are internally curried, as in Haskell, e.g. the type of pair is (a -> (b -> (a * b))). This allows for built-in support for partial application (cf. above) in the HM framework, while still allowing to define n-ary functions.

In effect, (lambda (a b) body) is syntactic sugar for (lambda (a) (lambda (b) body)).