日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

実用的な型エラースライサーに向けた改良と評価
対馬 かなえ脇川 奈穂

本論文ではコンパイラの型推論器を用いた効率的な型エラースライス手法を提案し、評価を行う。型エラースライスとは型エラーのプログラムの中でひとつの型エラーに関係する部分のみを集めたプログラムであり、デバッグ等で役立つ。今まで型エラースライサーは多く提案されてきたが、効率性や実際の速度についての研究はなされてこなかった。本論文では、型エラースライシングを行う際に、おおよそプログラムを半分にわけるように改良した手法を二種類導入する。加えて、それぞれの手法が人工的に作成したサイズが大きいプログラムに対してどの程度の速度か実験し、結果の考察を行う。

それは、それらを 2 で置き換えて、型推論器にかけ

1 はじめに
本論文では、型エラースライス [2] [5] の効率的な求め方を提案する。型エラースライスとは、型エラー

ると型エラーでなくなってしまうことからわかる。
型エラースライスの求め方はいくつかの手法に分けられる。

のプログラムの中でひとつの型エラーに関係する部分(1) プログラムから型制約を抽出し、型エラーになのみを集めたプログラムである。デバッグ時にプログる極小の組み合わせを求め、型制約をプログラムへ

ラマにとって便利であるほか、型エラーデバッガ [1]戻す[4] [6] [8] のデバッグ対象箇所を減らすことができる。

この手法の利点は、型制約さえ抽出してしまえば、まず型エラースライスとはどのようなものか見てみ既存のソルバ等を使用して、極小な型エラースライス

よう。2 を型制約のないプログラム (例外の発生など)が求められることである。 [2] など多くの先行研究でとする。OCaml の型エラーになるプログラム (fun xはこの手法が使われている。欠点は正しい型制約を抽→ x + 3) true の型エラースライスは (fun x →出するために、その言語の型と型推論に関しての知識

x + 2) true である。2 になった部分の型制約がなが必要になることである。

くてもプログラムは依然として型エラーになることがわかる。
また、型エラースライスには極小という概念が存在(2) プログラムを抽象化し、コンパイラの型推論器を使用して型エラーになるかを判定することで、型エラーになる極小のプログラムを求めるする。極小な型エラースライスでは、スライスに含まこの手法の利点は、型推論器をブラックボックスとれるどの部分も型エラーに関係していることが求めして使うことができることである。既存の研究 [3] [5]られる。上の例も極小な型エラースライスであるが、はこちらにあたる。それぞれの構文に対して一段階抽

そのスライスに含まれる部分、x や + など全ての部象化したプログラムを定義するだけで、型推論器を実

分は、全体として型エラーになるために必須である。

装することなく、既存の型推論器を利用してスライス

Practical Type Error Slicing
Kanae Tsushima, 国立情報学研究所, Wakikawa Naho,
お茶の水女子大学.

を求めることができる。大きい言語を対象として挙動が正しいスライサーを定義するためには、型規則の完全な理解が必要ないこちらの手法の方が容易である。

実際、著者らは OCaml を対象とした型エラースラ使用した関数 illtyped? を使用する。これは型推論

イサーの実装を行った [7]。欠点としては、抽象化の器を用いて型がつく時には false を、型がつかない時

たびに型推論を行うため、プログラムの大きさと構造には true を返す関数である。

によっては時間がかかることである。

単純なスライサーの定義を図 3 に示した。abst one

これまでの研究 [2] [3] [5] では型エラースライシ

は受け取ったプログラムを (2 で置き換えて) 一段階ングの手法の提案や正しさについては検討されてき抽象化したもののリストを返す関数である。choose

たが、効率性に関しては研究が行われてこなかった。

は抽象化されたものの中から一つを選ぶ関数である

よって本研究では、既存研究 [5] [7] のスライサーを改(ただし、本節の choose は単純に一番先頭のものを良し、スライシングの効率化について検討していく。

選ぶ)。スライシングのメイン関数 slicing1 では以下

2 節では AST の一番上のノードから、順にスライのようにスライシングを行う。abst one を使用して、シングを行うスライシング手法 [5] を簡単に振り返

