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.
(let ([name val] ...) body): basiclet(let* ([name val] ...) body): orderedlet(each symbol can access the symbols defined before it)(letrec ([name val] ...) body):letwith 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))
Types:
int(Schemenumber?)bool(Schemeboolean?)str(Schemestring?)unit(void/unit type)bottom(Haskellforall 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) |
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)).