Prolog でわかる TAPL 6日目 - 第Ⅱ部 単純型 (2)

アプロディーテー

アプロディーテー（古典ギリシア語：ΑΦΡΟΔΙΤΗ, Ἀφροδίτη, Aphrodītē）またはアプロディタ（アイオリス方言：ΑΦΡΟΔΙΤΑ, Ἀφροδιτα, Aphrodita）は、愛と美と性を司るギリシア神話の女神で、オリュンポス十二神の一柱である[1]。美において誇り高く、パリスによる三美神の審判で、最高の美神として選ばれている[1]。また、戦の女神としての側面も持つ。日本語では、アプロディテ[1]、アフロディテ、アフロディーテ、アフロダイティ（英: Aphrodite）などとも表記される。

元来は、古代オリエントや小アジアの豊穣の植物神・植物を司る精霊・地母神であったと考えられる[2]。アプロディーテーは、生殖と豊穣、すなわち春の女神でもあった。

ホメーロスの『イーリアス』では「黄金のアプロディーテー」や「笑いを喜ぶアプロディーテー」など特有の形容語句を持っている。プラトンの『饗宴』では純粋な愛情を象徴する天上の「アプロディーテー・ウーラニアー（英語版)」と凡俗な肉欲を象徴する大衆の「アプロディーテー・パンデーモス（英語版）」という二種類の神性が存在すると考えられている[3]。

聖獣はイルカで、聖鳥は白鳥、鳩、雀、燕。聖樹は薔薇、芥子、花梨、銀梅花。真珠、帆立貝、林檎もその象徴とされる。また、牡山羊や鵞鳥に乗った姿でも描かれる。

本来、豊穣多産の植物神としてイシュタルやアスタルテー同様に金星の女神であったが、このことはホメーロスやヘーシオドスでは明言されていない。しかし古典期以降、再び金星と結び付けられ、ギリシアでは金星を「アプロディーテーの星」と呼ぶようになった。現代のヨーロッパ諸言語で、ラテン語の「ウェヌス」に相当する語で金星を呼ぶのはこれに由来する。

今日は 参照とエラーについて見ます。参照は書き換え可能な変数を SML や OCaml のリファレンスのような形で実装し、エラーは問題のあるプログラムをエラーの規則を追加して補足します。

13章 参照

図13-1.参照1

→Unit Ref λ→のUnit(図9-1と図11-2)を用いた拡張

構文
t ::= 項:
　unit 定数unit
　x 変数
　λx:T.t ラムダ抽象
　t t 関数適用
　ref t 参照の生成
　!t 参照先の値の取り出し
　t:=t 破壊的代入
　l ストアでの位置
v ::= 値:
　unit 定数unit
　λx:T.t ラムダ抽象値
　l ストアでの位置
T ::= 型:
　Unit Unit型
　T->T 関数の型
　Ref T 参照セルの型
μ::= ストア:
　∅ 空のストア
　μ,l->v 位置への束縛
Γ::= 文脈:
　∅ 空の文脈
　Γ,x:T 項変数の束縛
Σ::= ストア型付け:
　∅ 空のストア型付け
　Σ,l:T 位置の型付け

評価 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)

l ∉ dom(μ)
------------------------------------------ (E-RefV)
ref v1 | μ ==> l | (μ, l->v1)

l ∉ dom(μ)
------------------------------------------ (E-Ref)
ref v1 | μ ==> l | (μ, l->v1)

t1 | μ ==> t1’ | μ’
------------------------------------------ (E-Ref)
ref t1 | μ ==> ref t1’ | μ’

μ(l) = v
------------------------------------------ (E-DerefLoc)
!l | μ ==> v | μ

t1 | μ ==> t1’ | μ’
------------------------------------------ (E-Deref)
!t1 | μ ==> !t1’ | μ’

l:=v2 | μ ==> unit | [l->v2]μ            (E-Assign)

t1 | μ ==> t1’| μ’
------------------------------------------ (E-Assign1)
t1:=t2|μ==>t1’:=t2|μ’

t2 | μ ==> t2’| μ’
------------------------------------------ (E-Assign2)
v1:=t2|μ==>v1:=t2’|μ’

図13-1.参照2

型付け Γ|Σ ⊢ t:T

Γ|Σ ⊢ unit:Unit                         (T-Unit)

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

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

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

Σ(l) = T1
---------------------------------------- (T-Loc)
Γ|Σ ⊢ l:Ref T1

Γ|Σ ⊢ t1:T1
---------------------------------------- (T-Ref)
Γ|Σ ⊢ ref t1:Ref T1

Γ|Σ ⊢ t1:Ref T11
---------------------------------------- (T-Deref)
Γ|Σ ⊢ !t1:T11

Γ|Σ ⊢ t1:Ref T11   Γ|Σ ⊢ t2:T11
---------------------------------------- (T-Assign)
Γ|Σ ⊢ t1:=t2:Unit

14章 エラー

図14-1.エラー

→エラー λ→(図9-1)に基づく

新しい構文規則

t::= … 項:
　error 実行時エラー


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

error t2 ==> error                         (E-AppErr1)

v1 error ==> error                         (E-AppRaise2)


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

Γ ⊢ error : T                              (T-Error)

図14-2.エラー補捉

→エラー 捕捉 λ→とエラー(図14-1)の拡張

新しい構文規則

t::= … 項:
　try t with t エラーの捕捉


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

try v1 with t2 ==> v1                      (E-TryV)

try error with t2 ==> t2                  (E-TryError)

t1 ==> t1’
----------------------------------------- (E-Try)
try t1 with t2 ==> try t1’ with t2

try error with t2 ==> t2                  (E-TryError)


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

Γ ⊢ t1 : T　　Γ ⊢ t2 : T
----------------------------------------- (T-Try)
Γ ⊢ try t1 with t2:T

図14-3.例外

→例外 λ→(図9-1)の拡張

新しい構文規則

t::= … 項:
　raise t 例外の送出
　try t with t 例外の処理

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

(raise v11) t2 ==> raise v11               (E-AppRaise1)

v1 (raise v21) ==> raise v21               (E-AppRaise2)

t1 ==> t1’
------------------------------------------ (E-Raise)
raise t1 ==> raise t1’

raise (raise v11) ==> raise v11            (E-RaiseRaise)

try v1 with t2 ==> v1                      (E-TryV)

try raise v11 with t2 ==> t2 v11           (E-TryRaise)

t1 ==> t1’
------------------------------------------ (E-Try)
try t1 with t2 ==> try t1’ with t2

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

Γ ⊢ t1 : Texn
------------------------------------------ (E-Exn)
Γ ⊢ raise t1 : T

Γ ⊢ t1 : T　　Γ ⊢ t2 : Texn->T
------------------------------------------ (E-Try)
try t1 with t2 : T

実装

fullref.pl

プログラムの全体を見る

fullref.pl

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

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

:- use_module(rtg).

w ::= bool | nat | unit | float | string | true | false. % キーワード:
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)].            % リスト

t ::=                           % 型:
      bool                      % ブール値型
    | nat                       % 自然数型
    | unit                      % Unit型
    | float                     % 浮動小数点数型
    | string                    % 文字列型
    | top                       % 最大の型
    | bot                       % 最小の型
    | tx                        % 型変数
    | (t -> t)                  % 関数の型
    | {list(l : t)}             % レコードの型
    | [list(x : t)]             % バリアント型
    | ref(t)                    % 参照セルの型
    | source(t)
    | sink(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                     % 射影
    | case(m, list(x = (x, m))) % 場合分け
    | tag(x, m) as t            % タグ付け
    | loc(integer)              % ストアでの位置
    | ref(m)                    % 参照の生成
    | '!'(m)                    % 参照先の値の取り出し
    | m := m                    % 破壊的代入
    .
n ::=                           % 数値:
    0                           % ゼロ
    | succ(n)                   % 後者値
    .
v ::=                           % 値:
    true                        % 真
    | false                     % 偽
    | n                         % 数値
    | unit                      % 定数unit
    | floatl                    % 浮動小数点数値
    | stringl                   % 文字列定数
    | (fn(x : t) -> m)          % ラムダ抽象
    | {list(l = v)}             % レコード
    | tag(x, v) as t            % タグ付け
    | loc(integer)              % ストアでの位置
    . 

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

maplist2(_, [], []).
maplist2(F, [X | Xs], [Y | Ys]) :- call(F, X, Y), maplist2(F, Xs, Ys).

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.
top![(J -> S)] tsubst top.
bot![(J -> S)] tsubst bot.
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_).
[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_.
source(T1)![(J -> S)] tsubst source(T1_)  :- T1![(J -> S)] tsubst T1_.
sink(T1)![(J -> S)] tsubst sink(T1_)      :- T1![(J -> S)] tsubst T1_.
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_.

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_.
(tag(L, M1) as T1)![(J -> M)] subst (tag(L, M1_) as T1)    :- M1![(J -> M)] subst M1_.
case(M1, Cases)![(J -> M)] subst case(M1_, Cases_)         :- M1![(J -> M)] subst M1_, maplist([L = (X, M2), L = (X, M2_)] >> (M2![(J -> M)] subst M2_), Cases, Cases_).
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).
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_.

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 /- tag(L, M1) as T ==> (tag(L, M1_) as T)/St_       :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- case(tag(L, V11) as _, Bs) ==> M_/St             :- v(V11), member(L = (X, M), Bs), M![(X -> V11)] subst M_.
Γ/St /- case(M1, Bs) ==> case(M1_, Bs)/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 /- M ==>> M_/St_                                    :- Γ/St /- M ==> M1/St1, Γ/St1 /- M1 ==>> M_/St_.
Γ/St /- M ==>> M/St. 

% ------------------------   SUBTYPING  ------------------------

gettabb(Γ, X, T)   :- member(X :: T, Γ).
compute(Γ, X, T)   :- tx(X), gettabb(Γ, X, T).
simplify(Γ, T, T_) :- compute(Γ, T, T1), simplify(Γ, T1, T_).
simplify(Γ, T, T).

Γ /- S = T         :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ /- S_ == T_.
Γ /- bool == bool.
Γ /- nat == nat.
Γ /- unit == unit.
Γ /- float == float.
Γ /- string == string.
Γ /- top == top.
Γ /- bot == bot.
Γ /- 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).
Γ /- [Sf] == [Tf]             :- length(Sf, Len), length(Tf, Len),
                                 maplist2([L : S, L : T] >> (Γ /- S = T), Sf, Tf).
Γ /- ref(S) == ref(T)         :- Γ /- S = T.
Γ /- source(S) == source(T)   :- Γ /- S = T.
Γ /- sink(S) == sink(T)       :- Γ /- S = T.

Γ /- S <: T                   :- Γ /- S = T.
Γ /- S <: T                   :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ <: T_.
Γ \- _ <: top.
Γ \- bot <: _.
Γ \- (S1 -> S2) <: (T1 -> T2) :- Γ /- T1 <: S1, Γ /- S2 <: T2.
Γ \- {SF} <: {TF}             :- maplist([L : T] >> (member(L : S, SF), Γ /- S <: T), TF).
Γ \- [SF] <: [TF]             :- maplist([L : S] >> (member(L : T, TF), Γ /- S <: T), SF).
Γ \- ref(S) <: ref(T)         :- Γ /- S <: T, Γ /- T <: S.
Γ \- ref(S) <: source(T)      :- Γ /- S <: T.
Γ \- source(S) <: source(T)   :- Γ /- S <: T.
Γ \- ref(S) <: sink(T)        :- Γ /- T <: S.
Γ \- sink(S) <: sink(T)       :- Γ /- T <: S.

