Prolog でわかる TAPL 12日目 - 第Ⅵ部 高階の型システム (1)

ユーピテル

ユーピテルもしくはユッピテル（ラテン語: Jūpiter, Juppiter, 古典綴 IV́PITER, IVPPITER）は、ローマ神話の主神である[1]。また最高位の女神であるユーノーの夫である[1]。 時として女性化・女体化して女神となり、その姿がディアーナであるという言い伝えもある。

日本語では長母音を省略してユピテルとも呼ばれ、英語読みのジュピターでも呼ばれている[1]。

ラテン語のユーピテルは、古ラテン語の呼格 Jou と pater（父）の合成語として生じた呼称とされる。比較言語学の研究により、Jou-pater はインド＝ヨーロッパ祖語の Dyēus-pətēr の呼格 Dyēu-pəter （ディェーウ＝パテル、父なるディェーウス〔天空神〕よ）からの派生と推定される、と主張されている。ラテン名の属格は Jovis（ヨウィス）となり[2]、斜格の語幹 Jov- に基づく英語の別名 Jove は詩語などに使用される。本来は天空の神、転じて気象現象（特に雷）を司る神とされた[1]。

後にギリシア神話のゼウスと同一視される[1]。実際、ともに古いインド・ヨーロッパ語系神話の天空神に起源を有する。『リグ・ヴェーダ』のディヤウスや北欧神話のテュールとも起源を同じくするとされている。

高階多相な型システムの型の型がカインドと呼ばれます。より上層のお話がオメガな世界なのです。
高階多相な世界は曼荼羅のような上には上があったーっという話なわけですな。

TAPL29,30 λω,Fω

図29-1.型演算子とカインド付け(λω)

→ ⇒ λ→(図9-1)の拡張

構文

t ::=       項：
x         変数
λx:T.t    ラムダ抽象
t t       関数適用
v ::=       値：
λx:T.t    ラムダ抽象値
T ::=       型：
X         型変数
λX::K.T   演算子抽象
T T       演算子適用
T->T      関数の型
Γ ::=       文脈：
∅         空の文脈
Γ,x:T     項変数の束縛
Γ,X::K    型変数の束縛
K ::=       カインド:
*         真の型のカインド
K=>K      演算子のカインド

評価 t ==> t'

t1 ==> t1'
------------------------------- (E-App1)
t1 t2 ==> t1' t2

t2 ==> t2'
------------------------------- (E-App2)
v1 t2 ==> v1 t2'

(λx:T11.t12) v2 ==> [x->v2]t12  (E-AppAbs)

カインド付け Γ|- T :: K

X::K ∈ Γ
------------------------------------ (K-TVar)
Γ |- X ::K

Γ,X::K1 |- T2::K2
------------------------------------ (K-Abs)
Γ |- λX::K1.T2 :: K1=>K2

Γ |- T1 :: K11 => K12   Γ |- T2::K11
------------------------------------ (K-App)
Γ |- T1 T2 :: K1=>K12

Γ |- T1 :: *   Γ |- T2 :: *
------------------------------------ (K-Arrow)
Γ |- T1->T2 :: *

型等価関係 S ≡ T

T ≡ T                 (Q-Refl)

T ≡ S
--------------------- (Q-Symm)
S ≡ T

S ≡ U   U ≡ T
--------------------- (Q-Trans)
S ≡ T

S1 ≡ T1   S2 ≡ T2
--------------------- (Q-Arrow)
S1->S2 ≡ T1->T2

S2 ≡ T2
--------------------- (Q-Abs)
λX::K1.S2 ≡ λX::K1.T2

S1 ≡ T1   S2 ≡ T2
--------------------- (Q-App)
S1 S2 ≡ T1 T2

(λX::K11.T12)T2 ≡ [X|->T2]T12
                    (Q-AppAbs)

型付け Γ ⊢ t : T

x : T ∈ Γ
------------------------------ (T-Var)
Γ ⊢ x : T

Γ ⊢ T1 :: *   Γ,x:T1 ⊢ t2 : T2
------------------------------ (T-Abs)
Γ ⊢ λx:T1.t2 : T1 -> T2

Γ ⊢ t1 : T11 -> T12
Γ ⊢ t2 : T11
------------------------------ (T-App)
Γ ⊢ t1 t2 : T12

Γ ⊢ t : S   S == T   Γ ⊢ T : *
------------------------------ (T-Eq)
Γ ⊢ t : T

図30-1.高階多相ラムダ計算(Fω)

→ ∀ ⇒ λω(図29-1)とSystem F(図23-1)の拡張

構文

t ::=       項：
  x         変数
  λx:T.t    ラムダ抽象
  t t       関数適用
  λX::K.t   型抽象
  t[T]      型適用

v ::=       値：
  λx:T.t    ラムダ抽象値
  λX::K.t   型抽象値

T ::=       型：
  X         型変数
  T->T      関数の型
  ∀X::K.T  全称型
  λX::K.T   演算子抽象
  T T       演算子適用

Γ ::=       文脈：
  ∅         空の文脈
  Γ,x:T     項変数の束縛
  Γ,X::K    型変数の束縛

K ::=       カインド:
  *         真の型のカインド
  K=>K      演算子のカインド

図30-2.高階存在型

→ ∀ ∃ ⇒ Fω(図30-1)と図24-1の拡張

新しい構文形式

T ::= …    型：
　{∃X::K,T}  存在型

新しい評価規則 t ==> t’

let {X,x}=({*T11,v12}as T1) in t2
  ⇒ [X->T11][x->v12]t2              (E-UnpackPack)

t12 ⇒ t12’
------------------------------------ (E-Pack)
{*T11,t12} as T1 ⇒{*T11,t12’} as T1

新しいカインド付け規則 Γ ⊢ T :: K

Γ,X::K1 ⊢ T2 :: *
------------------------------------ (K-Some)
Γ ⊢ {∃X::K1,T2} :: *

新しい型等価関係の規則 S ≡ T

S2 ≡ T2
------------------------------------ (Q-Some)
{∃X::K1,S2} ≡ {∃X::K1,T2}

新しい型付け規則 Γ ⊢ t : T

Γ ⊢ t2 : [X -> U] T2
Γ ⊢ {∃X::K1,T2} :: *
------------------------------------ (T-Pack)
Γ ⊢ {*U,t2} as {∃X::K1,T2}

Γ ⊢ t1 : {∃X::K11,T12}
Γ,X::K11,x:T12 ⊢ t2 : T2
------------------------------------ (T-Unpack)
Γ ⊢ let {X,x}=t1 in t2 : T2

図30-3.型の並行簡約

並行簡約 S ⇛ T

T ⇛ T                              (QR-REFL)

S1 ⇛ T1   S2 ⇛ T2
---------------------------------- (QR-Arrow)
S1 -> S2 ⇛ T1 -> T2

S2 ⇛ T2
---------------------------------- (QR-All)
∀X::K1.S2 ⇛ ∀X::K1.S2

S2 ⇛ T2
---------------------------------- (QR-Abs)
λX::K1.S2 ⇛ λX::K1.T2

S1 ⇛ T1   S2 ⇛ T2
---------------------------------- (QR-App)
S1 S2 ⇛ T1 T2

S12 ⇛ T12   S2 ⇛ T2 
---------------------------------- (QR-AppAbs)
(λX::K11.S12) S2 ⇉ [X ↦ T2]T12

実装

• fomega +kind
• fullomega フル型演算とカインド、高階多相 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+ref+all+some+kind(29,30章)

fomega.pl

プログラムの全体を見る

fomega.pl

:- discontiguous((\-)/2).
:- discontiguous((/-)/2).
:- op(1050, xfy, [=>]).
:- op(920, xfx, [==>, ==>>, <:]).
:- op(910, xfx, [/-, \-]).
:- op(600, xfy, [::]).
:- op(500, yfx, [$, !, tsubst, tsubst2, subst, subst2, tmsubst, tmsubst2]).
:- style_check(- singleton). 

% ------------------------   SYNTAX  ------------------------

:- use_module(rtg).

syntax(x). x(X) :- atom(X), (sub_atom(X, 0, 1, _, P), char_type(P, lower) ; P = '_').  % 識別子:
syntax(tx). tx(TX) :- atom(TX), sub_atom(TX, 0, 1, _, P), char_type(P, upper).  % 型変数:

k ::=                     % カインド:
      '*'                 % 真の型のカインド
    | (k => k)            % 演算子のカインド
    .
t ::=                     % 型:
      tx                  % 型変数
    | (t -> t)            % 関数の型
    | (all(tx :: k) => t) % 全称型
    | (fn(tx :: k) => t)  % 型抽象
    | t $ t               % 関数適用
    .
m ::=                     % 項:
      x                   % 変数
    | (fn(x : t) -> m)    % ラムダ抽象
    | m $ m               % 関数適用
    | (fn(tx <: k) => m)  % 型抽象
    | m![t]               % 型適用
    .
v ::=                     % 値:
      (fn(x : t) -> m)    % ラムダ抽象 
    | (fn(tx <: k) => m)  % 型抽象
    . 

% ------------------------   SUBSTITUTION  ------------------------

J![(J -> S)] tsubst S                     :- tx(J).
X![(J -> S)] tsubst X                     :- tx(X).
(T1 -> T2)![(J -> S)] tsubst (T1_ -> T2_) :- T1![(J -> S)] tsubst T1_, T2![(J -> S)] tsubst T2_.
(all(TX :: K) => T2)![(J -> S)] tsubst (all(TX :: K) => T2_)
                                          :- T2![TX, (J -> S)] tsubst2 T2_.
(fn(TX :: K) => T2)![(J -> S)] tsubst (fn(TX :: K) => T2_)
                                          :- T2![TX, (J -> S)] tsubst2 T2_.
T1 $ T2![(J -> S)] tsubst (T1_ $ T2_)     :- T1![(J -> S)] tsubst T1_, T2![(J -> S)] tsubst T2_.
T![(J -> S)] tsubst T_                    :- writeln(error : T![(J -> S)] tsubst T_), halt.
T![X, (X -> S)] tsubst2 T.
T![X, (J -> S)] tsubst2 T_                :- T![(J -> S)] tsubst T_. 

J![(J -> M)] subst M                 :- x(J).
(fn(X1 : T1) -> M2)![(J -> M)] subst (fn(X1 : T1) -> M2_)
                                     :- M2![X1, (J -> M)] subst2 M2_.
M1 $ M2![(J -> M)] subst (M1_ $ M2_) :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
(fn(TX <: K) => M2)![(J -> M)] subst (fn(TX <: K) => M2_)
                                     :- M2![(J -> M)] subst M2_.
M1![T2]![(J -> M)] subst (M1_![T2])  :- M1![(J -> M)] subst M1_.
M1![(J -> M)] subst M1.
A![(J -> M)] subst B                 :- writeln(error : A![(J -> M)] subst B), fail.
T![X, (X -> M)] subst2 T.
T![X, (J -> M)] subst2 T_            :- T![(J -> M)] subst T_.

X![(J -> S)] tmsubst X                 :- x(X).
(fn(X : T1) -> M2)![(J -> S)] tmsubst (fn(X : T1_) -> M2_)
                                       :- T1![(J -> S)] tsubst T1_, M2![(J -> S)] tmsubst M2_.
M1 $ M2![(J -> S)] tmsubst (M1_ $ M2_) :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
(fn(TX <: K) => M2)![(J -> S)] tmsubst (fn(TX <: K) => M2_)
                                       :- M2![TX, (J -> S)] tmsubst2 M2_.
M1![T2]![(J -> S)] tmsubst (M1_![T2_]) :- M1![(J -> S)] tmsubst M1_, T2![(J -> S)] tsubst T2_.
T![X, (X -> S)] tmsubst2 T.
T![X, (J -> S)] tmsubst2 T_            :- T![(J -> S)] tmsubst T_.

% ------------------------   EVALUATION  ------------------------

Γ /- (fn(X : T11) -> M12) $ V2 ==> R   :- v(V2), M12![(X -> V2)] subst R.
Γ /- V1 $ M2 ==> V1 $ M2_              :- v(V1), Γ /- M2 ==> M2_.
Γ /- M1 $ M2 ==> M1_ $ M2              :- Γ /- M1 ==> M1_.
Γ /- (fn(X <: _) => M11)![T2] ==> M11_ :- M11![(X -> T2)] tmsubst M11_.
Γ /- M1![T2] ==> M1_![T2]              :- Γ /- M1 ==> M1_. 

Γ /- M ==>> M_ :- Γ /- M ==> M1, Γ /- M1 ==>> M_.
Γ /- M ==>> M. 

% ------------------------   KINDING  ------------------------

compute(Γ, (fn(X :: _) => T12) $ T2, T) :- T12![(X -> T2)] tsubst T.

simplify(Γ, T1 $ T2, T_)                :- simplify(Γ, T1, T1_), simplify2(Γ, T1_ $ T2, T_).
simplify(Γ, T, T_)                      :- simplify2(Γ, T, T_).
simplify2(Γ, T, T_)                     :- compute(Γ, T, T1), simplify(Γ, T1, T_).
simplify2(Γ, T, T).

Γ /- S = T                                          :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ /- S_ == T_.
Γ /- X == X                                         :- tx(X).
Γ /- (S1 -> S2) == (T1 -> T2)                       :- Γ /- S1 = T1, Γ /- S2 = T2.
Γ /- (all(TX1 :: K1) => S2) == (all(_ :: K2) => T2) :- K1 = K2, [TX1-name|Γ] /- S2 = T2.
Γ /- (fn(TX1 :: K1) => S2) == (fn(_ :: K2) => T2)   :- K1 = K2, [TX1-name|Γ] /- S2 = T2.
Γ /- S1 $ S2 == T1 $ T2                             :- Γ /- S1 = T1, Γ /- S2 = T2.

Γ /- T :: K                            :- Γ \- T :: K, !.
Γ /- T :: K                            :- writeln(error : kindof(T, K)), fail.
Γ \- X :: '*'                          :- tx(X), \+ member(X - _, Γ).
Γ \- X :: K                            :- tx(X), !, member(X :: K, Γ).
Γ \- (T1 -> T2) :: '*'                 :- !, Γ /- T1 :: '*', Γ /- T2 :: '*'.
Γ \- (all(TX :: K1) => T2) :: '*'      :- !, [TX :: K1 | Γ] /- T2 :: '*'.
Γ \- (fn(TX :: K1) => T2) :: (K1 => K) :- !, [TX :: K1 | Γ] /- T2 :: K.
Γ \- T1 $ T2 :: K12                    :- !, Γ /- T1 :: (K11 => K12), Γ /- T2 :: K11.
Γ \- T :: '*'. 

% ------------------------   TYPING  ------------------------ *)

Γ /- X : T                            :- x(X), !, member(X : T, Γ).
Γ /- (fn(X : T1) -> M2) : (T1 -> T2_) :- Γ /- T1 :: '*', [X : T1 | Γ] /- M2 : T2_.
Γ /- M1 $ M2 : T12                    :- Γ /- M1 : T1, simplify(Γ, T1, (T11 -> T12)),
                                         Γ /- M2 : T2, Γ /- T11 = T2.
Γ /- (fn(TX <: K1) => M2) : (all(TX :: K1) => T2)
                                      :- [TX :: K1 | Γ] /- M2 : T2.
Γ /- M1![T2] : T12_                   :- Γ /- T2 :: K2, Γ /- M1 : T1,
                                         simplify(Γ, T1, (all(X :: K2) => T12)),
                                         T12![(X -> T2)] tsubst T12_.
Γ /- M : _                            :- writeln(error : typeof(M)), !, halt.

show(X : T)  :- format('~w : ~w\n', [X, T]).
show(X :: K) :- format('~w :: ~w\n', [X, K]).

run(X : T, Γ, [X:T|Γ])   :- x(X), t(T), show(X : T).
run(X :: K, Γ, [X::K|Γ]) :- tx(X), k(K), show(X :: K).
run(M, Γ, Γ)             :- !, m(M), !, Γ /- M : T, Γ /- M ==>> M_, !, writeln(M_ : T), !.

run(Ls) :- foldl(run, Ls, [], Γ). 

% ------------------------   TEST  ------------------------

% lambda X. lambda x:X. x;
:- run([(fn('X' <: '*') => fn(x : 'X') -> x)]). 
% (lambda X. lambda x:X. x) [All X.X->X]; 
:- run([(fn('X' <: '*') => fn(x : 'X') -> x)![(all('X' :: '*') => 'X' -> 'X')]]). 
% T :: *;
% k : T;
:- run(['T' :: '*', k : 'T']). 
% TT :: * => *;
% kk : TT;
:- run(['TT' :: ('*' => '*'), kk : 'TT']). 
% T :: *;
% x : (lambda X::*=>*.T) T;
:- run(['T' :: '*', x : (fn('X' :: ('*' => '*')) => 'T') $ 'T']).

:- halt.

fullomega.pl

プログラムの全体を見る

fullomega.pl