一段階抽象化したもののリストを得る。そのリストる。3 節では、それを改良し、AST の一番上のノーと、その時のコンテキスト cxt および、一段階の抽象ドの中で、そのノードのサイズの半分に最も近いも化したものに全て型がついた場合のサンクで searchのからスライシングを行う手法を導入する。4 節でを呼び出す。search では choose を使用して、一段は、より改良を行い、AST 全体の中で全体のサイズ

階抽象化したものから一つ選ぶ。もしそれに型がつの半分に最も近いものからスライシングを行う。5 節

かないならば、(cxt e) は型エラーになるのに十分ででは、2 節から 4 節のそれぞれの手法を、人工的にあるので、再び slicing1 を呼ぶ。もし型がつくなら作成したノード数の多いプログラムでどの程度時間

ば、search に再帰して残りのリストから他の可能性がかかるかの実験とその考察を行う。

を探す。他の可能性がない場合には、あらかじめ渡されていた三つ目の引数のサンクを実行する。

2 単純に AST の上の方から順に探索するス
ライサー

この手法では、AST の一番上のノードの子ノード
から順にひとつずつ抽象化を行っていく。よってこの本節では、単純なスライサーを簡単に説明する。型手法で時間がかかる例は、バランスが偏った深い木でエラースライスの厳密な定義、アルゴリズム中の不変

AST の一番下の方に型エラーの原因が含まれている

条件、アルゴリズムで導出されるものが極小なスライ

ような場合である。実はそのような例は OCaml でスであることの証明などは論文 [5] を参照されたい。

は簡単に実現できる。OCaml では大きいリストはコ対象とする言語とその型を図 1 に示した。対象とンストラクタの大きい入れ子になる。よって要素がたする言語は定数、変数、ラムダ式、関数適用、組であくさん入ったリストを作成し、最後のみ型が違う要素

り、単純型付ラムダ計算に定数と組を追加したものを入れれば良い。本節の手法を要素数が 200 のリスである。図 2 に示したスライス用の構文では、上にト ([1;2;3;...;199;true]) で試した場合、スライ

加えて 2 が追加される。これはスライスで抽象化さシングに 13.15 秒かかった。

れた式を示す、型制約をもたないプログラムである。

AST のある葉が型エラーに関係ない場合には、(13 AST の上の方から探索するが、サイズ+ 2.0) の型エラースライス (2 + 2.0) のように葉が全体の半分に近いものを優先するスラが 2 で置き換えられる。ノード自体が型エラーに関イサー

係ないが、その子ノードは関係がある場合には (x =本節では、前節の単純なスライサーを少し改良す

3, x = 1.0) の型エラースライス@ 2 (x = 3) (xる。基本的にスライシング前にはどの部分が型エラー= 1.0) のように、ノード自体が関数部分が 2 の関数に関係があるか分からないため、要素数が半分の状態

適用で置き換えられる。

で型がつくかを試すのが効率的であると考えられる。

本研究のスライシング手法では、既存の型推論器をそこで、前節と同じように AST の一番上のノードか(s : int):=n(プログラムのサイズ)(M : term)

:=

cs

(定数)

|

s

(変数)

s

(関数抽象)(τ : type)

x

|

λ x.M

|

s

@ M ...M|

let x = M in M|

(M, . . . , M )s

s

:=

cs

(定数)

(関数適用)|

s(変数)(let 文)

|

s

λ x.S

(関数抽象)( 組)|s@ S ...S(関数適用)|

lets x = S in S

(S : slice)

x

:=

α

(型変数)

|

(S, . . . , S)|

int, f loat, . . .

(型定数)

|

τ →τ

|

2

(関数型)

|

τ ∗ ... ∗ τ

(組の型)

図1

図2

s

(let 文)(組)(ホール)

スライスの構文

ラムダ計算の構文と型ら探索するが、子ノードの中でもサイズが全体の半分となる AST の直下の子ノードのみを対象としたが、に近いものを優先してみる。

