A Swift Playground containing Martin Grabmüller's "Algorithm W Step-by-Step"
/// Playground - noun: a place where people can play | |
/// I am the very model of a modern Judgement General | |
//: # Algorithm W | |
//: In this playground we develop a complete implementation of the classic | |
//: algorithm W for Hindley-Milner polymorphic type inference in Swift. | |
//: ## Introduction | |
//: Type inference is a tricky business, and it is even harder to learn | |
//: the basics, because most publications are about very advanced topics | |
//: like rank-N polymorphism, predicative/impredicative type systems, | |
//: universal and existential types and so on. Since I learn best by | |
//: actually developing the solution to a problem, I decided to write a | |
//: basic tutorial on type inference, implementing one of the most basic | |
//: type inference algorithms which has nevertheless practical uses as the | |
//: basis of the type checkers of languages like ML or Haskell. | |
//: | |
//: The type inference algorithm studied here is the classic Algoritm W | |
//: proposed [by Milner](http://web.cs.wpi.edu/~cs4536/c12/milner-type-poly.pdf). | |
//: For a very readable presentation of this algorithm and possible variations and extensions | |
//: [read also Heeren et al.](https://pdfs.semanticscholar.org/8983/233b3dff2c5b94efb31235f62bddc22dc899.pdf). | |
//: Several aspects of this tutorial are also inspired by [Jones](http://web.cecs.pdx.edu/~mpj/thih/thih.pdf). | |
//: ## Preliminaries | |
//: We start by defining the abstract syntax for both *expressions* | |
//: (of type `Expression`), *types* (`Type`) and *type schemes* | |
//: (`Scheme`). | |
indirect enum Expression : CustomStringConvertible { | |
case evar(String) | |
case lit(Literal) | |
case app(Expression, Expression) | |
case abs(String, Expression) | |
case elet(String, Expression, Expression) | |
case fix(String, String, Expression) | |
var description : String { | |
switch self { | |
case let .evar(name): | |
return name | |
case let .lit(lit): | |
return lit.description | |
case let .elet(x, b, body): | |
return "let \(x) = \(b) in \(body)" | |
case let .app(e1, e2): | |
switch e2 { | |
case .elet(_, _, _): | |
return "\(e1)(\(e2))" | |
case .abs(_, _): | |
return "\(e1)(\(e2))" | |
case .app(_, _): | |
return "\(e1)(\(e2))" | |
default: | |
return "\(e1) \(e2)" | |
} | |
case let .abs(n, e): | |
return "λ \(n) -> \(e)" | |
case let .fix(f, n, e): | |
return "fix \(f) \(Expression.abs(n, e))" | |
} | |
} | |
} | |
enum Literal : CustomStringConvertible { | |
case int(Int) | |
case bool(Bool) | |
var description : String { | |
switch self { | |
case let .int(i): | |
return i.description | |
case let .bool(b): | |
return b ? "True" : "False" | |
} | |
} | |
} | |
indirect enum Type : Equatable, CustomStringConvertible { | |
case typeVar(String) | |
case int | |
case bool | |
case arrow(Type, Type) | |
static func ==(l : Type, r : Type) -> Bool { | |
switch (l, r) { | |
case let (.typeVar(ls), .typeVar(rs)): | |
return ls == rs | |
case (.int, .int): | |
return true | |
case (.bool, .bool): | |
return true | |
case let (.arrow(l1, r1), .arrow(l2, r2)): | |
return l1 == l2 && r1 == r2 | |
default: | |
return false | |
} | |
} | |
var description : String { | |
switch self { | |
case let .typeVar(n): | |
return n | |
case .int: | |
return "Int" | |
case .bool: | |
return "Bool" | |
case let .arrow(.arrow(ss, sr), t2): | |
return "(\(ss) -> \(sr)) -> \(t2)" | |
case let .arrow(t1, t2): | |
return "\(t1) -> \(t2)" | |
} | |
} | |
} | |
struct Scheme : CustomStringConvertible { | |
let vars : [String] | |
let type : Type | |
var description : String { | |
return "∀ \(self.vars.joined(separator: ", ")) . \(self.type)" | |
} | |
} | |
//: We will need to determine the free type variables of a type. The `freeTypeVariables` accessor | |
//: implements this operation, which appears as a requirement of the `TypeCarrier` protocol because | |
//: it will also be needed for type environments (to be defined below). Another useful operation on | |
//: types, type schemes and the like is that of applying a substitution. | |
protocol TypeCarrier { | |
var freeTypeVariables : Set<String> { get } | |
func apply(_ : Substitution) -> Self | |
} | |
extension Type : TypeCarrier { | |
var freeTypeVariables : Set<String> { | |
switch self { | |
case let .typeVar(n): | |
return Set([ n ]) | |
case .int: | |
return Set() | |
case .bool: | |
return Set() | |
case let .arrow(t1, t2): | |
return t1.freeTypeVariables.union(t2.freeTypeVariables) | |
} | |
} | |
func apply(_ s : Substitution) -> Type { | |
// To apply a substitution to a type: | |
switch self { | |
case let .typeVar(n): | |
// If it's a type variable, look it up in the substitution map to | |
// find a replacement. | |
if let t = s[n] { | |
// If we get replaced with ourself we've reached the desired fixpoint. | |
if t == self { | |
return t | |
} | |
// Otherwise keep substituting. | |
return t.apply(s) | |
} | |
return self | |
case .int: | |
// Literals can't be substituted for. | |
return self | |
case .bool: | |
// Literals can't be substituted for. | |
return self | |
case let .arrow(t1, t2): | |
// Substitute down the input and output types of an arrow. | |
return .arrow(t1.apply(s), t2.apply(s)) | |
} | |
} | |
} | |
extension Scheme : TypeCarrier { | |
var freeTypeVariables : Set<String> { | |
return self.type.freeTypeVariables.subtracting(Set(self.vars)) | |
} | |
func apply(_ s : Substitution) -> Scheme { | |
// To apply a substitution to a type scheme, knock out all the things that are no longer | |
// type variables. | |
return Scheme(vars: self.vars, type: self.type.apply(self.vars.reduce(into: s) { (map, k) in | |
map.removeValue(forKey: k) | |
})) | |
} | |
} | |
//: Now we define substitutions, which are finite mappings from type | |
//: variables to types. | |
typealias Substitution = Dictionary<String, Type> | |
//: Type environments, called Γ in the text, are mappings from term | |
//: variables to their respective type schemes. | |
struct Γ { | |
let unEnv : Dictionary<String, Scheme> | |
//: We define several functions on type environments. The operation | |
//: `Γ \ x` removes the binding for `x` from `Γ`. Naturally, we call it | |
//: `remove`. | |
func remove(_ v : String) -> Γ { | |
var dict = self.unEnv | |
dict.removeValue(forKey: v) | |
return Γ(unEnv: dict) | |
} | |
//: The `generalize` function abstracts a type over all type variables | |
//: which are free in the type but not free in the given type environment. | |
// Γ ⊢ e : σ α ∉ free(Γ) | |
// −−−−−−−−−−−−−−−−−------− | |
// Γ ⊢ e : ∀ α . σ | |
func generalize(_ t : Type) -> Scheme { | |
return Scheme(vars: t.freeTypeVariables.subtracting(self.freeTypeVariables).map { $0 }, type: t) | |
} | |
} | |
extension Γ : TypeCarrier { | |
var freeTypeVariables : Set<String> { | |
return self.unEnv.reduce(Set<String>(), { (acc, t) -> Set<String> in | |
return acc.union(t.value.freeTypeVariables) | |
}) | |
} | |
func apply(_ s : Substitution) -> Γ { | |
return Γ(unEnv: Dictionary(self.unEnv.map { (k, v) in (k, v.apply(s)) }, uniquingKeysWith: {$1})) | |
} | |
} | |
enum TypeError : Error { | |
case unificationFailed(Type, Type) | |
case occursCheckFailed(String, Type) | |
case foundUnbound(String) | |
var description : String { | |
switch self { | |
case let .unificationFailed(t1, t2): | |
return "types do not unify: \(t1) vs. \(t2)" | |
case let .occursCheckFailed(u, t): | |
return "'occurs' check failed: \(u) appears in its own type: \(t)" | |
case let .foundUnbound(n): | |
return "unbound variable \(n)" | |
} | |
} | |
} | |
//: Several operations, for example type scheme instantiation, require | |
//: fresh names for newly introduced type variables. This is implemented | |
//: by using an appropriate monad which takes care of generating fresh | |
//: names. It is also capable of passing a dynamically scoped | |
//: environment, error handling and performing I/O, but we will not go | |
//: into details here. | |
final class Inferencer { | |
var supply : Int = 0 | |
//: The instantiation function replaces all bound type variables in a type | |
//: scheme with fresh type variables. | |
//: | |
//: In more creative type systems, this rule acts as a trapdoor that lets | |
//: you insert whatever you want "subtype" to mean - note this is not necessarily the | |
//: subtype in the object-oriented sense, but rather in a type-scheme sense. | |
//: For example, the type `int -> int` is subtype of `∀ a . a -> a` because we | |
//: only intend "subtype" to mean "is more/less specialized than". | |
// Γ ⊢ e : σ′ σ′ ⊑ σ | |
// −−−−−−−−−−−−−−------- | |
// Γ ⊢ e : σ | |
func instantiate(_ s : Scheme) throws -> Type { | |
let nvars = s.vars.map { _ in self.createTypeVariable(named: "τ") } | |
let subst = Substitution(zip(s.vars, nvars), uniquingKeysWith: {$1}) | |
return s.type.apply(subst) | |
} | |
//: This is the unification function for types. | |
func unify(_ t1 : Type, with t2 : Type) throws -> Substitution { | |
switch (t1, t2) { | |
case let (.arrow(l, r), .arrow(l2, r2)): | |
let subst1 = try self.unify(l, with: l2) | |
let subst2 = try self.unify(r.apply(subst1), with: r2.apply(subst1)) | |
return subst1.merging(subst2, uniquingKeysWith: {$1}) | |
case let (.typeVar(tv), ty): | |
return try self.bindTypeVariable(tv, to: ty) | |
case let (ty, .typeVar(tv)): | |
return try self.bindTypeVariable(tv, to: ty) | |
case (.int, .int): | |
return [:] | |
case (.bool, .bool): | |
return [:] | |
default: | |
throw TypeError.unificationFailed(t1, t2) | |
} | |
} | |
//: The function `bindTypeVariable` attempts to bind a type variable to a type | |
//: and return that binding as a subsitution, but avoids binding a | |
//: variable to itself and performs the occurs check. | |
private func bindTypeVariable(_ u : String, to t : Type) throws -> Substitution { | |
if t == .typeVar(u) { | |
return [:] | |
} else if t.freeTypeVariables.contains(u) { | |
throw TypeError.occursCheckFailed(u, t) | |
} else { | |
return [u:t] | |
} | |
} | |
//: ## Main type inference function | |
//: The function `inferType` infers the types for expressions. The type | |
//: environment must contain bindings for all free variables of the | |
//: expressions. The returned substitution records the type constraints | |
//: imposed on type variables by the expression, and the returned type is | |
//: the type of the expression. | |
//: Algorithm W takes a "top-down" (context-free) approach to type inference at the | |
//: expense of failing later and generating more constraints than Algorithm M. As | |
//: presented here, Algorithm W will only fail at the boundary of an application expression | |
//: where function and argument fail to unify. By the time that occurs, type checking of | |
//: both will have been performed, and the resulting error will apply to the entirety of the | |
//: application rather than an erroneous subexpression. | |
//: | |
//: Algorithm W was proven sound and complete [by Milner](http://web.cs.wpi.edu/~cs4536/c12/milner-type-poly.pdf) | |
//: in his original presentation of the type system for which this algorithm was built. | |
private func inferTypeW(of exp : Expression, in env : Γ) throws -> (Substitution, Type) { | |
switch exp { | |
// x : σ ∈ Γ | |
// --−−−−−−− | |
// Γ ⊢ x : σ | |
case let .evar(n): | |
// The only thing we can do is lookup in the context to check if | |
// it contains an entry for the variable we're interested in. If it | |
// doesn't then the variable must be unbound. | |
guard let sigma = env.unEnv[n] else { | |
throw TypeError.foundUnbound(n) | |
} | |
let t = try self.instantiate(sigma) | |
return ([:], t) | |
// We require no premises to infer types for boolean and integer literals. | |
case let .lit(l): | |
switch l { | |
// | |
// --−−−−−−−------ | |
// Γ ⊢ true : bool | |
// | |
// --−−−−−−−------- | |
// Γ ⊢ false : bool | |
case .bool(_): | |
return ([:], Type.bool) | |
// | |
// --−−−−−−−------- | |
// Γ ⊢ [0-9]+ : int | |
case .int(_): | |
return ([:], Type.int) | |
} | |
// Γ , x : τ ⊢ e : τ′ | |
// −−−−−−−−−−−−−−------ | |
// Γ ⊢ λ x . e : τ → τ′ | |
case let .abs(n, body): | |
// Create a new type variable to solve for the abstraction. | |
let tv = self.createTypeVariable(named: "τ") | |
// Setup a new environment that binds the type of the bound variable to our new type variable. | |
var updatedEnv = env.unEnv | |
updatedEnv[n] = Scheme(vars: [], type: tv) | |
// Infer the type of the body. | |
let (bodySubst, bodyTy) = try self.inferTypeW(of: body, in: Γ(unEnv: updatedEnv)) | |
return (bodySubst, .arrow(tv.apply(bodySubst), bodyTy)) | |
// Γ ⊢ e0 : τ → τ′ Γ ⊢ e1 : τ | |
// −--------−−−−−−−−−−−−−−−−−−−− | |
// Γ ⊢ e0(e1) : τ′ | |
case let .app(e0, e1): | |
// Create a new type variable to solve for the application. | |
let tv = self.createTypeVariable(named: "τ") | |
// Infer the type of the function... | |
let (funcSubst, funcTy) = try self.inferTypeW(of: e0, in: env) | |
// Then infer the type of the argument. | |
let (argSubst, argTy) = try self.inferTypeW(of: e1, in: env.apply(funcSubst)) | |
// Now, apply function type to argument type to get back whatever substitutions | |
// we need to perform to yield the correct output type. | |
let subst = try self.unify(funcTy.apply(argSubst), with: .arrow(argTy, tv)) | |
// Yield the output with those substitutions. Dump all the work we've done | |
// up to this point in the context for good measure, too. | |
return (subst.merging(argSubst, uniquingKeysWith: {$1}).merging(funcSubst, uniquingKeysWith: {$1}), tv.apply(subst)) | |
// Γ ⊢ e0 : σ Γ , x : σ ⊢ e1 : τ | |
// −------------−−−−−−−−−−−−−−−−−−−− | |
// Γ ⊢ let x = e0 in e1 : τ | |
case let .elet(x, e0, e1): | |
// First, infer the type of the body of the binding. | |
let (boundSubst, boundTy) = try self.inferTypeW(of: e0, in: env) | |
// Update the context with that information. | |
var updatedEnv = env.unEnv | |
updatedEnv[x] = env.apply(boundSubst).generalize(boundTy) | |
// Now infer the type of the body | |
let (bodySubst, bodyTy) = try self.inferTypeW(of: e1, in: Γ(unEnv: updatedEnv).apply(boundSubst)) | |
return (boundSubst.merging(bodySubst, uniquingKeysWith: {$1}), bodyTy) | |
// This rule (recursion) is not a part of the original system. Nonetheless its typing rules | |
// are easy enough we may as well support it. | |
// | |
// Γ, f : τ ⊢ λ x . e : τ | |
// ---------------------- | |
// Γ ⊢ fix f λx . e : τ | |
case let .fix(f, n, body): | |
// Create a new type variable to solve for the fixpoint. | |
let tv = self.createTypeVariable(named: "τ") | |
// Setup a new environment that binds the type of the recursor. | |
var updatedEnv = env.unEnv | |
updatedEnv[f] = Scheme(vars: [], type: tv) | |
// Infer the type of the lambda. | |
let (lamSubst, lamTy) = try self.inferTypeW(of: .abs(n, body), in: Γ(unEnv: updatedEnv)) | |
let subst = try self.unify(tv.apply(lamSubst), with: lamTy) | |
return (subst.merging(lamSubst, uniquingKeysWith: {$1}), lamTy.apply(subst)) | |
} | |
} | |
//: Algorithm M carries a type constraint from the context of an expression and stops when the | |
//: expression cannot satisfy the current type constraint. | |
//: | |
//: Algorithm M was proven [by Lee and Yi](https://ropas.snu.ac.kr/~kwang/paper/98-toplas-leyi.pdf) to be | |
//: sound and complete. It also has the desirable property that it generates less constraints overall than | |
//: Algorithm W and has better locality of type errors at the expense needing to carry a context through the | |
//: computation. | |
private func inferTypeM(of exp : Expression, in env : Γ, against rho : Type) throws -> Substitution { | |
switch exp { | |
// x : σ ∈ Γ | |
// --−−−−−−− | |
// Γ ⊢ x : σ | |
case let .evar(n): | |
// The only thing we can do is lookup in the context to check if | |
// it contains an entry for the variable we're interested in. If it | |
// doesn't then the variable must be unbound. | |
guard let sigma = env.unEnv[n] else { | |
throw TypeError.foundUnbound(n) | |
} | |
let t = try self.instantiate(sigma) | |
return try self.unify(rho, with: t) | |
// We require no premises to infer types for boolean and integer literals. | |
case let .lit(l): | |
switch l { | |
// | |
// --−−−−−−−------ | |
// Γ ⊢ true : bool | |
// | |
// --−−−−−−−------- | |
// Γ ⊢ false : bool | |
case .bool(_): | |
return try self.unify(rho, with: .bool) | |
// | |
// --−−−−−−− | |
// Γ ⊢ [0-9]+ : int | |
case .int(_): | |
return try self.unify(rho, with: .int) | |
} | |
// Γ , x : τ ⊢ e : τ′ | |
// −−−−−−−−−−−−−−------ | |
// Γ ⊢ λ x . e : τ → τ′ | |
case let .abs(n, body): | |
// Create a new type variable to solve for the abstraction. | |
let inputTV = self.createTypeVariable(named: "τ") | |
let outputTV = self.createTypeVariable(named: "τ") | |
// Check that the type variable we have is an arrow. | |
let arrowSubst = try self.unify(rho, with: .arrow(inputTV, outputTV)) | |
// Setup a new environment that binds the type of the bound variable to our new type variable. | |
var updatedEnv = env.unEnv | |
updatedEnv[n] = Scheme(vars: [], type: inputTV.apply(arrowSubst)) | |
// Infer the type of the body in the updated context. | |
let bodySubst = try self.inferTypeM(of: body, in: Γ(unEnv: updatedEnv).apply(arrowSubst), against: outputTV.apply(arrowSubst)) | |
return bodySubst.merging(arrowSubst, uniquingKeysWith: {$1}) | |
// Γ ⊢ e0 : τ → τ′ Γ ⊢ e1 : τ | |
// −--------−−−−−−−−−−−−−−−−−−−− | |
// Γ ⊢ e0(e1) : τ′ | |
case let .app(e0, e1): | |
// Create a new type variable to solve for the application. | |
let tv = self.createTypeVariable(named: "τ") | |
// | |
let funcSubst = try self.inferTypeM(of: e0, in: env, against: .arrow(tv, rho)) | |
let argSubst = try self.inferTypeM(of: e1, in: env.apply(funcSubst), against: tv.apply(funcSubst)) | |
return argSubst.merging(funcSubst, uniquingKeysWith: {$1}) | |
// Γ ⊢ e0 : σ Γ , x : σ ⊢ e1 : τ | |
// −------------−−−−−−−−−−−−−−−−−−−− | |
// Γ ⊢ let x = e0 in e1 : τ | |
case let .elet(x, e0, e1): | |
let tv = self.createTypeVariable(named: "τ") | |
let boundSubst = try self.inferTypeM(of: e0, in: env, against: tv) | |
// Insert the bound variable into the context. | |
var updatedEnv = env.unEnv | |
updatedEnv[x] = env.generalize(tv.apply(boundSubst)) | |
// Infer the type of the body. | |
let bodySubst = try self.inferTypeM(of: e1, in: Γ(unEnv: updatedEnv).apply(boundSubst), against: rho.apply(boundSubst)) | |
return bodySubst.merging(boundSubst, uniquingKeysWith: {$1}) | |
// Γ, f : τ ⊢ λ x . e : τ | |
// ---------------------- | |
// Γ ⊢ fix f λ x . e : τ | |
case let .fix(f, n, body): | |
// Add the recursor to the environment. | |
var updatedEnv = env.unEnv | |
updatedEnv[f] = Scheme(vars: [], type: rho) | |
// Infer the type of the rest as a lambda term. | |
return try self.inferTypeM(of: Expression.abs(n, body), in: Γ(unEnv: updatedEnv), against: rho) | |
} | |
} | |
typealias Assumptions = [(String, Type)] | |
typealias ConstraintGraph = [Constraint] | |
enum Constraint : CustomStringConvertible { | |
case equivalent(Type, Type) | |
case explicitInstance(Type, Scheme) | |
case implicitInstance(Type, Set<String>, Type) | |
var description : String { | |
switch self { | |
case let .equivalent(t1, t2): | |
return "\(t1) = \(t2)" | |
case let .explicitInstance(t, s): | |
return "\(t) <~ \(s)" | |
case let .implicitInstance(t1, m, t2): | |
return "\(t1) <= (\(m.joined(separator: ","))) \(t2)" | |
} | |
} | |
} | |
//: A cute function that translates the work HM-inference is doing behind the scenes to an explicit | |
//: constraint-based format. | |
func gatherConstraints(for exp : Expression, _ m : Set<String>) -> (Assumptions, ConstraintGraph, Type) { | |
switch exp { | |
case let .evar(n): | |
// If we find a variable, spawn a constraint for it and add it to the list | |
// of assumptions needed to solve this system. | |
let tv = self.createTypeVariable(named: "τ") | |
return ([(n, tv)], [], tv) | |
case .lit(.int(_)): | |
// Literals spawn type variables that are solved immediately by generated constraints. | |
let tv = self.createTypeVariable(named: "τ") | |
return ([], [.equivalent(tv, .int)], tv) | |
case .lit(.bool(_)): | |
// Literals spawn type variables that are solved immediately by generated constraints. | |
let tv = self.createTypeVariable(named: "τ") | |
return ([], [.equivalent(tv, .bool)], tv) | |
case let .app(e0, e1): | |
// For an application, gather the constraints necessary to check the function. | |
let (funcAssump, funcConstr, funcTy) = self.gatherConstraints(for: e0, m) | |
// The gather the constraints needed for the argument. | |
let (argAssump, argConstr, argTy) = self.gatherConstraints(for: e1, m) | |
// Now spawn a type variable for the application itself and take the union of all | |
// generated constraints and assumptions plus a constraint on the output type. | |
let b = self.createTypeVariable(named: "τ") | |
return (funcAssump + argAssump, funcConstr + argConstr + [.equivalent(funcTy, .arrow(argTy, b))], b) | |
case let .abs(x, body): | |
// Spawn a type variable for the abstraction. | |
guard case let .typeVar(vn) = self.createTypeVariable(named: "τ") else { | |
fatalError("Wat?") | |
} | |
// Gather the constraints for the body of the lambda. | |
let (bodyAssump, bodyConstr, bodyTy) = self.gatherConstraints(for: body, m.union([vn])) | |
let b = Type.typeVar(vn) | |
// Replace all the assumptions about the bound variable with fresh ones that are in scope. | |
return (bodyAssump.filter { (n, _) in x != n }, bodyConstr + bodyAssump.filter({ (x2, _) in x == x2 }).map { (x2, t2) in .equivalent(t2, b) }, .arrow(b, bodyTy)) | |
case let .elet(x, e0, e1): | |
// Gather the constraints for the binding. | |
let (bindAssump, bindConstr, bindTy) = self.gatherConstraints(for: e0, m) | |
// The gather them for the body. | |
let (bodyAssump, bodyConstr, bodyTy) = self.gatherConstraints(for: e1, m.subtracting([x])) | |
return ( | |
// Update any assumptions that mention the newly bound variable. | |
bindAssump + bodyAssump.filter { (n, _) in x != n }, | |
bindConstr + bodyConstr + bodyAssump.filter({ (v, _) in x == v }).map { (x2, t2) in .implicitInstance(t2, m, bindTy) }, | |
bodyTy | |
) | |
case let .fix(f, n, body): | |
// Create a new type variable to solve for the fixpoint. | |
guard case let .typeVar(vn) = self.createTypeVariable(named: "τ") else { | |
fatalError("Wat?") | |
} | |
// Gather the constraints for the body of the fixpoint. | |
let (bodyAssump, bodyConstr, bodyTy) = self.gatherConstraints(for: .abs(n, body), m.union([vn])) | |
let b = Type.typeVar(vn) | |
return ( | |
bodyAssump.filter { (n, _) in f != n }, | |
bodyConstr + bodyAssump.filter({ (x2, _) in f == x2 }).map { (x2, t2) in .equivalent(t2, b) }, | |
bodyTy | |
) | |
} | |
} | |
private func createTypeVariable(named prefix : String) -> Type { | |
self.supply += 1 | |
return .typeVar(prefix + self.supply.description) | |
} | |
enum Direction { | |
case topDown | |
case bottomUp | |
} | |
//: This is the main entry point to the type inferencer. It simply calls | |
//: `inferType` and applies the returned substitution to the returned type. | |
func inferType(of e : Expression, direction : Direction = .topDown) throws -> Type { | |
switch direction { | |
case .topDown: | |
let (subst, type) = try self.inferTypeW(of: e, in: Γ(unEnv: [:])) | |
return type.apply(subst) | |
case .bottomUp: | |
let tv = self.createTypeVariable(named: "τ") | |
let subst = try self.inferTypeM(of: e, in: Γ(unEnv: [:]), against: tv) | |
return tv.apply(subst) | |
} | |
} | |
} | |
//: ## Tests | |
//: The following simple expressions (partly taken from [Heeren](https://pdfs.semanticscholar.org/8983/233b3dff2c5b94efb31235f62bddc22dc899.pdf)) | |
//: are provided for testing the type inference function. | |
let e0 : Expression = .elet("id", .abs("x", .evar("x")), .evar("id")) | |
let e1 : Expression = .elet("id", .abs("x", .evar("x")), .app(.evar("id"), .evar("id"))) | |
let e2 : Expression = .elet("id", .abs("x", .elet("y", .evar("x"), .evar("y"))), .app(.evar("id"), .evar("id"))) | |
let e3 : Expression = .elet("id", .abs("x", .elet("y", .evar("x"), .evar("y"))), .app(.app(.evar("id"), .evar("id")), .lit(.int(2)))) | |
let e4 : Expression = .elet("id", .abs("x", .app(.evar("x"), .evar("x"))), .evar("id")) | |
let e5 : Expression = .abs("m", .elet("y", .evar("m"), .elet("x", .app(.evar("y"), .lit(.bool(true))), .evar("y")))) | |
let e6 : Expression = .fix("id", "x", .app(.evar("id"), .evar("x"))) | |
//: This simple set of tests tries to infer the type for the given | |
//: expression. If successful, it prints the expression together with its | |
//: type, otherwise, it prints the error message. | |
for exp in [e0, e1, e2, e3, e4, e5, e6] { | |
do { | |
print(exp) | |
print("Algorithm W: ",try Inferencer().inferType(of: exp, direction: .topDown)) | |
print(Inferencer().gatherConstraints(for: exp, Set()).1) | |
print("Algorithm M: ",try Inferencer().inferType(of: exp, direction: .bottomUp)) | |
print("---------") | |
} catch let e as TypeError { | |
print(e.description) | |
print("---------") | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment