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

型付き DSL に対するプログラム変換の型安全なフレー
ムワーク
高木 尚

亀山 幸義

領域特化言語（DSL）の設計においては，型による安全性が重要である．コンパイラやプログラム変換の記述は誤りが発生しやすく，出力を確認しデバックするのは現実的ではない．DSL を型付きで埋め込み，プログラム変換実装
におけるミスを事前に取り除くことを目指す．型を保存する変換のみを許すことで，プログラム変換に安全性を与える試みがあるが，従来の手法では記述が困難な変換が存在する．自由変数を含むコードの解析や，MGU(最汎単一化子) の計算を行う変換は難しく，特にスーパーコンパイラという最適化は安全な実装ができるかわかっていない．本
研究では，従来の高階抽象構文 (HOAS) で表現していたコードを，型付き de Bruijn インデックスを用いたコードの表現に変換することで，型安全性を保ったまま表現力の拡張を図ったフレームワークを提案する．フレームワーク
におけるスーパーコンパイラの実装を通して，その表現力について検討を行った．

け規則もホスト言語に埋め込むことにより，DSL の

1 導入

項の型付けをホスト言語の型システムで行う点にあ

1. 1 DSL とタグレスファイナル法

る．この手法は，DSL のプログラムの型エラーを静領域特化言語 (DSL) は，特定の問題領域における的に発見できるだけでなく，DSL のプログラム変換処理の記述のために，広く用いられている．DSL のが型付けを保存しないことも静的に発見できる．その実現方法には，様々なものがあるが，多種多様な DSL

ため，DSL に対する様々な領域固有の最適化を実装が比較的短期間に設計・開発され改訂されていく，とするプログラマにとっても利点がある．Kiselyov らいう状況のもと，開発・設計・最適化等を軽量にでは，SQL のクエリ最適化 [8] や部分評価などの領域にきる DSL 開発手法 (フレームワーク) に注目が集まっ

タグレスファイナル法を適用している．

ている．軽量に開発される DSL は，多くの場合，汎タグレスファイナル法によるプログラム変換の記用プログラミング言語に埋め込まれるかたちで実現

述は，静的に型が付く保証が得られるという利点がされ，DSL のプログラムに対する最適化は，埋め込ある一方で，記述の容易さにおいて問題がある．そのまれたコードに対するプログラム変換として実現さ原因は，変数束縛の表現方法であり，通常のタグレスれる．

ファイナル法は，高階抽象構文 (HOAS) を利用してKiselyov らによるタグレスファイナル法 [3] は，静変数束縛を表現するため，項の中の変数を直接取り的に型付けられた DSL(以降では型付き DSL と呼ぶ)

扱う変換を表現するのが容易ではないといったことを汎用プログラミング言語に埋め込む手法である．埋や，閉じた項のみが表現可能であるといった問題がめ込み先の言語をホスト言語と呼ぶ．タグレスファイある．この問題を回避するためには，(1)de Bruijn イ

ナル法の特徴は，DSL の構文だけでなく，その型付

ンデックスによる表現を導入する [4]，(2) 弱高階抽象

The type safe framework for program transformationsof typed DSL
Sho Takaki
Yukiyoshi Kameyama, 筑波大学コンピュータサイエンス専攻, Dept. of Computer Science,
University of Tsukuba.

構文 (WHOAS) による表現を導入する，(3) 依存型を持つ言語をホスト言語として型文脈を直接扱う [1]，という方法がある．しかし，(1) は，DSL のプログラ
ム記述が簡便ではなくなる，(2) は WHOAS を用い

ても変数の束縛の構文においては HOAS と同様の扱いにくさがあるという点，(3) はホスト言語そのものが拡張されて煩雑になるという問題がある．一方で，この問題はタグレスファイナル法そのものに起因するのではなく，既存の枠組みの上に，変換を表現できる
幅を広げる仕組みを構築することは可能であると我々は考えている．

1. 2 提案方式
本研究では，これらの観察をもとに，タグレスファ
イナル法において，外部的・表層的には HOAS を用い，内部的には必要に応じて，型付き de Bruijn イン
デックス (以降 TDB と表記する) を用いるというハ
イブリット型プログラム変換フレームワークを提案
する．2 つの表現間の変換は，個々の DSL に依存しないためフレームワークが提供を行う．TDB への変図1

提案方式による最適化

換および TDB 上での操作は一貫して型の保証が保たれるため，全体を通して型の保証は保たれる．図 1

告する．第 5 章では，研究内容と成果についてまとは，提案方式による最適化の概略である．DSL の最め，今後の研究課題について述べる．

適化の開発者は本フレームワーク上で，基本的にはHOAS を用いて最適化を記述する．同時に，パター

2 埋め込み手法

ンマッチや変数操作を含む最適化では TDB を用いる

2. 1 対象言語の一例ということが可能になる．プログラム変換を記述する

この論文では，具体的な説明をするため、対象となのに適切な表現形式を選択できるフレームワークをる DSL を 1 つ固定して考える．これの構文を図 2 に提供し，プログラム変換を記述する際の負担が軽減す示す．

ることが本研究の目的である．

型付け規則の一部として，関数と変数に関わる規則
は図 3 の通りである．

1. 3 本論文の構成
本論文は，本章を含め全 5 章から構成される．

2. 2 高階抽象構文

第 2 章では，型付き DSL として対象言語の一例を

高階抽象構文 (HOAS) は，ホスト言語の関数とし

提示し，それが HOAS と TDB の双方でどのようにて対象言語のコードを表現する．加えて，関数の型をメタ言語上で表現されているかについて述べる．第 3

設定することで，DSL に型安全性を与える．関数の章では，本研究の提示するフレームワークの実装方式，

型の設定方法はホスト言語により異なるが，今回は並びに使用方法について説明する．加えて，HOAS

OCaml をホスト言語としてモジュールのシグネチャ

上では，素直には実装が難しかった変換のプロセスにに記述する．対象言語の一部について対応する関数のついて例を挙げ，TDB 上ではどのように行うかにつ型を記述したシグネチャの一部をソースコード 1 にいて述べる．第 4 章では，本フレームワークをもち示す．シグネチャは，モジュールの型を示すものであいて，複雑な変数操作を必要とするプログラム変換をり，val で宣言したものが，モジュールにおける関数

記述することに向けての課題を，スーパーコンパイラの型に対応する．type ’a exp で宣言しているのは，[9] というプログラム最適化の手法の実装を通して報抽象型といい，ここでは具体的な型を設定しない．シ構成子がホスト言語上の関数であることと，3. 3. 1 節

t ::=v (変数),

で述べるように tlam の内部には，関数適用行わなけ

f t1 . . . tn (関数適用)

nil (空リスト),

ればアクセスできないことから，パターンマッチや項

cons(t,t) (リスト構成子)同士の比較を正しく実装することは容易ではない．

case t : τ list of [] → t | (vh : vtl ) → t (case 式)
if v = t then t else t (if 式)

2. 3 型付き de Bruijn インデックス (TDB)f ::=本研究では，TDB を，ホスト言語の一般化代数

λv1 : τ1 . . . . λvn : τn .t (関数)データ型を用いて埋め込むことにより表現する．ソー

fix(f : τ ) (再帰関数)

スコード 2 は，OCaml をホスト言語として対象言語

fix2(f : τ and f : τ ) (相互再帰関数)

でコードを表すデータ構造の一部である．型 index,

fst(f ) (左抽出),

tTerm は共に型パラメータが 3 つ設定されており，1

snd(f ) (右抽出)τ ::=char (文字型),

つ目が型環境，3 つ目が表現型をさす．⊢ の左の型環

bool (真偽値型)

τ list (リスト型),(τ ,τ ) (組型),

境を第 1 パラメータ，右の表現型を第 3 パラメータとτ → τ (関数型)

