Skip to content

zdimension/hm-infer-rs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

16 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Hindley-Milner type inference for Scheme, in Rust

Port of hm-infer-scheme and hm-infer-cs.

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
  • (head 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:

NameSignature (n-ary syntax)
Numbers+, -, *, /, modulo, succ, pred[int int] -> int
=[int int] -> bool
zeroint -> bool
Booleansand, or[bool bool] -> bool
Utilitieserrorstr -> never
if[bool a a] -> a
Pairspair[a b] -> (a * b)
car(a * b) -> a
cdr(a * b) -> b
Listsnil(list a)
cons[a (list a)] -> (list a)
hd(list a) -> a
tl(list a) -> (list a)
null?(list a) -> bool
Eitherlefta -> (either a b)
rightb -> (either a b)
either[(either a b) (a -> x) (b -> y)] -> (either x y)
Maybejusta -> (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)).

About

Hindley-Milner type inference for Scheme, in Rust

Topics

Resources

License

Stars

Watchers

Forks

Languages