本節では全てのノードの中で、サイズが全体の半分に定義を図 4 に示した。プログラムのサイズを求める近いものを選ぶ。サイズが全体の半分に近いものを選関数 size はスライシング開始時に使用され、プログ

んだのち、型推論を行い、どの部分が必要なのか判定

ラムの各ノードにサイズ情報を付与する。search の

4 つめの引数、プログラムサイズ n の情報は choose

する。対象となる部分 exp およびそのコンテキスト
cxt が必要・不要で 3 パターンが存在する †1 。

でノードを選ぶ際に使用される。choose は候補のス(1) 対象となる部分 exp を 2 にしても型がつかライスのリストとサイズ n を受け取り、サイズが最も n/2 に近いスライスとそれ以外のリストを返す。
この手法では、AST の一番上のノードの子ノードない→ exp が不要、(cxt 2) の型エラースライスを求めれば良いの中から、最もそのサイズの半分に近いものを選ぶ。

(2) コンテキストを抽象化しても型がつかない

この手法では、バランスが偏った木でも、小さいもの→ cxt が不要。

を一つ一つ見ていくのではなく、存在するならば、半(3) 対象となる部分、コンテキストの両方が必要分くらいに抽象化したものから見ていくことが可能となる。前節の例 [1;2;3;...;199;true] (要素が 200の場合) では 7.90 秒と、前節の単純なスライシングである→ cxt と exp の両方が必要。cxt を前提とした上で、exp の探索を行うに比べて半分程度の時間となった。これは前節のもの

このような処理を行うために、ふたつのコンテキ

は 1::2 を型推論してから 2::... を行っていたの

ストを用いる。ひとつはそのままのコンテキスト

が、2::... を直接行うようになったからであると考

exp cxt (上の cxt と同じもの)、もうひとつはコンテえられる。

キストの中でもすでにスライスされたものと (スライスの対象ではない) 束縛だけを持つコンテキスト

4 AST の中で最もサイズが全体の半分に近slice cxt である。

いものを優先するスライサー
本節では、プログラム全体の大きさの半分に近いノードを選ぶスライサーを導入する。前節では対象†1 (cxt exp) が型エラーになるプログラムのみがスライサーに渡されるため、両方とも不要なパターンは存在しない。

abst one:slice → slice list

abst one[[S]]=ERROR when S = cl , v ll=[λ x.2] \ (λ x.S)l=[@ 2S1 . . . Sn ; @l 2 . . . Sn ; @l S1 . . . 2] \ (@l S1 . . . Sn )=[@ 2S1 . . . 2; . . . ; @ 22 . . . Sn ] \ (@ 2S1 . . . S2 )abst one[[(S1 , . . . , Sn ) ]]=[(2, . . . , Sn )l ; . . . ; (S1 , . . . , 2)l ; @ 2S1 . . . Sn ] \ (S1 , . . . , Sn )lchoose:slice list → slice ∗ (slice list)

choose(f st :: rest)

=

f st

abst one[[λ x.S]]
abst one[[@ S1 . . . Sn ]]abst one[[@ 2S1 . . . Sn ]]ll(* この引数では呼ばれない *)lsearch:(slice list ∗ (slice → slice) ∗ (unit → slice)) → slice

search([], cxt, f )

=

f ()

search(lst, cxt, f )=let (e, rest) = choose lst in
if (ill typed?(cxt e))then slicing1[[(e, cxt)]]
else search(rest, cxt, f )slicing1:(slice ∗ (slice → slice)) → slice

slicing1[[(2, cxt)]]

=

ERROR

slicing1[[(v, cxt)]]=v

slicing1[[(c, cxt)]]=c

slicing1[[(λx.S, cxt)]]=