Γ /- S /\ T : T                            :- Γ /- S <: T.
Γ /- S /\ T : S                            :- Γ /- T <: S.
Γ /- S /\ T : R                            :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ /\ T_ : R.
Γ \- {SF} /\ {TF} : {UF_}                  :- include([L : _] >> member(L : _, TF), SF, UF), maplist([L : S, L : T_] >> (member(L : T, TF), Γ /- S /\ T : T_), UF, UF_).
Γ \- (S1 -> S2) /\ (T1 -> T2) : (S_ -> T_) :- Γ /- S1 \/ T1 : S_, Γ /- S2 /\ T2 : T_.
Γ \- ref(S) /\ ref(T) : ref(S)             :- Γ /- S <: T, Γ /- T <: S.
Γ \- ref(S) /\ ref(T) : source(T_)         :- /* Warning: this is incomplete... */ Γ /- S /\ T : T_.
Γ \- source(S) /\ source(T) : source(T_)   :- Γ /- S /\ T : T_.
Γ \- ref(S) /\ source(T) : source(T_)      :- Γ /- S /\ T : T_.
Γ \- source(S) /\ ref(T) : source(T_)      :- Γ /- S /\ T : T_.
Γ \- sink(S) /\ sink(T) : sink(T_)         :- Γ /- S \/ T : T_.
Γ \- ref(S) /\ sink(T) : sink(T_)          :- Γ /- S \/ T : T_.
Γ \- sink(S) /\ ref(T) : sink(T_)          :- Γ /- S \/ T : T_.
Γ \- _ /\ _ : top.

Γ /- S \/ T : S                            :- Γ /- S <: T.
Γ /- S \/ T : T                            :- Γ /- T <: S.
Γ /- S \/ T : R                            :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ \/ T_ : R.
Γ \- {SF} \/ {TF} : {UF_}                  :- maplist([L : S, L : T_] >> (
                                                member(L : T, TF), Γ /- S \/ T : T_ ; T_ = S
                                              ), SF, SF_),
                                              include([L : _] >> (\+ member(L : _, SF)), TF, TF_),
                                              append(SF_, TF_, UF_).
Γ \- (S1 -> S2) \/ (T1 -> T2) : (S_ -> T_) :- Γ /- S1 /\ T1 : S_, Γ /- S2 \/ T2 : T_.
Γ \- ref(S) \/ ref(T) : ref(T)             :- Γ /- S <: T, Γ /- T <: S.
Γ \- ref(S) \/ ref(T) : source(T_)         :- Γ /- S \/ T : T_.
Γ \- source(S) \/ source(T) : source(T_)   :- Γ /- S \/ T : T_.
Γ \- ref(S) \/ source(T) : source(T_)      :- Γ /- S \/ T : T_.
Γ \- source(S) \/ ref(T) : source(T_)      :- Γ /- S \/ T : T_.
Γ \- sink(S) \/ sink(T) : sink(T_)         :- Γ /- S /\ T : T_.
Γ \- ref(S) \/ sink(T) : sink(T_)          :- Γ /- S /\ T : T_.
Γ \- sink(S) \/ ref(T) : sink(T_)          :- Γ /- S /\ T : T_.
Γ \- _ \/ _ : bot. 

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

Γ /- true : bool.
Γ /- false : bool.
Γ /- if(M1, M2, M3) : T               :- Γ /- M1 : T1, Γ /- T1 <: bool,
                                            Γ /- M2 : T2, Γ /- M3 : T3, Γ /- T2 /\ T3 : T.
Γ /- 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_) :- [X:T1|Γ] /- M2 : T2_, !.
Γ /- M1 $ M2 : bot                    :- Γ /- M1 : T1, Γ /- M2 : T2, simplify(Γ, T1, bot).
Γ /- M1 $ M2 : T12                    :- Γ /- M1 : T1, simplify(Γ, T1, (T11 -> T12)),
                                            Γ /- M2 : T2, Γ /- T2 <: T11.
Γ /- (let(X) = M1 in M2) : T          :- Γ /- M1 : T1, [X:T1|Γ] /- M2 : T.
Γ /- fix(M1) : T12                    :- Γ /- M1 : T1, simplify(Γ, T1, (T11 -> T12)), Γ /- T12 <: T11.
Γ /- fix(M1) : bot                    :- Γ /- M1 : T1, simplify(Γ, T1, bot).
Γ /- inert(T) : T.
Γ /- (M1 as 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).
Γ /- M1 # L : bot                     :- Γ /- M1 : T1, simplify(Γ, T1, bot).
Γ /- (tag(Li, Mi) as T) : T           :- simplify(Γ, T, [Tf]), member(Li : Te, Tf),
                                            Γ /- Mi : T_, Γ /- T_ <: Te.