みて，型規則と同様の形式をしていることがわかる．
型パラメータの 2 つ目は，プログラム変換で一時的

図2

対象言語

に用いるもので関数の型環境を表す．
変数は，通常の de Bruijn インデックスと同様に，グネチャを実装したモジュールにおいては，この型を変数束縛の位置をインデックスで示したものを変数の個別に具体化することができる．

代わりに用いる．

GADT では，データの構造により設定される型がソースコード 1 HOAS による対象言語の埋め込み
module type THOAS = sig
type ’a exp
val tlam :’a typ-> ( ’ a exp -> ’b exp )-> ( ’ a -> ’b ) exp
val tapp :( ’ a -> ’b ) exp-> ’a exp-> ’b exp...
end

注目するべきは，ラムダ抽象の構造である．ラムダ抽象の第 2 引数の型は，(’a exp -> ’b exp) であり，これはホスト言語上のラムダ式に対応する．例
えば，λx : bool.cons(x,nil) は，tlam (Bool) (funx -> cons x nil) となる．この x のように，各変数の管理は，ホスト言語上に委譲されるため，束縛されていない変数や，誤った型での変数の扱いはホスト言語の型検査によって防止することができる．
一方で，自由変数を表現することができないため，全ての項は閉じていなければならない．加えて，項の異なるため，DSL の型を埋め込むことができている．
また，パターンマッチや項同士の比較も容易に実装ができる．一方で，変数がインデックスになるため，可読性が低く，プログラム変換の際にも変数を適切に操作することが求められる．
ソースコード 2 TDB による対象言語の埋め込み
type (_ , _ , _ ) index =| Z : ( ’ a -> ’g , ’d , ’a ) index| S : ( ’g , ’d , ’b ) index-> ( ’ a -> ’g , ’d , ’b ) index

type (_ , _ , _ ) tTerm =| TVar : ( ’g , ’d , ’a ) index-> ( ’g , ’d , ’a ) tTerm| TLam : ’a typ *( ’ a -> ’g , ’d , ’b ) tTerm-> ( ’g , ’d , ( ’ a -> ’b ) ) tTerm| TApp : ( ’g , ’d , ’a -> ’b ) tTerm *( ’g , ’d , ’a ) tTerm-> ( ’g , ’d , ’b ) tTerm...

(v : τ ) ∈ Γ(T-Var)Γ⊢v:τ

Γ, (v : τ1 ) ⊢ t : τ2
(T-Lam)Γ ⊢ λv : τ1 .t : τ1 → τ2
図3

Γ ⊢ t1 : τ1 → τ2 Γ ⊢ t2 : τ1
(T-App)Γ ⊢ t1 t2 : τ2

対象言語の型付け規則の一部

2. 4 結合関数の例)

2 つのリストを受け取り，結合させたリストを返す
関数は，まず，対象言語の構文では，以下のように定義される．

3 両表現を併用するフレームワーク
まず，両表現をタグレスファイナル上にハイブリッ

