Algorithm W and Algorithm M in F#

What is this?

This is a type inference implementation of both Algorithm W and Algorithm M written in F#.

Referenced articles:

1. Algorithm W Step by Step
2. Proofs about a Folklore Let-Polymorphic Type Inference Algorithm

The method of article 1 was implemented with care not to change it as much as possible.

Example

// NuGet package is available.
#r "nuget: TypeInferencer"

open TypeInferencer

// `let id = fun x -> x in id id`
let expr =
    ELet("id",
        EAbs("x", EVar "x"),
        EApp(EVar "id", EVar "id"))

// Type environment (is empty)
let env = TypeEnv []

// Do inferring with `Algorithm W` (top-down)
let actual = infer TopDown env expr

// Pretty printing
printfn "Expression: %s" (show expr)
printfn "Actual: %s" (show actual)

Results:

Expression: let id = fun x -> x in id id
Actual: a3 -> a3

---

How to play it

A playing guide is here:

• English:
  • Markdown (Inside this repository)
  • Rendered pdf (pandoc/wkhtmltopdf)
• Japanese:
  • Markdown (Inside this repository)
  • Rendered pdf (pandoc/wkhtmltopdf)

---

Basic interface

Well-defined types

AST expression type:

type public Lit =
    | LInt of value:int32
    | LBool of value:bool

type public Exp =
    | EVar of name:string
    | ELit of literal:Lit
    | EApp of func:Exp * arg:Exp
    | EAbs of name:string * expr:Exp
    | ELet of name:string * expr:Exp * body:Exp
    | EFix of func:string * name:string * expr:Exp

Result type type:

type public Type =
    | TVar of name:string
    | TInt
    | TBool
    | TFun of parameterType:Type * resultType:Type

The inferencer:

type public InferAlgorithm =
    | TopDown
    | BottomUp

[<AutoOpen>]
module public Inferencer =
    let infer: InferAlgorithm -> TypeEnv -> Exp -> Type

---

Requirements

• F# 6.0 or upper
• NuGet package supported platforms:
  • net8.0
  • net7.0
  • net6.0
  • net5.0
  • netcoreapp3.1
  • netcoreapp2.1
  • netstandard2.1
  • netstandard2.0
  • net48
  • net461

License

Copyright (c) Kouji Matsui (@kozy_kekyo, @kekyo2)

License under Apache-v2.