Γ /- case(M, Cases) : bot             :- Γ /- M : T, simplify(Γ, T, bot),
                                            maplist([L = _] >> member(L : _, Tf), Cases),
                                            maplist([Li = (Xi, Mi)] >> (
                                              member(Li : Ti, Tf),
                                              [Xi:Ti|Γ] /- Mi : Ti_
                                            ), Cases).
Γ /- case(M, Cases) : T_              :- Γ /- M : T, simplify(Γ, T, [Tf]),
                                            maplist([L = _] >> member(L : _, Tf), Cases),
                                            maplist([Li = (Xi, Mi), Ti_] >> (
                                              member(Li : Ti, Tf),
                                              [Xi:Ti|Γ] /- Mi : Ti_
                                            ), Cases, CaseTypes),
                                            foldl([S, T1, U] >> (Γ /- S /\ T1 : U), CaseTypes, bot, T_).
Γ /- ref(M1) : ref(T1)                :- Γ /- M1 : T1.
Γ /- '!'(M1) : T1                     :- Γ /- M1 : T, simplify(Γ, T, ref(T1)).
Γ /- '!'(M1) : bot                    :- Γ /- M1 : T, simplify(Γ, T, bot).
Γ /- '!'(M1) : T1                     :- Γ /- M1 : T, simplify(Γ, T, source(T1)).
Γ /- (M1 := M2) : unit                :- Γ /- M1 : T, simplify(Γ, T, ref(T1)), Γ /- M2 : T2, Γ /- T2 <: T1.
Γ /- (M1 := M2) : bot                 :- Γ /- M1 : T, simplify(Γ, T, bot), Γ /- M2 : _.
Γ /- (M1 := M2) : unit                :- Γ /- M1 : T, simplify(Γ, T, sink(T1)),
                                            Γ /- M2 : T2, subtyping(Γ, T2, T1).
Γ /- loc(l) : _                       :- !, fail. 

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

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

run(type(X), Γ/St, [X-tvar|Γ]/St)    :- tx(X), show(X).
run(type(X) = T, Γ/St, [X::T|Γ]/St)  :- tx(X), t(T), show(X :: T).
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 : T_, Γ /- T_ = 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  ------------------------

% lambda x:Bot. x;
:- run([(fn(x : bot) -> x)]). 
% lambda x:Bot. x x;
:- run([(fn(x : bot) -> x $ x)]). 
% lambda x:<a:Bool,b:Bool>. x;
:- run([(fn(x : [[a : bool, b : bool]]) -> x)]). 
% lambda x:Top. x;
:- run([(fn(x : top) -> x)]). 
% (lambda x:Top. x) (lambda x:Top. x);
:- run([(fn(x : top) -> x) $ (fn(x : top) -> x)]). 
% (lambda x:Top->Top. x) (lambda x:Top. x);
:- run([(fn(r : (top -> top)) -> r $ r) $ (fn(z : top) -> z)]). 
% (lambda r:{x:Top->Top}. r.x r.x)
%   {x=lambda z:Top.z, y=lambda z:Top.z};
:- run([(fn(r : {[x : (top -> top)]}) -> r # x $ r # x) $
           {[x = (fn(z : top) -> z), y = (fn(z : top) -> z)]}]). 
% "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)]). 
% {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]). 
% if true then {x=true,y=false,a=false} else {y=false,x={},b=false};
:- run([if(true, {[x = true, y = false, a = false]}, {[y = false, x = {[]}, b = false]})]). 
% 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))]). 
% let a = ref 1 in !a;
:- run([(let(a) = ref(succ(0)) in '!'(a))]). 
% let a = ref 2 in (a := (succ (!a)); !a);
:- run([(let(a) = ref(succ(succ(0))) in let('_') = (a := succ('!'(a))) in '!'(a))]).

