HM型推論をJuliaで実装する

型

mutable struct TType
		name::String
		value::Union{TType, Nothing}
	  types::Vector{TType}
end
 
int = TType("int", nothing, [])
bool = TType("bool", nothing, [])

環境 env

a = typeVar()
env = Dict(
	"true" => bool,
  "false" => bool,
  "id" => fun(a, a), # Type(types=[a, a])
  "zero" => fun(int, bool),
  "not" => fun(bool, bool),
  "left" => fun(a, fun(a, a)),
  "succ" => fun(int, int),
)

Node

abstract type Node end# Nodes
struct
		λ <: Node
    arg::Node
    body::Node
end
 
struct Id <: Node
    name::String
end
 
struct Apply <: Node
    func::Node
    arg::Node
end
 
# let a = 1 in a + 1
struct Let <: Node
    id::Id
    value::Node
    body::Node
end

---

# λxy.x true false
    # (λx (λy. x false) true)
    expr3 = Apply(
        λ(
            Id("x"),
            Apply(
                λ(
                    Id("y"), 
                    Id("x")
                ),
                Id("false")
            ),
        ),
        Id("true"),
    )

doInfer!(env, res, expr)::Type: 項 expr に対して推論を行う

• isa(expr, Id) のとき
  • env から型を参照してコピーして返す
• isa(expr, Apply) のとき
  • 関数の型を infer する(:= funType)
  • パラメーターを infer (:= paramType), 戻り値の型を暫定で置く (:= retType)
  • (funType) と (paramType -> retType) で unify!
  • 戻り値の型を返す
• isa(expr, λ) のとき
  • 引数の型 argType を作り, env と ref に追加
  • 値部を推論して argType -> retType を返す

unify!(type1, type2): 型のmguを求める

• どちらも型変数じゃなかったら
  • 型が一致しているかチェック
  • typeの各要素に対して unify!
• どちらかが型変数
  • 一方に対して型代入を行う

具体例①

(id 1)

1. (id: ? 1: ?): ? を infer
   1. id を infer
      1. envから id: a -> a をコピー, id: b -> b
   2. 1 を infer -> 1: int
   3. (id 1) に暫定の型 c をつける -> (id: b -> b 1: int): c
      1. パラメーターの型は int なので id: int -> c
   4. unify(b -> b, int -> c)
      1. b = int
      2. c = int

具体例②

(λx. (λy.x false) true)

• (λx: ?. (λy: ?.x: ? false: ?): ? true: ?): ? を infer
  • λx. (λy.x false) を infer
    • x を型 b とする
    • (λy.x false) を infer
      • λy.x を infer
        • y を型 c とする
          • x を infer = b
          • (λy.x false) を型 d とする
          • unify(bool -> d, c -> b) -> c = bool, b = d

具体例②

1. (λx. (λy.x false) true) を infer

• (λx. (λy.x false) true) を 型 e とする
  • unify(bool -> e, d -> d)
    • d = bool
    • e = bool

論理学

• 二階述語論理

ラムダ計算

• System F: λ に全称量化(パラメタ多相)を導入したもの
  • (カリー＝ハワード同型 の下で(???)) 二階述語論理に対応するらしい
• $F_{\le }$: 派生型を導入したもの(Subtyping の概念)

型推論

• 線形時相論理 (Linear Temporal Logic, LTL)
  • 時相論理 を用いて並行システムの検証とかできるらしい(計算木論理 の話)

参考文献

• Hindley-Milner型推論をCで実装した話 - free(malloc(sizeof(MRM)));