-
Notifications
You must be signed in to change notification settings - Fork 2
labichn/hmc
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
Hindley-Milner with contracts. Class assignment for dvh's fall '14 cmsc631. labichn E ::= n # some natural number | true | false | x # some variable name | (add1 E) | (+ E E) | (* E E) | (/ E E) | (= E E) | (and E E) | (not E) | (or E E) | (if E E E) | (lambda x E) | (let (x E) E) | (? E) | (-> E E) | (! E E) | (E E) T ::= B | N # includes divide by zero errors | T -> T | T/c | X TE ∈ ℘(T * T) EQ ∈ ℘(T * T) XS ∈ ℘(X) The notation `T = T'` denotes that types T and T' are equal and is represented as a pair of types T and T'. The notation `T if EQ` represents some type T if the set of type equality assertions EQ can be unified and is represented as a pair of types T and EQ. Most work of the type system is shunted off to unification. Unification is implemented as per Van Horn's /Program Analysis and Understanding/ with some extensions detailed below. The ternary typing relation _ |- _ : _ ∈ TE * E * (B * EQ) is defined as follows: Base leaves: -------------------- true TE |- true : B if {} --------------------- false TE |- false : B if {} ----------------- n TE |- n : N if {} `unary` and `binary` handle tedious patterns for expressions that always return base types: TE |- E : T' if EQ ----------------------------------- base unary unary T TE E = T if EQ U (T = T') TE |- E : T' if EQ TE |- E' : T'' if EQ' ------------------------------------------------------- base binary binary T TE E E' = T if EQ U EQ' U (T = T') U (T = T'') Base operations: N if EQ = unary N TE E ------------------------ add1 TE |- (add1 E) : N if EQ N if EQ = binary N TE E E' -------------------------- * TE |- (* E E') : N if EQ N if EQ = binary N TE E E' -------------------------- + TE |- (+ E E') : N if EQ N if EQ = binary N TE E E' -------------------------- / TE |- (/ E E') : N if EQ B if EQ = unary B TE E ----------------------- not TE |- (not E) : B if EQ B if EQ = binary B TE E E' -------------------------- or TE |- (or E E') : B if EQ B if EQ = binary B TE E E' -------------------------- and TE |- (and E E') : B if EQ Equality is defined for everything and always returns a boolean. Bit of a cop-out, but we'll just assume that function equality is defined to be false. TE |- E : T if EQ TE |- E' : T' if EQ --------------------------------------- = (= E E') |- B if EQ U EQ' For if, the predicate must be in B and the branches must have the same type. TE |- E' : T' if EQ' TE |- E'' : T'' if EQ'' TE |- E : T if EQ ------------------------------------------------------------------- if TE |- (if E E' E'') : T' if EQ U EQ' U EQ'' U (T = B) U (T' = T'') The metafunction `genvar` always returns a fresh type variable. It is used here to generate a new type variable for lambda's input, T = genvar TE, X : T |- E : T' if EQ -------------------------------------- lambda TE |- (lambda X E) : T -> T' if EQ `genvar` is used again to generate a type variable for the result of an application. TE |- E : T if EQ TE |- E' : T' if EQ' T'' = genvar ------------------------------------------------------- app TE |- (E E') : T'' if EQ U EQ' U (T = T' -> T'') The metafunction `fv` is defined using structural recursion over the given type: fv(X) = {X} fv(T -> T') = fv(T) U fv(T') fv(T/c) = fv(T) fv(∀ X ... . T) = fv(T) - BS ... fv(_) = {} otherwise `fv` can be lifted to TE as the union of the free variables of every element in its codomain. The metafunction `gen` generalizes some type T in environment TE as follows: gen(TE, T) = ∀ (fv T) - (fv TE) . T and enables let polymorphism in the following rule. TE |- E : T if EQ TE, X : gen(TE, T) |- E' : T' if EQ' -------------------------------------------------------- let TE |- (let (X E) E') : T' if EQ U EQ' Typing contracts is easy. Predicates generate a new assertion that E's type is a function from some type T to B. T = genvar TE |- E : T' if EQ --------------------------------------- pred contract TE |- (? E) : T/c if EQ U (T' = T -> B) Contract arrows generate new type variables T'' and T''' for the type parameters of the contract types T and T', respectively. TE |- E : T if EQ TE |- E' : T' if EQ' T'' = genvar T''' = genvar --------------------------------------------- arr contract TE |- (-> E E') : (T'' -> T''')/c if EQ U EQ' U (T'' = T/c) U (T''' = T''/c) Monitors generate a new type variable T'' for the type parameter of the contract type T. TE |- E : T if EQ TE |- E' : T' if EQ' T'' = genvar --------------------------------------------- monitor TE |- (! E E') : T' if EQ U EQ' U (T = T''/c) Beta reduction is defined for types as follows: β(T -> T', X, U) = β(T, X, U) -> β(T', X, U) β(T/c, X, U) = β(T, X, U)/c β(Y, X, U) = U when X = Y β(Y, X, U) = X when X != Y β(∀ YS . T, X, U) = ∀ YS . T when X ∈ YS β(∀ YS . T, X, U) = ∀ YS . β(T, X, U) when X ∉ YS β(T, X, U) = T otherwise Variables mapping to polytypes are instantiated with the metafunction `inst`, iteratively generating fresh variables for all bound variables using `β`. Monotypes are just returned: inst(∀ XS . T) = inst'(XS, T) inst(T) = T otherwise inst'({}, T) = T inst'(X U XS, T) = inst'(XS, β(T, X, genvar)) Finally the typing rule for variables: X : T ∈ TE T' = inst(T) ------------------------- var TE |- X : T' if {} After all this we have some type T if EQ can be unified. Unification is extended componentwise through arrows and contracts, and handles recursive types by checking if a variable occurs in its own type expansion: occurs(TE, X, T -> T') = occurs(TE, X, T) or occurs(TE, X, T') occurs(TE, X, T/c) = occurs(TE, X, T) occurs(TE, X, Y) = X = Y occurs(TE, X, _) = false otherwise unify(T) = unify'(EQ, T) unify'( {}, TE) = TE unify'( (T = T') U EQ, TE) = unify'(EQ, TE) when T = T' unify'( (X = T) U EQ, TE) = unify'(EQ U (T = TE(X)), TE) when not occurs(TE, X, T) unify'( (T = X) U EQ, TE) = unify'(EQ U (X = T), TE) unify'( (T/c = T'/c) U EQ, TE) = unify'(EQ U (T = T'), TE) unify'((T -> U = T' -> U') U EQ, TE) = unify'(EQ U (T = T') U (U = U'), TE) References: Clement, (1987). The Natural Dynamic Semantics of Mini-Standard ML. TAPSOFT'87, Vol 2. LNCS, Vol. 250, pp 67–81 Damas, Milner (1982), "Principal type-schemes for functional programs". 9th Symposium on Principles of programming languages (POPL'82) pp. 207–212, ACM Findler, Robert Bruce, and Matthias Felleisen. "Contracts for higher-order functions." ACM SIGPLAN Notices. Vol. 37. No. 9. ACM, 2002. Van Horn, Program Analysis and Understanding
About
Hindley-Milner with contracts
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published