:- halt.

fullerror.pl

プログラムの全体を見る

fullerror.pl

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

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

:- use_module(rtg).
w ::= bool | top | bot | 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). % 型変数:

t ::=                  % 型:
      bool             % ブール値型
    | top              % 最大の型
    | bot              % 最小の型
    | tx               % 型変数
    | (t -> t)         % 関数の型
    .
m ::=                  % 項:
      true             % 真
    | false            % 偽
    | if(m, m, m)      % 条件式
    | x                % 変数
    | (fn(x : t) -> m) % ラムダ抽象
    | m $ m            % 関数適用
    | error            % 実行時エラー
    | try(m, m)        % エラーの捕捉
    .
v ::=                  % 値:
      true             % 真
    | false            % 偽
    | (fn(x : t) -> m) % ラムダ抽象
    . 

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

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_.
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_.
try(M1, M2)![(J -> M)] subst try(M1_, M2_)              :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
error![(J -> M)] subst error.
S![J, (J -> M)] subst2 S.
S![X, (J -> M)] subst2 M_                               :- S![(J -> M)] subst M_.

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

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

eval_context(if(M1, M2, M3), ME, if(MH, M2, M3), H) :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(M1 $ M2, ME, MH $ M2, H)               :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(V1 $ M2, ME, V1 $ MH, H)               :- \+ v(M2), eval_context(M2, ME, MH, H).
eval_context(try(M1, M2), M1, try(H, M2), H).
eval_context(M1, M1, H, H)                          :- \+ v(M1). 

Γ /- if(true, M2, _) ==> M2.
Γ /- if(false, _, M3) ==> M3.
Γ /- X ==> M                         :- x(X), member(X:_=M,Γ).
Γ /- (fn(X : T11) -> M12) $ V2 ==> R :- v(V2), M12![(X -> V2)] subst R.
Γ /- try(error, M2) ==> M2.
Γ /- try(V1, M2) ==> V1              :- v(V1).
Γ /- try(M1, M2) ==> try(M1_, M2)    :- Γ /- M1 ==> M1_.
Γ /- error ==> _                     :- !, fail.
Γ /- M ==> error                     :- eval_context(M, error, _, _), !.
Γ /- M ==> M_                        :- eval_context(M, ME, M_, H), M \= ME, Γ /- ME ==> H.
Γ /- M ==>> M_                       :- Γ /- M ==> M1, Γ /- M1 ==>> M_.
Γ /- M ==>> M. 

% ------------------------   SUBTYPING  ------------------------

gettabb(Γ, X, T)   :- member(X :: T, Γ).
compute(Γ, X, T)   :- tx(X), gettabb(Γ, X, T).
simplify(Γ, T, T_) :- compute(Γ, T, T1), simplify(Γ, T1, T_).
simplify(Γ, T, T).

Γ /- S = T                    :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ /- S_ == T_.
Γ /- bool == bool.
Γ /- top == top.
Γ /- bot == bot.
Γ /- 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.

Γ /- S <: T                   :- Γ /- S = T.
Γ /- S <: T                   :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S <: S_.
Γ \- _ <: top.
Γ \- bot <: _.
Γ \- (S1 -> S2) <: (T1 -> T2) :- Γ /- T1 <: S1, Γ /- S2 <: T2.

Γ /- S /\ T : T                            :- Γ /- S <: T.
Γ /- S /\ T : S                            :- Γ /- T <: S.
Γ /- S /\ T : S                            :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ /\ T_ : S.
Γ \- (S1 -> S2) /\ (T1 -> T2) : (S_ -> T_) :- Γ /- S1 \/ T1 : S_, Γ /- S2 /\ T2 : T_.
Γ \- _ /\ _ : top.

Γ /- S \/ T : S                            :- Γ /- S <: T.
Γ /- S \/ T : T                            :- Γ /- T <: S.
Γ /- S \/ T : S                            :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ \/ T_ : S.
Γ \- (S1 -> S2) \/ (T1 -> T2) : (S_ -> T_) :- Γ /- S1 /\ T1 : S_, Γ /- S2 \/ T2 : T_.
Γ \- _ \/ _ : bot. 

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