:- discontiguous((\-)/2).
:- discontiguous((/-)/2).
:- op(1100, xfy, [in]).
:- op(1050, xfy, [=>]).
:- op(920, xfx, [==>, ==>>, <:]).
:- op(910, xfx, [/-, \-]).
:- op(600, xfy, [::, as]).
:- op(500, yfx, [$, !, tsubst, tsubst2, subst, subst2, tmsubst, tmsubst2]).
:- op(400, yfx, [#]).
:- style_check(- singleton). 

% ------------------------   SYNTAX  ------------------------

:- use_module(rtg).

w ::= bool | nat | unit | float | string | true | false | error. % キーワード:
syntax(x). x(X) :- \+ w(X), atom(X), sub_atom(X, 0, 1, _, P), (char_type(P, lower) ; P = '_'). % 識別子:
syntax(tx). tx(TX) :- atom(TX), sub_atom(TX, 0, 1, _, P), char_type(P, upper). % 型変数:
syntax(floatl). floatl(F) :- float(F).     % 浮動小数点数
syntax(stringl). stringl(F) :- string(F).  % 文字列
syntax(integer).                           % 整数
syntax(l). l(L) :- atom(L) ; integer(L).   % ラベル
list(A) ::= [] | [A | list(A)].            % リスト

k ::=                       % カインド:
    '*'                     % 真の型のカインド
    | (k => k)              % 演算子のカインド
    .
t ::=                       % 型:
    bool                    % ブール値型
    | nat                   % 自然数型
    | unit                  % Unit型
    | float                 % 浮動小数点数型
    | string                % 文字列型
    | tx                    % 型変数
    | (t -> t)              % 関数の型
    | {list(l : t)}         % レコードの型
    | ref(t)                % 参照セルの型
    | (all(tx :: k) => t)   % 全称型
    | {some(tx :: k), t}    % 存在型
    | (fn(tx :: k) => t)    % 型抽象
    | t $ t                 % 関数適用
    .
m ::=                       % 項:
    true                    % 真
    | false                 % 偽
    | if(m, m, m)           % 条件式
    | 0                     % ゼロ
    | succ(m)               % 後者値
    | pred(m)               % 前者値
    | iszero(m)             % ゼロ判定
    | unit                  % 定数unit
    | floatl                % 浮動小数点数値
    | m * m                 % 浮動小数点乗算
    | stringl               % 文字列定数
    | x                     % 変数
    | (fn(x : t) -> m)      % ラムダ抽象
    | m $ m                 % 関数適用
    | (let(x) = m in m)     % let束縛
    | fix(m)                % mの不動点
    | inert(t) | m as t     % 型指定
    | {list(l = m)}         % レコード
    | m # l                 % 射影
    | loc(integer)          % ストアでの位置
    | ref(m)                % 参照の生成
    | '!'(m)                % 参照先の値の取り出し
    | m := m                % 破壊的代入
    | {(t, m)} as t         % パッケージ化
    | (let(tx, x) = m in m) % アンパッケージ化
    | (fn(tx <: k) => m)    % 型抽象
    | m![t]                 % 型適用
    .
n ::=                       % 数値:
    0                       % ゼロ
    | succ(n)               % 後者値
    .
v ::=                       % 値:
    true                    % 真
    | false                 % 偽
    | n                     % 数値
    | unit                  % 定数unit
    | floatl                % 浮動小数点数値
    | stringl               % 文字列定数
    | (fn(x : t) -> m)      % ラムダ抽象
    | {list(l = v)}         % レコード
    | loc(integer)          % ストアでの位置
    | {(t, v)} as t         % パッケージ化
    | (fn(tx <: k) => m)    % 型抽象
    . 

% ------------------------   SUBSTITUTION  ------------------------

bool![(J -> S)] tsubst bool.
nat![(J -> S)] tsubst nat.
unit![(J -> S)] tsubst unit.
float![(J -> S)] tsubst float.
string![(J -> S)] tsubst string.
J![(J -> S)] tsubst S                                          :- tx(J).
X![(J -> S)] tsubst X                                          :- tx(X).
(T1 -> T2)![(J -> S)] tsubst (T1_ -> T2_)                      :- T1![(J -> S)] tsubst T1_, T2![(J -> S)] tsubst T2_.
{Mf}![(J -> S)] tsubst {Mf_}                                   :- maplist([L : T, L : T_] >> (T![(J -> S)] tsubst T_), Mf, Mf_).
ref(T1)![(J -> S)] tsubst ref(T1_)                             :- T1![(J -> S)] tsubst T1_.
(all(TX :: K1) => T2)![(J -> S)] tsubst (all(TX :: K1) => T2_) :- T2![TX, (J -> S)] tsubst2 T2_.
{some(TX :: K1), T2}![(J -> S)] tsubst {some(TX :: K1), T2_}   :- T2![TX, (J -> S)] tsubst2 T2_.
(fn(TX :: K1) => T2)![(J -> S)] tsubst (fn(TX :: K1) => T2_)   :- T2![TX, (J -> S)] tsubst2 T2_.
T1 $ T2![(J -> S)] tsubst (T1_ $ T2_)                          :- T1![(J -> S)] tsubst T1_, T2![(J -> S)] tsubst T2_.
A![(J -> S)] tsubst _                                          :- writeln(error : tsubst(J, S, A)), fail.
T![X, (X -> S)] tsubst2 T.
T![X, (J -> S)] tsubst2 T_                                     :- T![(J -> S)] tsubst T_.

true![(J -> M)] subst true.
false![(J -> M)] subst false.
if(M1, M2, M3)![(J -> M)] subst if(M1_, M2_, M3_)                  :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_, M3![(J -> M)] subst M3_.
0![(J -> M)] subst 0.
succ(M1)![(J -> M)] subst succ(M1_)                                :- M1![(J -> M)] subst M1_.
pred(M1)![(J -> M)] subst pred(M1_)                                :- M1![(J -> M)] subst M1_.
iszero(M1)![(J -> M)] subst iszero(M1_)                            :- M1![(J -> M)] subst M1_.
unit![(J -> M)] subst unit.
F1![(J -> M)] subst F1                                             :- float(F1).
M1 * M2![(J -> M)] subst M1_ * M2_                                 :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
X![(J -> M)] subst X                                               :- string(X).
J![(J -> M)] subst M                                               :- x(J).
X![(J -> M)] subst X                                               :- x(X).
(fn(X : T1) -> M2)![(J -> M)] subst (fn(X : T1) -> M2_)            :- M2![X, (J -> M)] subst2 M2_.
M1 $ M2![(J -> M)] subst (M1_ $ M2_)                               :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
(let(X) = M1 in M2)![(J -> M)] subst (let(X) = M1_ in M2_)         :- M1![(J -> M)] subst M1_, M2![X, (J -> M)] subst2 M2_.
fix(M1)![(J -> M)] subst fix(M1_)                                  :- M1![(J -> M)] subst M1_.
inert(T1)![(J -> M)] subst inert(T1).
(M1 as T1)![(J -> M)] subst (M1_ as T1)                            :- M1![(J -> M)] subst M1_.
{Mf}![(J -> M)] subst {Mf_}                                        :- maplist([L = Mi, L = Mi_] >> (Mi![(J -> M)] subst Mi_), Mf, Mf_).
M1 # L![(J -> M)] subst M1_ # L                                    :- M1![(J -> M)] subst M1_.
ref(M1)![(J -> M)] subst ref(M1_)                                  :- M1![(J -> M)] subst M1_.
'!'(M1)![(J -> M)] subst '!'(M1_)                                  :- M1![(J -> M)] subst M1_.
(M1 := M2)![(J -> M)] subst (M1_ := M2_)                           :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
loc(L)![(J -> M)] subst loc(L).
(fn(TX <: K1) => M2)![(J -> M)] subst (fn(TX <: K1) => M2_)        :- M2![(J -> M)] subst M2_.
M1![T2]![(J -> M)] subst (M1_![T2])                                :- M1![(J -> M)] subst M1_.
({(T1, M2)} as T3)![(J -> M)] subst ({(T1, M2_)} as T3)            :- M2![(J -> M)] subst M2_.
(let(TX, X) = M1 in M2)![(J -> M)] subst (let(TX, X) = M1_ in M2_) :- M1![X, (J -> M)] subst2 M1_, M2![X, (J -> M)] subst2 M2_.
S![(J -> M)] subst _                                               :- writeln(error : subst(J, M, S)), fail.
S![J, (J -> M)] subst2 S.
S![X, (J -> M)] subst2 M_                                          :- S![(J -> M)] subst M_.

true![(J -> S)] tmsubst true.
false![(J -> S)] tmsubst false.
if(M1, M2, M3)![(J -> S)] tmsubst if(M1_, M2_, M3_)           :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_,
                                                                 M3![(J -> S)] tmsubst M3_.
0![(J -> S)] tmsubst 0.
succ(M1)![(J -> S)] tmsubst succ(M1_)                         :- M1![(J -> S)] tmsubst M1_.
pred(M1)![(J -> S)] tmsubst pred(M1_)                         :- M1![(J -> S)] tmsubst M1_.
iszero(M1)![(J -> S)] tmsubst iszero(M1_)                     :- M1![(J -> S)] tmsubst M1_.
unit![(J -> S)] tmsubst unit.
F1![(J -> S)] tmsubst F1                                      :- float(F1).
M1 * M2![(J -> S)] tmsubst M1_ * M2_                          :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
X![(J -> S)] tmsubst X                                        :- string(X).
X![(J -> S)] tmsubst X                                        :- x(X).
(fn(X : T1) -> M2)![(J -> S)] tmsubst (fn(X : T1_) -> M2_)    :- T1![(J -> S)] tsubst T1_, M2![(J -> S)] tmsubst M2_.
M1 $ M2![(J -> S)] tmsubst (M1_ $ M2_)                        :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
(let(X) = M1 in M2)![(J -> S)] tmsubst (let(X) = M1_ in M2_)  :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
fix(M1)![(J -> S)] tmsubst fix(M1_)                           :- M1![(J -> S)] tmsubst M1_.
inert(T1)![(J -> S)] tmsubst inert(T1).
(M1 as T1)![(J -> S)] tmsubst (M1_ as T1_)                    :- M1![(J -> S)] tmsubst M1_, T1![(J -> S)] tsubst T1_.
{Mf}![(J -> S)] tmsubst {Mf_}                                 :- maplist([L = Mi, L = Mi_] >> (Mi![(J -> S)] tmsubst Mi_), Mf, Mf_).
M1 # L![(J -> S)] tmsubst M1_ # L                             :- M1![(J -> S)] tmsubst M1_.
ref(M1)![(J -> S)] tmsubst ref(M1_)                           :- M1![(J -> S)] tmsubst M1_.
'!'(M1)![(J -> S)] tmsubst '!'(M1_)                           :- M1![(J -> S)] tmsubst M1_.
(M1 := M2)![(J -> S)] tmsubst (M1_ := M2_)                    :- M2![(J -> S)] tmsubst M2_, M2![(J -> S)] tmsubst M2_.
loc(L)![(J -> S)] tmsubst loc(L).
(fn(TX <: K1) => M2)![(J -> S)] tmsubst (fn(TX <: K1) => M2_) :- M2![TX, (J -> S)] tmsubst2 M2_.
M1![T2]![(J -> S)] tmsubst (M1_![T2_])                        :- M1![(J -> S)] tmsubst M1_, T2![(J -> S)] tsubst T2_.
({(T1, M2)} as T3)![(J -> S)] tmsubst ({(T1_, M2_)} as T3_)   :- T1![(J -> S)] tsubst T1_, M2![(J -> S)] tmsubst M2_, T3![(J -> S)] tsubst T3_.
(let(TX, X) = M1 in M2)![(J -> S)] tmsubst (let(TX, X) = M1_ in M2_)
                                                              :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
T![X, (X -> S)] tmsubst2 T.
T![X, (J -> S)] tmsubst2 T_                                   :- T![(J -> S)] tmsubst T_.

gett(Γ, X, T) :- member(X:T, Γ).
gett(Γ, X, T) :- member(X:T=_, Γ). 

% ------------------------   EVALUATION  ------------------------

extendstore(St, V1, Len, St_)            :- length(St, Len), append(St, [V1], St_).
lookuploc(St, L, R)                      :- nth0(L, St, R).
updatestore([_ | St], 0, V1, [V1 | St]).
updatestore([V | St], N1, V1, [V | St_]) :- N is N1 - 1, updatestore(St, N, V1, St_).

e([L = M | Mf], M, [L = M_ | Mf], M_)    :- \+ v(M).
e([L = M | Mf], M1, [L = M | Mf_], M_)   :- v(M), e(Mf, M1, Mf_, M_).

Γ/St /- if(true, M2, M3) ==> M2/St.
Γ/St /- if(false, M2, M3) ==> M3/St.
Γ/St /- if(M1, M2, M3) ==> if(M1_, M2, M3)/St_       :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- succ(M1) ==> succ(M1_)/St_                   :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- pred(0) ==> 0/St.
Γ/St /- pred(succ(NV1)) ==> NV1/St                   :- n(NV1).
Γ/St /- pred(M1) ==> pred(M1_)/St_                   :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- iszero(0) ==> true/St.
Γ/St /- iszero(succ(NV1)) ==> false/St               :- n(NV1).
Γ/St /- iszero(M1) ==> iszero(M1_)/St_               :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- F1 * F2 ==> F3/St                            :- float(F1), float(F2), F3 is F1 * F2.
Γ/St /- F1 * M2 ==> F1 * M2_/St_                     :- float(F1), eval1(Γ, St, M2, M2_).
Γ/St /- M1 * M2 ==> M1_ * M2/St_                     :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- X ==> M/St                                   :- x(X), member(X:_=M, Γ).
Γ/St /- (fn(X : _) -> M12) $ V2 ==> R/St             :- v(V2), M12![(X -> V2)] subst R.
Γ/St /- V1 $ M2 ==> (V1 $ M2_)/St_                   :- v(V1), Γ/St /- M2 ==> M2_/St_.
Γ/St /- M1 $ M2 ==> (M1_ $ M2)/St_                   :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- (let(X) = V1 in M2) ==> M2_/St               :- v(V1), M2![(X -> V1)] subst M2_.
Γ/St /- (let(X) = M1 in M2) ==> (let(X) = M1_ in M2)/St_
                                                         :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- fix((fn(X : T11) -> M12)) ==> M/St           :- M12![(X -> fix((fn(X : T11) -> M12)))] subst M.
Γ/St /- fix(M1) ==> fix(M1_)/St_                     :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- V1 as _ ==> V1/St                            :- v(V1).
Γ/St /- M1 as T ==> (M1_ as T)/St_                   :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- {Mf} ==> {Mf_}/St_                           :- e(Mf, M, Mf_, M_), Γ/St /- M ==> M_/St_.
Γ/St /- {Mf} # L ==> M/St                            :- member(L = M, Mf).
Γ/St /- M1 # L ==> M1_ # L/St_                       :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- ref(V1) ==> loc(L)/St_                       :- v(V1), extendstore(St, V1, L, St_).
Γ/St /- ref(M1) ==> ref(M1_)/St_                     :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- '!'(loc(L)) ==> V1/St                        :- lookuploc(St, L, V1).
Γ/St /- '!'(M1) ==> '!'(M1_)/St_                     :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- (loc(L) := V2) ==> unit/St_                  :- v(V2), updatestore(St, L, V2, St_).
Γ/St /- (V1 := M2) ==> (V1 := M2_)/St_               :- v(V1), Γ/St /- M2 ==> M2_/St_.
Γ/St /- (M1 := M2) ==> (M1_ := M2)/St_               :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- (fn(X <: K) => M11)![T2] ==> M11_/St         :- M11![(X -> T2)] tmsubst M11_.
Γ/St /- M1![T2] ==> (M1_![T2])/St_                   :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- {(T1, M2)} as T3 ==> ({(T1, M2_)} as T3)/St_ :- Γ/St /- M2 ==> M2_/St_.
Γ/St /- (let(_, X) = {(T11, V12)} as _ in M2) ==> M/St
                                                         :- v(V12), M2![(X -> V12)] subst M2_, M2_![(X -> T11)] tmsubst M.
Γ/St /- (let(TX, X) = M1 in M2) ==> (let(TX, X) = M1_ in M2)/St_
                                                         :- St/Γ /- M1 ==> M1_/St_.

Γ/St /- M ==>> M_/St_ :- Γ/St /- M ==> M1/St1, Γ/St1 /- M1 ==>> M_/St_.
Γ/St /- M ==>> M/St. 

% ------------------------   KINDING  ------------------------

gettabb(Γ, X, T)                        :- member(X::(_:T), Γ).
compute(Γ, X, T)                        :- tx(X), gettabb(Γ, X, T).
compute(Γ, (fn(X :: _) => T12) $ T2, T) :- T12![(X -> T2)] tsubst T.
simplify(Γ, T1 $ T2, T_)                :- simplify(Γ, T1, T1_), simplify2(Γ, T1_ $ T2, T_).
simplify(Γ, T, T_)                      :- simplify2(Γ, T, T_).
simplify2(Γ, T, T_)                     :- compute(Γ, T, T1), simplify(Γ, T1, T_).
simplify2(Γ, T, T).

Γ /- S = T                                          :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ /- S_ == T_.
Γ /- bool == bool.
Γ /- nat == nat.
Γ /- unit == unit.
Γ /- float == float.
Γ /- string == string.
Γ /- X == T                                         :- tx(X), gettabb(Γ, X, S), Γ /- S = T.
Γ /- S == X                                         :- tx(X), gettabb(Γ, X, T), Γ /- S = T.
Γ /- X == X                                         :- tx(X).
Γ /- (S1 -> S2) == (T1 -> T2)                       :- Γ /- S1 = T1, Γ /- S2 = T2.
Γ /- {Sf} == {Tf}                                   :- length(Sf, Len), length(Tf, Len),
                                                       maplist([L : T] >> (member(L : S, Sf), Γ /- S = T), Tf).
Γ /- ref(S) == ref(T)                               :- Γ /- S = T.
Γ /- (all(TX1 :: K1) => S2) == (all(_ :: K2) => T2) :- K1 = K2, [TX1-name|Γ] /- S2 = T2.
Γ /- {some(TX1 :: K1), S2} == {some(_ :: K2), T2}   :- K1 = K2, [TX1-name|Γ] /- S2 = T2.
Γ /- (fn(TX1 :: K1) => S2) == (fn(_ :: K2) => T2)   :- K1 = K2, [TX1-name|Γ] /- S2 = T2.
Γ /- S1 $ S2 == T1 $ T2                             :- Γ /- S1 = T1, Γ /- S2 = T2.

Γ /- T :: K                            :- Γ \- T :: K, !.
Γ /- T :: K                            :- writeln(error : kindof(T, K)), fail.
Γ \- X :: '*'                          :- tx(X), \+ member(X::_, Γ),!.
Γ \- X :: K                            :- tx(X), member(X::(K:_), Γ),!.
Γ \- X :: K                            :- tx(X), !,member(X::K, Γ),!.
Γ \- (T1 -> T2) :: '*'                 :- !, Γ /- T1 :: '*', Γ /- T2 :: '*'.
Γ \- {Tf} :: '*'                       :- maplist([L : S] >> (Γ /- S :: '*'), Tf).
Γ \- (all(TX :: K1) => T2) :: '*'      :- !, [TX::K1|Γ] /- T2 :: '*'.
Γ \- {some(TX :: K1), T2} :: '*'       :- !, [TX::K1|Γ] /- T2 :: '*'.
Γ \- (fn(TX :: K1) => T2) :: (K1 => K) :- !, [TX::K1|Γ] /- T2 :: K.
Γ \- T1 $ T2 :: K12                    :- !, Γ /- T1 :: (K11 => K12), Γ /- T2 :: K11.
Γ \- T :: '*'. 

% ------------------------   TYPING  ------------------------

Γ /- true : bool.
Γ /- false : bool.
Γ /- if(M1, M2, M3) : T2                          :- Γ /- M1 : T1, Γ /- T1 = bool,
                                                        Γ /- M2 : T2, Γ /- M3 : T3, Γ /- T2 = T3.
Γ /- 0 : nat.
Γ /- succ(M1) : nat                               :- Γ /- M1 : T1, Γ /- T1 = nat.
Γ /- pred(M1) : nat                               :- Γ /- M1 : T1, Γ /- T1 = nat.
Γ /- iszero(M1) : bool                            :- Γ /- M1 : T1, Γ /- T1 = nat.
Γ /- unit : unit.
Γ /- F1 : float                                   :- float(F1).
Γ /- M1 * M2 : float                              :- Γ /- M1 : T1, Γ /- T1 = float, Γ /- M2 : T2, Γ /- T2 = float.
Γ /- X : string                                   :- string(X).
Γ /- X : T                                        :- x(X), !, gett(Γ, X, T).
Γ /- (fn(X : T1) -> M2) : (T1 -> T2_)             :- Γ /- T1 :: '*', [X:T1|Γ] /- M2 : T2_.
Γ /- M1 $ M2 : T12                                :- Γ /- M1 : T1, simplify(Γ, T1, (T11 -> T12)), Γ /- M2 : T2, Γ /- T11 = T2.
Γ /- (let(X) = M1 in M2) : T                      :- Γ /- M1 : T1, [X:T1|Γ] /- M2 : T.
Γ /- fix(M1) : T12                                :- Γ /- M1 : T1, simplify(Γ, T1, (T11 -> T12)), Γ /- T12 = T11.
Γ /- inert(T) : T.
Γ /- (M1 as T) : T                                :- Γ /- T :: '*', Γ /- M1 : T1, Γ /- T1 = T.
Γ /- {Mf} : {Tf}                                  :- maplist([L = M, L : T] >> (Γ /- M : T), Mf, Tf).
Γ /- M1 # L : T                                   :- Γ /- M1 : T1, simplify(Γ, T1, {Tf}), member(L : T, Tf).
Γ /- ref(M1) : ref(T1)                            :- Γ /- M1 : T1.
Γ /- '!'(M1) : T1                                 :- Γ /- M1 : T, simplify(Γ, T, ref(T1)).
Γ /- (M1 := M2) : unit                            :- Γ /- M1 : T, simplify(Γ, T, ref(T1)), Γ /- M2 : T2, Γ /- T2 = T1.
Γ /- ({(T1, M2)} as T) : T                        :- Γ /- T :: '*', simplify(Γ, T, {some(Y :: K1), T2}),
                                                        Γ /- T1 :: K1, Γ /- M2 : S2, T2![(Y -> T1)] tsubst T2_, Γ /- S2 = T2_.
Γ /- (let(TX, X) = M1 in M2) : T2                 :- Γ /- M1 : T1, simplify(Γ, T1, {some(_ :: K), T11}),
                                                        [X:T11, TX::K | Γ] /- M2 : T2.
Γ /- (fn(TX <: K1) => M2) : (all(TX :: K1) => T2) :- [TX::K1 | Γ] /- M2 : T2.
Γ /- M1![T2] : T12_                               :- Γ /- T2 :: K2, Γ /- M1 : T1, simplify(Γ, T1, (all(X :: K2) => T12)),
                                                        T12![(X -> T2)] tsubst T12_.
Γ /- M : _                                        :- writeln(error : typeof(M)), !, halt. 

% ------------------------   MAIN  ------------------------

show(X : T)  :- format('~w : ~w\n', [X, T]).
show(X :: K) :- format('~w :: ~w\n', [X, K]).

check_someBind(X:TBody, {(_, T12)} as _, X:some(TBody)=T12).
check_someBind(X:TBody, _, X:TBody).

run({(TX, X)} = M, Γ/St, [B, TX::K|Γ]/St_)  :- tx(TX), x(X), m(M), !, Γ /- M : T, simplify(Γ, T, {some(_ :: K), TBody}),
                                               Γ/St /- M ==>> M_/St_, check_someBind(X:TBody, M_, B),
                                               format('~w\n~w : ~w\n', [TX, X, TBody]).
run(type(X) = T, Γ/St, [X::(K:T)|Γ]/St)     :- tx(X), t(T), Γ /- T :: K, show(X :: K).
run(type(X :: K) = T, Γ/St, [X::(K:T)|Γ]/St):- tx(X), k(K), t(T), Γ /- T :: K, show(X :: K).
run(X :: K, Γ/St, [X::K|Γ]/St)              :- tx(X), k(K), show(X :: K).
run(X : T, Γ/St, [X:T|Γ]/St)                :- x(X), t(T), show(X : T).
run(X : T = M, Γ/St, [X:T=M_|Γ]/St_)        :- x(X), t(T), m(M), Γ /- M : T1, Γ /- T1 = T,
                                               Γ/St /- M ==>> M_/St_, show(X : T).
run(X = M, Γ/St, [X:T=M_|Γ]/St_)            :- x(X), m(M), Γ /- M : T, Γ/St /- M ==>> M_/St_, show(X : T).
run(M, Γ/St, Γ/St_)                         :- !, m(M), !, Γ /- M : T, !, Γ/St /- M ==>> M_/St_, !, writeln(M_ : T).

run(Ls) :- foldl(run, Ls, []/[], _). 

% ------------------------   TEST  ------------------------

% "hello";
:- run(["hello"]). 
% unit;
:- run([unit]). 
% lambda x:A. x;
:- run([(fn(x : 'A') -> x)]). 
% let x=true in x;
:- run([(let(x) = true in x)]). 
% timesfloat 2.0 3.14159;
:- run([2.0 * 3.14159]). 
% lambda x:Bool. x;
:- run([(fn(x : bool) -> x)]). 
% (lambda x:Bool->Bool. if x false then true else false) 
%   (lambda x:Bool. if x then false else true); 
:- run([(fn(x : (bool -> bool)) -> if(x $ false, true, false)) $ (fn(x : bool) -> if(x, false, true))]). 
% lambda x:Nat. succ x;
:- run([(fn(x : nat) -> succ(x))]). 
% (lambda x:Nat. succ (succ x)) (succ 0); 
:- run([(fn(x : nat) -> succ(succ(x))) $ succ(0)]). 
% T = Nat->Nat;
% lambda f:T. lambda x:Nat. f (f x);
:- run([type('T') = (nat -> nat), (fn(f : 'T') -> fn(x : nat) -> f $ (f $ x))]). 
% lambda X. lambda x:X. x;
:- run([(fn('X' <: '*') => fn(x : 'X') -> x)]). 
% (lambda X. lambda x:X. x) [All X.X->X]; 
:- run([(fn('X' <: '*') => fn(x : 'X') -> x)![(all('X' :: '*') => 'X' -> 'X')]]). 

% {*All Y.Y, lambda x:(All Y.Y). x} as {Some X,X->X};
:- run([{((all('Y' :: '*') => 'Y'), (fn(x : (all('Y' :: '*') => 'Y')) -> x))} as {some('X' :: '*'), ('X' -> 'X')}]). 

% {x=true, y=false};
:- run([{[x = true, y = false]}]). 
% {x=true, y=false}.x;
:- run([{[x = true, y = false]} # x]). 
% {true, false};
:- run([{[1 = true, 2 = false]}]). 
% {true, false}.1;
:- run([{[1 = true, 2 = false]} # 1]). 
% {*Nat, {c=0, f=lambda x:Nat. succ x}}
%   as {Some X, {c:X, f:X->Nat}};
:- run([{(nat, {[c = 0, f = (fn(x : nat) -> succ(x))]})} as {some('X' :: '*'), {[c : 'X', f : ('X' -> nat)]}}]). 

% let {X,ops} = {*Nat, {c=0, f=lambda x:Nat. succ x}}
%               as {Some X, {c:X, f:X->Nat}}
% in (ops.f ops.c);
:- run([(let('X', ops) = {(nat, {[c = 0, f = (fn(x : nat) -> succ(x))]})} as {some('X' :: '*'), {[c : 'X', f : ('X' -> nat)]}}
         in ops # f $ ops # c)]).
:- run([ 
% Pair = lambda X. lambda Y. All R. (X->Y->R) -> R;
type('Pair') = (fn('X' :: '*') => fn('Y' :: '*') => all('R' :: '*') => ('X' -> 'Y' -> 'R') -> 'R'),  
% pair = lambda X.lambda Y.lambda x:X.lambda y:Y.lambda R.lambda p:X->Y->R.p x y;
pair = (fn('X' <: '*') => fn('Y' <: '*') => fn(x : 'X') -> fn(y : 'Y') -> fn('R' <: '*') => fn(p : ('X' -> 'Y' -> 'R')) -> p $ x $ y),  
% fst = lambda X.lambda Y.lambda p:Pair X Y.p [X] (lambda x:X.lambda y:Y.x);
fst = (fn('X' <: '*') => fn('Y' <: '*') => fn(p : 'Pair' $ 'X' $ 'Y') -> p!['X'] $ (fn(x : 'X') -> fn(y : 'Y') -> x)),  
% snd = lambda X.lambda Y.lambda p:Pair X Y.p [Y] (lambda x:X.lambda y:Y.y);
snd = (fn('X' <: '*') => fn('Y' <: '*') => fn(p : 'Pair' $ 'X' $ 'Y') -> p!['Y'] $ (fn(x : 'X') -> fn(y : 'Y') -> y)),  
% pr = pair [Nat] [Bool] 0 false;
pr = pair![nat]![bool] $ 0 $ false, fst![nat]![bool] $ pr, snd![nat]![bool] $ pr,  

% List = lambda X. All R. (X->R->R) -> R -> R; 
type('List') = (fn('X' :: '*') => all('R' :: '*') => ('X' -> 'R' -> 'R') -> 'R' -> 'R'),  
% diverge =
% lambda X.
%   lambda _:Unit.
%   fix (lambda x:X. x);
diverge = (fn('X' <: '*') => fn('_' : unit) -> fix((fn(x : 'X') -> x))),  
% nil = lambda X.
%       (lambda R. lambda c:X->R->R. lambda n:R. n)
%       as List X; 
nil = (fn('X' <: '*') => (fn('R' <: '*') => fn(c : ('X' -> 'R' -> 'R')) -> fn(n : 'R') -> n) as 'List' $ 'X'),  
% cons = 
% lambda X.
%   lambda hd:X. lambda tl: List X.
%      (lambda R. lambda c:X->R->R. lambda n:R. c hd (tl [R] c n))
%      as List X; 
cons = (fn('X' <: '*') => fn(hd : 'X') -> fn(tl : 'List' $ 'X') -> (fn('R' <: '*') => fn(c : ('X' -> 'R' -> 'R')) -> fn(n : 'R') -> c $ hd $ (tl!['R'] $ c $ n)) as 'List' $ 'X'),  
% isnil =  
% lambda X. 
%   lambda l: List X. 
%     l [Bool] (lambda hd:X. lambda tl:Bool. false) true; 
isnil = (fn('X' <: '*') => fn(l : 'List' $ 'X') -> l![bool] $ (fn(hd : 'X') -> fn(tl : bool) -> false) $ true),  
% head = 
% lambda X. 
%   lambda l: List X. 
%     (l [Unit->X] (lambda hd:X. lambda tl:Unit->X. lambda _:Unit. hd) (diverge [X]))
%     unit; 
head = (fn('X' <: '*') => fn(l : 'List' $ 'X') -> l![(unit -> 'X')] $ (fn(hd : 'X') -> fn(tl : (unit -> 'X')) -> fn('_' : unit) -> hd) $ (diverge!['X']) $ unit),  
% tail =  
% lambda X.  
%   lambda l: List X. 
%     (fst [List X] [List X] ( 
%       l [Pair (List X) (List X)]
%         (lambda hd: X. lambda tl: Pair (List X) (List X). 
%           pair [List X] [List X] 
%             (snd [List X] [List X] tl)  
%             (cons [X] hd (snd [List X] [List X] tl))) 
%         (pair [List X] [List X] (nil [X]) (nil [X]))))
%     as List X; 
tail = (fn('X' <: '*') =>
  fn(l : 'List' $ 'X') ->
    fst!['List' $ 'X']!['List' $ 'X'] $ (
      l!['Pair' $ ('List' $ 'X') $ ('List' $ 'X')] $ (
        fn(hd : 'X') -> fn(tl : 'Pair' $ ('List' $ 'X') $ ('List' $ 'X')) ->
          pair!['List' $ 'X']!['List' $ 'X'] $
            (snd!['List' $ 'X']!['List' $ 'X'] $ tl) $
            (cons!['X'] $ hd $ (snd!['List' $ 'X']!['List' $ 'X'] $ tl))) $
        (pair!['List' $ 'X']!['List' $ 'X'] $ (nil!['X']) $ (nil!['X'])))
    as 'List' $ 'X')
]).

:- halt.

まとめ

オメガはカインドのある高階多相型システムです。

Dyaus

Dyáuṣ Pitṛ́ (Vedic Sanskrit: Dyáuṣpitṛ́, द्यौष्पितृ, literally 'Sky Father') is the 'Father Heaven' deity of the Vedic pantheon related to & possibly from the reconstructed Proto-Indo-European Sky father god, Dyeus. Dyáuṣ Pitṛ́ appears in hymns with Prithvi Mata 'Mother Earth' in the ancient scriptures of Hinduism. He is significant in comparative philology scholarship of Proto-Indo-European religion as similar vocative and nominative concepts share a similar derivation from the Indo-European language, such as Dies Pater and Jupiter (Latin), Zeus Patér (Zεύς πατήρ, Ancient Greek), Dievas, Tius or Zio (Old High German) and Toutiks dipater (South Picene), all of which like Dyáuṣ Pitṛ́ mean 'sky father'.[1][2][3]

天空神デュアスがインドにあったとされるのだけど、シンボリズムがこの辺から始まったようである。
Om という文字はオームとかと読むそうでωもオームの記号Ωの小文字なので木曜日というところと繋がった。

仏教

この聖音は後に仏教にも取り入れられ、密教では真言の冒頭の決まり文句（オン）として、末尾のスヴァーハー（ソワカ）と共に多用された（例えば「オン　アビラウンケン　ソワカ」で大日如来の真言）。 また、仏教の経典『守護国界主陀羅尼経』では「a」は法身、「u」は報身、「m」は応身の三身を象徴し、すべての仏たちはこの聖音を観想する事によって成仏すると説かれる。

ソワカー、ソワカーノーマクサンマンダーソワカー　アリアーダンケン♪っていうAkiraの映画の音楽に使われてた気がする。
アビラウンケンっていっていたのかなぁ。

ボンって天皇陛下が言って神と仏と一体になたとか何とかいう話もあったような。