fix(λf : char list → char list → char list.
λx : char list.λy : char list.
case x : char list of [] → y | (xh : xtl ) →cons(xh ,f xtl y) :char list → char list → char list)
この関数を HOAS を用いて埋め込むと次のようになる．
ソースコード 3 HOAS による結合関数
fix ( Arrow ( List ( Char ) ,Arrow ( List ( Char ) , List ( Char ) ) )( tlam ( Arrow ( List ( Char ) ,Arrow ( List ( Char ) , List ( Char ) ) ) )( fun f ->tlam ( List ( Char ) ) ( fun x ->tlam ( List ( Char ) ) ( fun y ->case ( Char ) x y ( fun xh xtl ->cons ( xh ) ( tapp ( tapp f xtl ) y )
)
)
)
)
)

TDB では次の通りである．
ソースコード 4 TDB による結合関数
Fix ( Arrow ( List ( Char ) ,Arrow ( List ( Char ) , List ( Char ) ) ) ,TLam ( Arrow ( List ( Char ) ,Arrow ( List ( Char ) , List ( Char ) ) ) ,TLam ( List ( Char ) , TLam ( List ( Char ) ,Case ( Char ,TVar ( S Z ) ,TVar ( Z ) ,Cons ( TVar ( Z ) ,TApp ( TApp ( TVar ( S ( S ( S ( S Z )) ) ) , TVar ( S Z ) ) ,TVar ( S ( S Z ) ) ) ) ))))トに構成する方法を述べ，開発者視点での使用法と，

HOAS では正しく記述することが困難な操作についての，本フレームワークでの実装を説明する．

3. 1 フレームワークとタグレスファイナル
タグレスファイナル法では，対象言語に対するプ
ログラム変換を，ファンクタすなわちモジュール間の関数として実装する．ファンクタの内部では，プ
ログラム変換の最中，一時的に，コードを GADT で保持することが可能である [5]．これに，TDB を表現
する GADT を適用することにより，本フレームワー
クは設計されている．ソースコード 5 にあるのが，GADT として TDB 表現を採用したファンクタである．DBLib がファンクタ名で，F が引数のモジュール(今回は HOAS シグネチャを実装したもの) である．
ソースコード 5 TDB を採用するファンクタ
module DBLib ( F : THOAS . THOAS ) = structmodule X = structtype ’a f = ’a F . exp
type ( ’g , ’d ) ctx =| CtxZ : ( unit , ’d ) ctx| CtxS : ’a typ * ( ’ ctx , ’d ) ctx-> ( ’ a -> ’ctx , ’d ) ctx

type ’d funs = EMPTY : unit funs
type ’a exp ={ contents : ’c ’d .
( ’c , ’d ) ctx ->’d funs ->( ’c , ’d , ’a ) tTerm }type ’a t =| Term : ’a exp -> ’a t
| Ukn : ’a f -> ’a t...
let fwd : type a . a f -> a t =fun t -> Ukn tlet bwd : type a . a t -> a f =function| Term ({ contents = c }) ->toHOAS TENil CtxZ TFNil ( c CtxZ
EMPTY )
| Ukn t -> tend
open X
module IDelta = struct
let tlam t f = (* to TLam *)let tapp x y = (* to TApp *)...
end

3. Case(..., TVar(S Z)) は，1, 2 と同様に case...

(fun h tl -> tl) に変換される．

TDB を用いるファンクタにはすべて，この相互変換を実装しなければならないが，本研究では，これを分離することに成功した．TDB を用いて最適化を記述する開発者は，本ライブラリを用いることで，記述したいプログラム変換のみに注目するコーディングを行うことができる．

3. 2 使用法

end’a t は，このファンクタ内でのコードの表現を表している．ここに’a exp を使用可能にすることで，TDBをファンクタ内の主要な表現として採用する．TDBから HOAS への変換は，toHOAS に記述し，HOAS
から TDB への変換は，各構文を構成する関数 (tlam，

tapp 等) の関数定義として記述する．具体的な TDB・
HOAS 相互変換は， [2] を元に実装を行ったため詳細は省くが，例をもとにアルゴリズムについて簡単に述

ソースコード 6 にその使用例を示す．このファン
クタでは，スーパーコンパイラの変換手続きを TDB上で行う SC.sc という関数を，sc というタグのある
位置から適用するという処理を記述している．DBLib
ファンクタの中に実装された TDB・HOAS 間の変換
を include 命令を使って展開する．HOAS の構造を意識することなく TDB での処理を書くことができて
いる．

べる．

ソースコード 6 最適化実装の一例
module SC ( F : THOAS . THOAS ) = structmodule Lib = LibTDB . DBLib ( F )例に考える．HOAS では，tlam t1 (fun x -> tlam
module X = struct
t2 (fun y -> cons x y)) という関数を含む項であinclude Lib . X
end
る．これを TDB の表現すなわち TLam(t1, TLam(t2,open X
Cons(TVar(S Z), TVar(Z)))) に変換する場合を考
module IDelta = struct
include Lib . IDelta
える．tlam の変換は，x や y に何を代入すればよい
let sc ( Term ({ contents = body }) ) =かという問題が主である．今回 HOAS の各変数は’a
let t =
exp 型である．したがって，変数が登場する位置のコ
fun i funs ->let unifier =ンテクスト (’c, ’d) ctx を参照することが可能でShift . ctx _to_un ifier i in
ある (これを j とおく)．tlam のコンテクスト (i とお
let memo =SC . ctx_to_memo iく) を記録しておけば，適切なインデックスを両者のin SC . sc
差分 (j − i) により計算することができる．例えば，
unifiermemo
ここでの x は 1 − 0 = 1，y は 1 − 1 = 0 となる．
i
逆に，TLam(List(t), Case(t, TVar(Z), TVar(Z),( TDB . FNil )TVar(S Z))) を HOAS に変換するプロセスは以下の( body i funs )in Term ({ contents = t })通りである．
end
1. TLam(List(t), ...) を tlam (List(t)) (fun end

tlam の実装として，λx : τ1 .λy : τ2 .cons(x,y) を

x -> ...) に変換し，x を先頭の環境に入れる．
2. Case(t, TVar(Z), TVar(Z), ...) の TVar(Z)，は環境から引かれ x に置換される．

module PSC ( F : SYMOBS ) = structmodule OptM = SC ( F )include SYMT ( OptM . X ) ( F )include OptM . IDeltaend

なお，自由変数が増えてしまうような変換を記述した場合，ホスト言語の型検査により静的に発見することができる．例として，自由変数が 1 つだけ許されている環境において，その変数にインデックス 1を代入するような変換を書く．以下のソースコード 7
は，その変換を sc というタグのある位置から実行した例である．substitute0 は，インデックス 0 に対して代入を行う関数である．

数 で あ る ．λx : τ1 . よ り 内 部 に ど の よ う な 項
が あ る か は ，関 数 fun x -> ... に 適 用 を 行 わ な
い 限 り 調 べ る こ と が で き な い ．一 方 ，TDB に
お い て は ，TLam(t1, TLam(t2, Cons(TVar(S Z),

TVar(Z)))) となり，ホスト言語の通常のパターン
マッチにより構文を調べることができる．

3. 3. 2 変数の使用不使用判断あるコードにおいて，各変数が使用されているかどうかを判定することが必要とされる場面がある．例えば，ソースコード 9 のループを含むコードについて

ソースコード 7 型エラーになる変換 (ctx over.ml)
let sc body =match body with| Term ({ contents = body }) ->let cnt : type c d .
(c , d ) ctx ->d funs ->(c , d , ’a ) tTerm =function| CtxS (_ , _ ) as i - >fun funs ->let term = body i funs in(* 24 *) substitute0 term ( TVar ( S Z ) )| i -> fun funs -> body i funsinTerm ({ contents = cnt })考える．
ソースコード 9
for i in item do
let x = 10! in
job x i ;
done

変換前

x = 10!は不変式であるから let 束縛を持ち上げ，
ソースコード 10 のプログラムに変換したい．
ソースコード 10
let x = 10! infor i in item do
job x i ;
done

変換後

このコードは，以下のようにホスト言語の型検査を通過しない．インデックス 1 が現在の環境では許されていないからである．

そのためには，x = 10!に変数 i が登場しないことを判定する必要がある．この判定は，TDB において素直に実装が可能である．

ソースコード 8 型エラーメッセージ
File " over_ctx . ml " , line 24 , characters
39 -40:Error : This expression has type ( ’ a -> ’
b , ’c , ’a ) TDB . index
but an expression was expected oftype ( $1 , d , $0 ) TDB . index
Type ’a -> ’b is not compatible
with type $1

出力として，次の used というデータ構造をおく．
ソースコード 11 出力のデータ構造
type ’g used =| Empty : unit used
| Used : ’a typ * ’g used-> ( ’ a -> ’g ) used
| NUsed : ’a typ * ’g used-> ( ’ a -> ’g ) used

このデータ構造は，インデックスに対応したリスト

3. 3 TDB による各種操作の構造をしている．外側が若いインデックスである．

3. 3. 1 構文的解析

例えば，1,3 が使用されている場合，これに対応する

TDB は一階のデータ構造のため，パターンマッチ

出力は NUsed(t0, Used(t1, NUsed(t2, Used(t3,が可能である．例えば，λx : τ1 .λy : τ2 .cons(x,y) は，

Empty)))) となる．型パラメータに型環境’g を取っ

HOAS では，tlam t1 (fun x -> tlam t2 (fun yており，インデックスの増減に対して，不適切な操作-> (cons x y))) で あ り，tlam の 第 2 引 数 は 関が行われた場合，ホスト言語の型検査により発見できる．
各インデックスの使用不使用を判定した結果を出力する関数 vsearch の一部は次のようになる．
ソースコード 12 使用不使用判定関数
let rec vsearch : type g a d . g used ->(g , d , a ) tTerm -> g used =let rec write : type g a d . g used ->(g , d , a ) index -> g used =fun u i ->match u , i with
| NUsed (t , u ) , S i ->NUsed (t , write u i )| Used (t , u ) , S i ->Used (t , write u i )| NUsed (t , u ) , _ -> Used (t , u )| _ , _ -> uin
let pick : type g a . ( a -> g ) used ->g used =function| NUsed (_ , u ) -> u
| Used (_ , u ) -> uin
fun u term ->match term with
| TVar ( i ) -> write u i| TApp (f , arg ) ->let u ’ = vsearch u arg invsearch u ’ f| TLam (t , body ) ->pick ( vsearch ( NUsed (t , u ) ) body )...

ソースコード 13 mapto0 の型
mapto0 : type a b g d .
( b -> g , d , b ) tTerm ->( b -> g , b -> g , d ) inx_term

戻り値にある inx term は，インデックスから項への関数を保持するデータ型である．次のように定義されている．
ソースコード 14 inx term
type ( ’ g1 , ’g2 , ’d ) inx_term ={ mapto : ’a . ( ’ g1 , ’d , ’a ) index ->( ’ g2 , ’d , ’a ) tTerm }次に，インデックス 1，インデックス 2，・・・に代入するためにはこの戻り値 (inx term) を持ちあげればよい．この持ち上げる関数の型は次の通りである．
ソースコード 15 exts の型
exts : type g1 g2 b d .
( g1 , g2 , d ) inx_term-> b typ-> ( b -> g1 , b -> g2 , d ) inx_term

第 2 引数にあるように，持ち上げる型が判明しなければならない．TDB がチャーチスタイルを採用している理由の 1 つである．

4 スーパーコンパイラ
スーパーコンパイラ [9] は，既に判明している変数の値と，分岐などから得られる情報に基づくプログラ3. 3. 3 代入

ムの最適化の技術である．得られた情報よりプログラ

代入は，HOAS においては想定することが難しい

ムの記号的実行を進めて，もとのプログラムより高性操作である．そもそも HOAS のコードは全て閉じて能な残余プログラムを生成する．今回実装を行うスー

いることが条件であるから，代入対象の変数を考え

パーコンパイラは [7] に則ったものである．一例としることがないからである．例えば，λy.λx.cons(x,y)てソースコード 16 を考える．

に，x = true を代入するというのは不適切な操作である．一方，前述のようにスーパーコンパイラにおいては，開いた項を扱い，自由変数に対して代入を行う必要もある．以後の実装は，依存型をもつ言語による

TDB の実装 [6] を元に構成したものである．
まず，代入する値を受け取り，インデックス 0 に代入を行う関数を生成する関数 (mapto0) の型は次のソースコード 13 である.

ソースコード 16 変換前
case ss of[] -> false(s ’: ss ’) -> if s ’ = pthen f ss
else true

3 行目の ss は，s′ = p が真である分岐の中にあり，また，case 式における分解可能な場合に位置するため，より詳しい表現にすることができる．実際にこの式に対して，変換を行うと以下のソースコード 17 が得られる．

行する必要が生じる．今回は部分的に負のインデックスを導入することでこの問題を解決した．一方で，負ソースコード 17

変換後case ss of[] -> false(s ’: ss ’) -> if s ’ = pthen f cons (p , ss ’)else trueのインデックスは不適切に扱うとコード生成時にエラーを生じてしまう問題がある．

4. 1. 2 相互再帰関数定義
スーパーコンパイラにおいては，ソースコード 18のように相互再帰の関数定義を動的に拡張する必要

このようにして得られた情報を用いて，処理を進がある．関数定義の拡張は，現在プログラム変換中のめて case 式や if 式を展開していく．また，関数がスコープとは異なる場所に定義をしなければならなあった場合は定義を展開する．再帰的な関数の場合いという点で難しい．また，引数の自由変数を発見しは，プログラム変換が停止しなくなってしまうことて新しく定義する関数の引数にセットするという操作をさけるため，folding という操作で展開を停止す

も同時に行う．これらの操作は HOAS から TDB にる．例えば，2 つのリストを結合する関数 append

変換してもなお，困難なものであるが，次の生成方法に cons(x,xs) と ys を適用した後，スーパーコンに変更することで folding 操作を実装した．

パイラに適用した場合を考える．append の関数定義が，2. 4 節のものに従う場合，変換後は，ソース

再帰関数のスコープ 関数をコピーして変換途中のスコープの内部に配置する

コード 18 になる．ただし，let f x = t in f y は，HOAS における任意の相互再帰の関数 HOAS に

fix(λf : τ1 → τ2 .λx : τ1 .t : τ1 → τ2 ) y の糖衣構文戻す際に，相互再帰から入れ子の再帰関数に変更

である．

する
引数の自由変数を関数の引数にセット 引 数 に 関

ソースコード 18 変換後の結合関数
let h1 xs ys = cons (x , h2 xs ys )andh2 xs ys =case xs of[] -> ys
| ( h : tl ) -> cons (h , h2 tl ys )in h1 xs ys

新たに，h1，h2 という関数を相互再帰的に定義し，元の再帰の構造を畳み込んでいる．この手続きにより，スーパーコンパイラは停止性を保っている．

4. 1 実装にあたっての困難点

わらず全ての自由変数を関数の引数にセットする
この生成方法に則ると append cons(x,xs) ys は，
ソースコード 19 に変換される．
ソースコード 19 本方式の結合関数の変換例
let h1 x xs ys = cons (x ,( let h2 x xs ys =case xs of[] -> ys
( h : tl ) -> cons (h , h2 x tl ys )in h2 x xs ys ) )in h1 x xs ys

スーパーコンパイラの実装にあたっては、本フレー
ムワークにおいても実装が困難な操作が存在した．

4. 1. 1 小さなインデックスへの代入

4. 2 実験の総括
実験の成果としては，変数操作を含むプログラム変3. 3. 3 節にある実装では，大きいインデックスを小換のプロセスを実際に TDB 上で実装することができ

さいインデックスに置き換えるような代入を記述す

ることがわかったという点である．構文的解析や代入ることはできない．例えば，λx : bool.y に対して，

操作および，関数定義などは，HOAS 上では実装がy = x という代入を適用するのは，想定されていな

難しいものであったが，TDB に変換することで，平かった．しかしながら，スーパーコンパイラにおいて易に実装することができた．本フレームワークで実装

はソースコード 17 のように，ss = cons(p,ss′ ) を実されたスーパーコンパイラは，前述の妥協点はあった図4

部分文字列照合の最適化 (比較回数)

図5

部分文字列照合の最適化 (実行時間)

ものの，最適化プロセスにおいて型を保存すること，

フレームワークの記述力を調査するため，スーパーコスコープの誤りやインデックスの取り違えが発生しなンパイラを実装を試みた．実装に際して，変換のアルいことを保証できている．

ゴリズムを変更しなければならない点や，変換の安全

最後に，実装したスーパーコンパイラについて，性性について一部妥協しなければならない点が生まれ能の検討を行ったものを付記する．スーパーコンパイ

た．今後の課題としては，実装できたスーパーコンパ

ラは，部分文字列照合のプログラムについて，照合しイラについて，求められる性能が出ているか検討する

たい文字列に特化したコードを生成することができ

ことと，WHOAS など他の埋め込み手法についてもる．特化したコードが KMP アルゴリズムに従うも同様の方式で導入できないかといった点である．

のになっているかは，スーパーコンパイラの性能を評
参 考 文 献価する上の指標となる．
k

1000k

照合文字列を A B ，検索をかける文字列を ABとして，変換前と変換後で比較を行なった．
図 4 は文字の比較回数についての結果である．変
換前の比較回数は非線形に増大しているが，変換後の比較回数は線形に推移していることが見て取れる．
比較回数で見ると変換による効率化が実現できていることが分かる．
一方で，全ての自由変数を引数にセットするように変更したことが影響し，現時点で実行速度の面では，望ましい性能には至っていない (図 5)．

5 まとめと今後の課題
本研究が提案するフレームワークは，タグレスファ
イナル法を拡張し，より変数の扱いが多様なプログ
ラム変換をサポートできるようにすることを目指している．従来のタグレスファイナル法に則りつつもTDB を中間表現として用い，全体として型安全性を保持しつつ変換を記述できるライブラリを実装した．
このフレームワークにより、HOAS では困難であったいくつかの操作を平易に実装できることを示した．

[1] Asai, K.: Extracting a Call-by-Name Partial
Evaluator from a Proof of Termination, Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM
2019, New York, NY, USA, Association for Computing Machinery, 2019, pp. 6167.
[2] Atkey, R., Lindley, S., and Yallop, J.: Unembedding domain-specific languages, Proceedings ofthe 2nd ACM SIGPLAN symposium on Haskell,
Haskell ’09, ACM, 2009, pp. 37–48.
[3] Carette, J., Kiselyov, O., and Shan, C.: Finally
Tagless, Partially Evaluated: Tagless Staged Interpreters for Simpler Typed Languages, J. Funct.
Program., Vol. 19, No. 5(2009), pp. 509–543.
[4] Kiselyov, O.: λto SKI, Semantically, Functionaland Logic Programming, Gallagher, J. P. and Sulzmann, M.(eds.), Cham, Springer International Publishing, 2018, pp. 33–50.
[5] Kiselyov, O: Embedding and optimizing domainspecific languages in the typed final style,
http://cufp.org/2015/t4-oleg-kiselyov-dsl-in-typed.html.
[6] Kokke, W., Siek, J. G., and Wadler, P.: Programming language foundations in Agda, Science of Computer Programming, Vol. 194(2020),
pp. 102440.
[7] Srensen, M. H., Glck, R., and Jones, N. D.: A
positive supercompiler, Journal of Functional Programming, Vol. 6, No. 6(1996), pp. 811838.
[8] Suzuki, K., Kiselyov, O., and Kameyama, Y.:Finally, Safely-extensible and Eﬃcient Languageintegrated Query, Proceedings of the 2016 ACM
SIGPLAN Workshop on Partial Evaluation and
Program Manipulation, PEPM ’16, New York, NY,

USA, ACM, 2016, pp. 37–48.
[9] Turchin, V. F.: The Concept of a Supercompiler, ACM Trans. Program. Lang. Syst., Vol. 8,
No. 3(1986), pp. 292325.