search(abst one[[λx.S]], cxt, (f un () →(* この引数では呼ばれない *)search(λx.(slicing1′ [[(S, (f un y → cxt(λx.y)))]]))
slicing1[[(@S1 S2 . . . Sn , cxt)]]=

search(abst one[[@S1 S2 . . . Sn ]], cxt, (f un () →let S1′ = slicing1′ [[(S1 , (f un x → cxt(@xS2 . . . Sn )))]] in
let S2′ = slicing1′ [[(S2 , (f un x → cxt(@S1′ x . . . Sn )))]] in . . .
let Sn′ = slicing1′ [[(Sn , (f un x → cxt(@S1′ S2′ . . . x)))]] in(@S1′ S2′ . . . Sn′ ))slicing1[[((S1 , S2 , . . . , Sn ), cxt)]]=

search(abst one[[(S1 , S2 , . . . , Sn )]], cxt, (f un () →let S1′ = slicing1′ [[(S1 , (f un y → cxt(y, S2 , . . . , Sn )))]] in
let S2′ = slicing1′ [[(S2 , (f un y → cxt(S1′ , y, . . . , Sn )))]] in . . .
let Sn′ = slicing1′ [[(Sn , (f un y → cxt(S1′ , S2 , . . . , y)))]] in(S1′ , S2′ , . . . , Sn′ ))′slicing1 [[(S, cxt)]]=

if S = 2 then 2 else slicing1[[(S, cxt)]]

図3

単純な型エラースライサ

具体例として、型エラーのプログラム (fun x →x (サイズ 6) である。その時のコンテキストは以下の

x + (x + x * x)) 2.0 (サイズ 13) を考える。まずようになる。

最もサイズが全体の半分に近いのは exp = x + x *exp cxt = (λ k.(fun x → x + k)) 2.0

size

:

slice → int

size[[2]]=20size[[c]]=c1

size[[x]]=x1

size[[λx.M ]]=let M s = size[[M ]] in (λx.M s )(s+1)

size[[@M1 ...Mn ]]=let M1s1 = size[[M1 ]] in...
let Mns2 = size[[Mn ]] in@(s1+...+s2+1) M1s1 ...Mns2

size[[(M1 , ..., Mn )]]=let M1s1 = size[[M1 ]] in...
let Mns2 = size[[Mn ]] in(M1s1 , ..., Mnsn )(s1+...+sn+1)

choose:slice list ∗ int → slice ∗ (slice list)

choose(lst, n)=

サイズが最も n/2 に近いスライスとそれ以外のリストを返す

search:(slice list ∗ (slice → slice) ∗ (unit → slice) ∗ int) → slice

search([], cxt, f, n)

=

f ()

search(lst, cxt, f, n)=let (en , rest) = choose lst n in
if (ill typed?(cxt e))then slicing2[[(size[[e]], cxt)]]
else search(rest, cxt, f, n)slicing2:(slice ∗ (slice → slice) ∗ int) → slice
slicing1 の定義中の slicing1 を slicing2 に置き換えたもの
slicing2(M n , cxt) のサイズ n を search を呼ぶ際の 4 つめの引数として渡す

図4

全体のサイズの半分に近い子ノードを選ぶ型エラースライサ

slice cxt = λ k.(fun x → 2 2 k)

これらのコンテキストと式で、先ほど示したパターン

これらのコンテキストと式で、先ほど示したパターを試してみる。slice cxt exp、exp cxt 2 共に型がつンを試してみる。exp cxt 2 は型がつかない。そのこく。よって、exp cxt と exp の両方が必要であることとから exp の部分は全体を型エラーにするために不がわかる。exp cxt を前提として、exp を対象にスラ要であることがわかる。よって対象のプログラムをイシングを行う。

(fun x → x + 2) 2.0 (サイズ 6) と変更し、はじめからスライシングを行う。

(fun x → x + 2) 2.0 の最もサイズが全体の半対象のプログラムが x + 2 と変更された (前提は(λ k. (fun x → k) 2.0))。この時サイズが全体の分に近いノードは exp = x + 2 (サイズ 3) である。

半分に近いと選ばれるノードを exp = + と仮定する。
†2 するとその時のコンテキストは以下のようになる。

その時のコンテキストは以下のようになる。

exp cxt = (λ k. (fun x. k x 2) 2.0)

exp cxt = λ k. (fun x → k) 2.0
slice cxt = λ k. (fun x → k) 2

†2 実際には x も同じ大きさなので、どちらが選ばれる
かは実装に依存する。

slice cxt = (λ k. (fun x → k 2 2) 2.0)
(λ k. (fun x → k) 2.0) が前提となっているた
め、slice cxt にまだスライス済みではない 2.0 が含まれていることに注意してほしい。exp cxt 2 および slice cxt exp は型がつく。よって、+ は型エラーになるために必須であることがわかる。定数 + はス
ライスに必要であると確定したため、+0 のようにサイズを 0 にする。
対 象 の プ ロ グ ラ ム が (λ k. (fun x. x +0 2)

2.0) と変更された。全体のサイズを付け直し、再びはじめからスライシングを行う。上と同じような

図6

リストの長さに応じた各スライシングの実行時間(エラーの原因が最下部にある場合)プロセスで x および 2.0 も必須であることが確定
し、最終結果として、(fun x → x0 +0 2) 2.00 が得られる。

2 節の例 [1;2;3;...;199;true] では、2.92 秒と、単純なスライシングに比べて 1/4、前節のスライシン

図 5 に定義を示した。関数 slice? は、スライスグに比べて 1/2 程度の時間となった。半数ずつに減済み (サイズが 0) の部分を残し、それ以外の部分をらしていった結果、高速化できていることがわかる。

2 で置き換える関数である。これは slice cxt を作るために使われる。関数 sublist は引数の式の、子5 実験と評価

ノードとその環境ふたつのリストを返す。一つ目の本節では、2 節から 3 節の手法がどの程度効率的

環境 exp cxt は子ノードを e としたとき (exp cxt e)に実行できているか、人工的に作成したサイズの大きが引数の式になるようなものである。二つ目の環境

いプログラムを用いて評価を行う。

slice cxt は exp cxt のうちスライス済みの部分はそ

ま ず、前 節 ま で で 使 用 し て い た リ ス ト の 例のままで、それ以外の部分は抽象化した環境である。

([1;2;3;...;199;true]) で長さを変更した実行結関数 pickup は一つ目の引数 exp の中から、四つ目

果を図 6 に示した。図からわかるように、どの手法での引数 n の半分の大きさに近いノードを見つけて返もリストの長さが長くなるほど、実行時間がかかる。

す関数である。同時にその exp cxt と slice cxt も返

slicing1 の実行時間を見てみると、単純な比例ではなす。定義中の biggest の定義は省略してあるが、リスい。長さを n とした時の実行時間 t はおおよそ t =トの中から最も大きい式を選んで返す関数である。

0.00025 * n2 となる。これはリストの長さの回数分、

関数 update はスライスを受け取り、サイズを再リストの長さのプログラムの型推論が行われている

計算して付与したのち、全体がスライス済みならばことに起因すると考えられる。slicing2 の実行時間を終了して結果を返し、スライス済みでなければ再び見てみると、長さが 600 までは slicing1 のおおよそ

slicing3 を呼び出す関数である。id は初期の環境で、半分である。これは (n :: 2) ではなく (2:: ...)

f un x → x で表される。関数 slicing3 はスライサー

がはじめに実行されていることに起因すると考えられのメイン関数である。パターン分けを行い、不要なる。slicing3 の実行時間を見てみると、長さを n とコンテキストおよび式を置き換えて、スライシング

した時の実行時間 t はおおよそ t = 0.00005 * n2 とを進める。update を呼び出している部分は、葉まで

およそ 1/5 になっている。

到達したので再び AST の全体をスライシングしてい

上の例は AST の右側への偏りがある例であるが、る。slicing3 に再帰している部分は、exp cxt もしく

左側への偏りも同様の傾向が見られる。足し算の例

は hole cxt を前提にして、子ノードのスライシング(true + 1 + 2 + ....

を行っている。

に示した。前の例に比べて、slicing2 および slicing3+ 199) の実行結果を図 7

れている例を考える。その実行結果は以下のようになる。

slicing1: 0.048731 (sec)slicing2: 0.061794 (sec)slicing3: 0.013203 (sec)
この例では slicing3 が最も早いが、エラーの原因である bool の値を入れる場所を変更すると、それぞれのスライシング手法で 0.02 〜 0.09 程度で変化し、slicing2 が最も早いこともあった。
図7

足し算の長さに応じた各スライシングの実行時間

また、要素のほとんどがエラーの原因であるような例 fun x -> fun y -> fun z -> fun a -> fun m(エラーの原因が最下部にある場合)-> fun n -> fun k -> fun l -> (x = y, y = z,z = a, a = m, m = n, n = k, k = l, x = 2.0, l= 3) では、
slicing1: 0.110034 (sec)slicing2: 0.029109 (sec)slicing3: 0.064413 (sec)という結果が得られた。

slicing1 では要素を選ぶ操作をしていない分、うまくいった場合のコストが小さいと考えていたが、実験前に想像していたよりもコストは実験からは確認で
図8足し算の長さに応じた各スライシングの実行時間きなかった (図 8 の例は、主にその例では非効率な順序であったことに起因すると考えられる)。多くの例(エラーの原因が最上部にある場合)

では slicing3 が早いことが多いことがわかる。今後の上がり幅が抑えられている原因はコンストラクタ

は人工的な例だけではなく、実際のプログラムで実験と関数適用の違いかと思われるが、現在さらなる実験と評価を行いたい。

で確認中である。
これらの例は AST の最も下の部分に型エラーが6 まとめと今後の課題

含まれている場合で、slicing3 に有利な例であった。

本論文では、型エラースライスの効率的な求め方にそのため、最も不利な場合、最も上部に型エラーのついて提案と実験を行った。新たに導入したのは二つ

原因が含まれている場合 (1 + 2 + ....

+ 199 +の型エラースライサーである。既存研究 [5] での単純

true) を考える。その際の実行結果を図 8 に示した。

な型エラースライサーを改良し、全体のサイズの半

slicing1 と比較して slicing3 は遅いことがわかる。こ分に近い子ノードを選ぼうとする slicing2 と、全体

れは slicing2 や slicing3 では様々な処理を行っていをおよそ 1/2 に分けるノードを選ぶ slicing3 を導入

るほか、この例では非効率なスライシング順序を選んした。

でいることによる。一方で、一つ目の例や二つ目の例

人工的に作成した大きいリストや足し算の例では、の slicing1 に比べて現実的な時間で抑えられている。

エラーの原因が含まれる場所に依存するが、おおよ

これまでの三つの例は、AST に偏りがある場合でそ slicing3 が高速であることが多いことが確認されあった。よって次には平衡木を考える。要素 512 のた。一方で、例によっては slicing1 の方が早い場合

足し算の完全な平衡木で、一つだけ bool の値が含まもあった。

今後の課題は三つ挙げられる。一つ目は実際のコードでの実行時間比較である。実際の型エラーのプログ
ラムの型エラースライシングではどの手法が効率的かの評価を行いたい。二つ目は更なる効率化である。
型エラーのメッセージで指摘された箇所をあらかじめスライシングに組み込むなどでさらに効率化できないか確認したい。三つ目は複数の手法をハイブリッドに用いて高速化する方法がないかの検証である。プロ
グラムが小さくなると要素を選ぶコストが存在しな
い slicing1 の方が早い場合も存在する。要素数が少なくなった場合には、slicing3 から slicing1 に切り替える等でより高速化できないか検討したい。

参 考 文 献[ 1 ] Chitil, O. “Compositional Explanation of Typesand Algorithmic Debugging of Type Errors,” Proceedings of the 6th ACM SIGPLAN International
Conference on Functional Programming (ICFP
01), pp. 193–204 (2001).
[ 2 ] Haack, C. and Wells, J. B.. “Type Error Slic-ing in Implicitly Typed Higher-Order Languages.”
Science of Computer Programming - Special issue on 12th European Symposium on Programming(ESOP 03), Volume 50 Issue 1-3 (2004).
[ 3 ] Schilling, T. “Constraint Free Type Error Slicing,” Proceedings of the 12th International Conference on Trends in Functional Programming (TFP’
11), pp. 1–16 (2012).
[ 4 ] Stuckey, P. J., Sulzmann, M. and Wazny, J.. “Interactive type debugging in Haskell,” Proceedingsof the 2003 ACM SIGPLAN Workshop on Haskell,pp. 72–83 (2003).
[ 5 ] 対馬 かなえ, 浅井 健一, “重み付き型エラースライスの提案”, コンピュータソフトウェア, Vol.31 (2014),
No.4, pp. 131–148 (2014).
[ 6 ] 対馬 かなえ, 浅井 健一, “コンパイラの型推論を利用した型デバッグ手法の提案”, コンピュータソフトウェ
ア, vol.30, no.1, pp. 180–186 (2013).
[ 7 ] 脇川 奈穂, 対馬 かなえ, 浅井 健一, “型エラースラ
イシングを利用した型エラーデバッガに関する実装と考察”, 第 58 回プログラミングシンポジウム 予稿集.
[ 8 ] Tsushima, K., and Asai, K.. “An Embedded
Type Debugger,” Proceedings of the 24th International Workshop on Implementation of Functional
Languages (IFL’12), Springer, LNCS 0302–9743,
pp. 190–206 (2013).

slice?

:slice → slice

slice?(S 0 )=S when S = v or cnslice?(S )=2 when S = v or c

l1=

let S ′l2 = slice?(S) in

slice?(λ x.S)

if l2 = 0 then λ0 x.S 0 else λl1 x.S ′l2
slice?(@l S1 ...Sn )=let S1′l1 = slice?(S1 ) in ...
let Sn′ln = slice?(Sn ) inif (l1 = 0 ∧ ... ∧ ln = 0) then (@0 S1′0 ...Sn′0 )else (@l S1′l1 ...Sn′ln )slice?((S1 , ..., Sn ))=関数適用の場合とほぼ同様なので、省略

sublist:slice → (slice ∗ (slice → slice) ∗ (slice → slice)) list

sublist[[S]](* この引数では呼ばれない *)=ERROR when S = v or clsublist[[λ x.S]]=[(S, (f un k → λ x.k), (f un k → λl x.k))]sublist[[@l S1 ...Sn ]]=[(S1 , (f un k → (@l k...Sn )), (f un k → (@l k...(slice? Sn ))));l...; (Sn , (f un k → (@l (slice? S1 )...k)))]siblist[[(S1 , ..., Sn )]]=関数適用の場合とほぼ同様なので、省略: slice ∗ (slice → slice) ∗ (slice → slice) ∗ int → (slice ∗ (slice → slice) ∗ (slice → slice))

pickuppickup(exp, exp cxt, hole cxt, n)

let subs = sublist exp in′let (exp′n , exp cxt, hole cxt) = biggest subs in′

if n/2 > n′ then (exp′n , exp cxt exp cxt′ , hole cxt hole cxt′ )′else pickup (exp′n , exp cxt exp cxt′ , hole cxt hole cxt′ )update:slice → slice

udpate(exp)=

let exp′n = size[[exp]] in
if n = 0 then exp′
else slicing3[[(exp′n , id, id)]]slicing3:

slice ∗ (slice → slice) ∗ (slice → slice) ∗ int → slice

slicing3[[(2, exp cxt, slice cxt, n)]]=ERROR (* この引数では呼ばれない *)slicing3[[(S, exp cxt, slice cxt, n)]]=if illtyped? (hole cxt exp) then update (hole cxt e0 )
else if illtyped? (exp cxt 2) then update (exp cxt 2)

when S = v or celse update (exp cxt e0 )slicing3[[(S, exp cxt, slice cxt, n)]]=if illtyped? (hole cxt exp)
then let(exp′ , exp cxt′ , hole cxt′ ) = pickup (exp, id, id, n) inthenslicing3[[exp′ , (hole cxt exp cxt′ ), (hole cxt hole cxt′ )]]else if illtyped? (exp cxt 2) then update (exp cxt 2)
else else let(exp′ , exp cxt′ , hole cxt′ ) = pickup (exp, id, id, n) inelse else slicing3[[(exp′ , (exp cxt exp cxt′ ), (exp cxt hole cxt′ ))]]

図5

全体で半分に近いノードを選ぶスライサー