Γ /- true : bool.
Γ /- false : bool.
Γ /- if(M1, M2, M3) : T               :- Γ /- M1 : T1, Γ /- T1 <: bool,
                                         Γ /- M2 : T2, Γ /- M3 : T3, Γ /- T2 /\ T3 : T.
Γ /- X : T                            :- x(X), !, gett(Γ, X, T).
Γ /- (fn(X : T1) -> M2) : (T1 -> T2_) :- [X : T1 | Γ] /- M2 : T2_.
Γ /- M1 $ M2 : T12                    :- Γ /- M1 : T1, Γ /- M2 : T2, simplify(Γ, T1, (T11 -> T12)), !,
                                         Γ /- T2 <: T11.
Γ /- M1 $ M2 : bot                    :- Γ /- M1 : T1, Γ /- M2 : T2, simplify(Γ, T1, bot), !.
Γ /- try(M1, M2) : T                  :- Γ /- M1 : T1, Γ /- M2 : T2, Γ /- T1 /\ T2 : T.
Γ /- error : bot. 

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

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

run(type(X), Γ, [X - X | Γ])      :- tx(X), writeln(X).
run(type(X) = T, Γ, [X :: T | Γ]) :- tx(X), t(T), show(X :: *).
run(X : T, Γ, [X : T | Γ])        :- x(X), t(T), show(X : T).
run(X = M, Γ, [X:T=M_ | Γ])       :- x(X), m(M), Γ /- M : T, Γ /- M ==>> M_, show(X : T).
run(X : T = M, Γ, [X:T=M_ | Γ])   :- x(X), t(T), m(M), Γ /- M : T_, Γ /- T_ = T,
                                     Γ /- M ==>> M_, show(X : T).
run(M, Γ, Γ)                      :- m(M), !, Γ /- M : T, !, Γ /- M ==>> M_, !, writeln(M_ : T).
run(Ls)                           :- foldl(run, Ls, [], _). 

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

% lambda x:Bot. x;
:- run([(fn(x : bot) -> x)]). 
% lambda x:Bot. x x;
:- run([(fn(x : bot) -> x $ x)]). 
% lambda x:Top. x;
:- run([(fn(x : top) -> x)]). 
% (lambda x:Top. x) (lambda x:Top. x);
:- run([(fn(x : top) -> x) $ (fn(x : top) -> x)]). 
% (lambda x:Top->Top. x) (lambda x:Top. x);
:- run([(fn(x : (top -> top)) -> x) $ (fn(x : top) -> x)]). 
% 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))]).  
% if error then true else false;
:- run([if(error, true, false)]). 
% error true;
:- run([error $ true]). 
% (lambda x:Bool. x) error;
:- run([(fn(x : bool) -> x) $ error]). 
% T = Bool;
:- run([type('T') = bool]). 
:- run([a = true, a]).
% try error with true;
:- run([try(error, true)]). 
% try if true then error else true with false;
:- run([try(if(true, error, true), false)]).

:- halt.

まとめ

参照型はデータを更新可能にします。

エラー処理の規則を加えれば、正常ではない場合の処理もうまく捉えてより扱いやすい言語にすることができます。

Rose
From Wikipedia, the free encyclopedia

For other uses, see Rose (disambiguation), Roses (disambiguation), and Rosa.

A rose is a woody perennial flowering plant of the genus Rosa, in the family Rosaceae, or the flower it bears. There are over three hundred species and thousands of cultivars. They form a group of plants that can be erect shrubs, climbing, or trailing, with stems that are often armed with sharp prickles. Flowers vary in size and shape and are usually large and showy, in colours ranging from white through yellows and reds. Most species are native to Asia, with smaller numbers native to Europe, North America, and northwestern Africa. Species, cultivars and hybrids are all widely grown for their beauty and often are fragrant. Roses have acquired cultural significance in many societies. Rose plants range in size from compact, miniature roses, to climbers that can reach seven meters in height. Different species hybridize easily, and this has been used in the development of the wide range of garden roses.[1]