Bidirectional Typechecking を実装してみた。

はじめに

Desk言語ではBidirectional Typechecking のテクニックを使っているという話を聞いてよくわからないので調べてみて最も基本的な単相の双方向型検査器をPrologで書いてみました:

% Implementation of Bidirectional Typing Rules: A Tutorial
% http://davidchristiansen.dk/tutorials/bidirectional.pdf
% t ::= bool | t -> t | [t]
% b ::= true | false
% e ::= b | x | e$e | λ(x,e) | if(e,e,e) | e:t | [e|e] | []
% t は型でboolがbool型、t->tが関数型、[t]がリスト型です。
% bはbool値でtrueまたはfalseです。
% eは式を表し、bがbool値、xが変数、e$eが関数適用、λ(x,e)が関数、
% if(e,e,e)がif式、e:tが型注釈、[e|e]がリストのcons、[]が空リストです。
:- op(650,xfy,$), op(600,xfy,[⇐,⇒,⊢]), op(1200,xfx,if).
term_expansion(A if B, A :- B).
% check type
Γ⊢λ(X,E)  ⇐ (T2->T1) if [X:T2|Γ]⊢E ⇐ T1.
Γ⊢[E1|E2] ⇐ [T1]     if Γ⊢E1 ⇐ T1, Γ⊢E2 ⇐ [T1].
_⊢[]      ⇐ [_].
Γ⊢E       ⇐ T1       if Γ⊢E ⇒ T1.
% infer type
_⊢true        ⇒bool.
_⊢false       ⇒bool.
Γ⊢X           ⇒T1   if member(X:T1,Γ).
Γ⊢(E1:T1)     ⇒T1   if Γ⊢E1⇐T1.
Γ⊢(E1$E2)     ⇒T1   if Γ⊢E1⇒(T2->T1), Γ⊢E2⇐T2.
Γ⊢if(E1,E2,E3)⇒T1   if Γ⊢E1⇐bool,     Γ⊢E2⇒T1, Γ⊢E3⇒T1.
Γ⊢[E1|E2]     ⇒[T1] if Γ⊢E1⇒T1,       Γ⊢E2⇐[T1].

test(E,ET):- []⊢E⇒T,!,T=ET.
:- test(λ(x, if(x, false, true)):(bool->bool),bool->bool).
:- test([true, true, false],[bool]).
:- test([([]:[bool]),[],[]],[[bool]]).
:- halt.

構文

t ::=       (型)
  bool      (bool型)
  t -> t    (関数型)
  [t]       (リスト型)
b ::=       (bool値)
  true      (真)
  false     (儀)
e ::=       (式)
  b         (bool値)
  x         (変数)
  e$e       (関数適用)
  λ(x,e)    (関数)
  if(e,e,e) (if式)
  e:t       (型注釈)
  [e|e]     (cons)
  []        (空リスト)

単相の双方向型検査器は、単一化をすることなく型推論ができたりできなかったりします。 ⊢e⇐t の形の規則は型推論が不可能な規則であり型を入力する型検査器であることを表します。 ⊢e⇒t の形の規則は型推論が可能な規則であり型が出力されることを表します。 型が推論できない場合は型注釈を付けることで型推論が可能な式にできます。