hindley-milner
An implementation of Algorithm W (and an interpreter) for a simple lambda-calculus.
Assumptions
You have installed Leiningen and Git
Getting Set Up
Clone the repository:
git clone https://github.com/ericnormand/hindley-milner
cd hindley-milner
lein repl
user>
user> (ns user
(:refer-clojure :exclude [eval])
(:require [hindley-milner.syntax :refer :all]
[hindley-milner.eval :refer :all]
[hindley-milner.types :refer :all]))
Usage - Syntax
user> '(fn [a] x)
(fn [a] x)
user> (lambda? '(fn [a] x))
true
user> (free-vars '(let [a x
b y]
(((z a) b) c)))
#{'x 'y 'z 'c}
Usage - Evaluation
user> (interpret env 1)
1
user> (interpret env
'(let [c (dec b)
id (fn a a)
b 2]
(id c)))
1
Usage - Type Inference
user> (infer tenv 1)
:Integer
user> (infer* tenv '(if true 1 2))
[:Lambda :Integer]
user> (let [[_ [_] [_ [_ _ x] y]]
(infer* tenv '(fn [a]
(let [x (fn [b]
(let [y (fn [c]
(a 1))]
(y 2)))]
(x 3))))]
(= x y))
true
Usage - Running Tests
To run the tests:
lein test
Goals
Pull requests welcome!
- Implement Hindley-Milner in Clojure (DONE!)
- Learn and teach about type systems
- Discover similarities between Lisp's meta-circular
evaland syntax-directed HM.
Non-goals
- To type check Clojure.
TODO
- Add support for inferencing multiple bindings in a
let. - Add negative tests
- Docstrings
License
Copyright Β© 2014 Eric Normand
Please see http://lispcast.com/Hindley-Milner-in-Clojure for rationale.
Distributed under the Eclipse Public License either version 1.0 or (at your option) any later version.