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

SML#の動的型付け機構
大堀 淳

上野 雄大

静的型システムを持つ言語における動的型付け（dynamic typing）は、Abadi 等によってその型理論が提案されているが、そこで提案されている操作的意味論理論には、コンパイルと実行のフェーズを超えた機能が暗黙に使われており、ネイティブコードコンパイラへ直接適用するのは困難である。特に、型推論に基づく多相型言語において、この問題は顕著である。我々は、我々が開発を進める ML 系高階関数型言語 SML#の基盤技術のひとつである型主導コンパイル方式を基礎に、動的型付け機構の系統的な実現方法を開発し、SML#に実装した。本発表では、方式とSML#への実装の概要を報告する。

付けられた言語（型が静的に決定されないデータを扱1 はじめにう言語）では、この機能が言語の基本機能として組み動的型付け（dynamic typing）とは、実行時に値込まれており、例えば Lisp では stringp などの型述の型を分析し、型に応じた処理を行う機構である。こ語で調べることができる。この機能から理解される通の動的型付けは、静的型システムを持たない言語でり、動的に型付けられた言語における実行時の値は、は、基本的なプログラム機能のひとつであるが、静的型の表現と型に応じた値とを持った一様なデータとみに型付けられた言語でも、外部データの操作などの際ることができる。Abadi 等の文献では、この型情報に必要となる機能である。Abadi 等 [1] によって型シを伴う値の一様な表現を、dynamic 型と呼んでいる。

ステムの機能として提案され以来、静的型システムを動的に型付けされた言語では、このような型情報を含持つ言語における有用性が広く認識され、多相型言語

む値の表現とその分析機能は、プログラミングの基における実装も報告されている [4] [2]。しかしながら、本である。Abadi 等の提案は、この動的に型付けら

現時点では、ML 系多相型言語の機能として確立されれた言語の値の表現である dynamic 型を、静的型シているとは言えず、実用的なコンパイラにおいても十ステムに導入し、動的型付け機能をプログラムに与分にサポートされているとは言えない。この現状は、えることを目指したシステムである。これによって、単に実装の努力がなされていない、とのことではな

データ永続性 [3] などの外部データの型安全な操作がく、型付き多相型プログラミング言語コンパイラにお可能となると期待される。

ける動的型付け機能の実現には、従来の研究成果を超える新たな理論や技術課題の克服を必要とすること

静的型システムの枠組みでの動的型付けの基本は、以下の形の型規則の導入である。

を反映している。
動的型付けの基本は、実行時にプログラムによって(dyn intro)作られる値に対して、その値の型情報をプログラムから利用可能にすることである。Lisp などの動的に型
Atsushi Ohori, Katsuhiro Ueno, 東 北 大 学, Tohoku
University.

(dyn elim)Γ⊢e : τΓ ⊢ dynamic(e : τ ) : dynamicΓ ⊢ e : dynamicΓ ⊢ e as τ : τ式 dynamic(e : τ ) の効果の直感的な理解は、e の値を型 τ の表現と組にし、動的言語の値の表現と同等の術の詳細、さらにそれらと従来の研究との詳細の比較型情報をもった値の生成である。このような機能は、は別の機会に発表する予定である。

プログラムの実行が型チェック機能を含むインタープリタで行われるような言語システムでは、比較的容2 静的言語での動的型付け実現上の課題易に実現できる。しかしながら、静的多相型言語のコ

前節で触れた通り、プログラムの実行時に、コンパンパイラでの実現方式が確立しているとは言えない。

イラが内部で管理する型情報、型推論情報、シンボル困難さの一旦を理解するために、Standard ML の構の束縛情報などを自由に利用できるインタープリタ

文で書かれた以下の仮想的な多相関数宣言を考えて形式の言語処理系では、動的な言語同様、動的な型付みよう。

け機能を実現する上での本質的な困難は伴わないとfun (’a) toDyn x = dynamic (x:’a): ’a -> dynamicfun (’a) toValue x = (x as ’a): dynamic -> ’a

考える。静的言語での動的型付け実現上の課題は、コンパイラとは独立に実行するコードを生成しなければならないコンパイラにとっての課題である。
静的に型付けられた言語のコンパイラが動的な型

ここで、(’a) は、この関数で束縛されるべき多相型付けを実現する上での主な技術的課題には、以下のも変数の宣言である。これら関数の意味を考えるなら、のが含まれる。

コンパイルされたコードは、任意の型 τ に対して、τ

• 動的型付け機構の多相的な利用の表現を生成する能力および任意の型 τ の値の実行

多相型言語において動的型付け機能を十分に利時表現をヒープ上に生成する能力を持たねばならない

用するためには、前節で例にあげた toDyn 関数が、従来のコンパイル技術に基づく多相型言語コンパのような多相的な関数の中での使用が重要であイラには、そのようなコードを生成する能力はない。

る。多相型言語のネイティブコードコンパイラ

我々は、この問題に取り組み、種々の新たな概念とは、多相関数も、もちろんネイティブコードにコ技術を開発し、型付き多相型プログラミング言語にンパイルする。従って、動的型付け機能を使用すおける動的型付けの実現方式を確立し、ほぼ完全なる多相関数をコンパイルするには、任意の型を取動的型付け機構を SML#コンパイラ [7] に実装するこりうる多相的な動的型付け機構をコードで実現とに成功した。図 1 に実際の対話型セッションの簡する必要がある。このことは、コンパイルされた単な例を示す。型変数’a の#reify は型の reify 機能

コードが、将来の型適用時にインスタンス化されを使うとの注釈であり、型変数の取りうる型には制る型の実行時型表現を生成・分析する必要がある

約はない。Dynamic は動的型付けを実現するシステことを意味する。

ムモジュール、Dynamic.dyn は動的に型付けられた• 静的型情報の reify

値の型、Dynamic.dyn の型パラメタは、部分的に検静的な型情報は、コンパイラがコンパイル時に構証された静的な型情報を表す。静的型情報が不明の築し利用するメタな情報である。これらをプログ

Dynamic.void Dynamic.dyn が従来の dynamic 型にラムから利用するためには、それらメタ情報のオ相当する型である。この例から理解される通り、上記ブジェクト化、すなわち、自己反映計算におけるの 2 つの関数が多相関数として定義され、ユーザ定reify 処理が必要である。

義の再帰的なデータ型を含む任意の型の動的型付けが実現されている。

• 動的型（dynamic 型）からの値の構築
dynamic 型をプログラムが e as τ などの構文

本発表では、ML 系の多相型言語での動的型付け実を通じて利用するためには、その実際の型に応じ現上の技術的課題とその解決戦略の概要を述べ、それた内部表現を持つ値を構築する必要がある。このら課題を達成して実現した SML#の動的型付けの実データの型に応じた実行時表現の構築は、コンパ装を紹介する。技術的課題とその実現方式及び実装技イラが行う処理である。この処理は、種々の最適$ smlsharp
SML# 3.4.1-... (2019-07-27 10:34:04 JST ...) for x86_64-pc-linux-gnu with LLVM 6.0.0# val toDyn = Dynamic.dynamic;
val toDyn = fn : [’a#reify. ’a -> Dynamic.void Dynamic.dyn]# fun (’a#reify) toValue x = _dynamic x as ’a;val toValue = fn : [’a,’b#reify. ’a Dynamic.dyn -> ’b]# datatype foo = A of int | B of real * foo;
# val x = Dynamic.dynamic (B (1.1, B (2.2, A 3)));val x = _ : Dynamic.void Dynamic.dyn# val y = toValue x : foo;
val y = B (1.1, B (2.2, A 3)) : foo
図1

SML#の動的型付けの例

化を含む複雑な処理である。dynamic 型からのな枠組みとその実装技術の詳細は、他の論文に譲り、値の構築を実現するためには、コンパイルされた

本発表では、課題実現戦略と実装の概要を報告する。

コードが、データレイアウトの決定や最適化を含むコンパイラの処理を利用可能である必要が3. 1 多相的な動的型付け機能の実現ある。

多相型言語における動的型付けの最大の課題は、環• ユーザ定義のデータ型の扱い境で束縛された型変数を含む型を持つ変数に対するML の datatype 宣言で定義される一般に相互再動的型の導入を許す体系の構築である。この機能なし

帰的なユーザ定義のデータ型は、データ構造とみには、動的型付け機能を用いるプログラムは多相型をれば、大きさに上限の無い循環的な構造である。

持つことができず、多相型言語の利点を十分に活用でもちろん、これらデータ構造は、コンパイラの型きないことになる。

チェック・型推論モジュールが表現し操作しているデータ構造であり、表現や操作方法自体に本質困難を理解するための典型的な例は、冒頭で挙げた
多相関数的で未解明の課題はない。しかし、型付き言語コfun (’a) toDyn (x:’a) = dynamic (x)ンパイラの型チェック・型推論モジュールは、コである。多相型ラムダ計算の標準的な文法では、ンパイラコードの中でも有数の大きさを占める

Λt.λx : t.dynamic(x : t)

コードである。型の reify や型からの値の再構築と表現される。この関数をコンパイルした結果のコーを行うコードは、これら処理と同等の処理を実行

ドは、束縛型変数 t に対して将来与えられる可能なイ時に行うことを要求するものであり、その系統的ンスタンス型 τ すべてに対応する動的値 (v, τ ) を作

な実装は技術的な課題と言える。

る能力が要求される。注意深い読者はすでに理解されていることと思うが、この問題の本質は、引数の型に

3 課題解決戦略と SML#での実装概要

応じて振る舞いが異なる多相関数をネイティブコード

我々は、前節で議論したものを含む、多相型言語コにコンパイルする問題と共通であり、その系統的な一ンパイラが動的型付け機構を実現する型理論的な枠組

つの解決方法は、レコード多相性のコンパイルの過程みとその実装技術の構築に成功し、それらを実装したで提案された型主導コンパイル方式である。

SML#コンパイラをすでに実現している。型理論的

型主導コンパイル方式 [5] [6] では、型抽象時に、抽象の対象となる式に含まれる型依存の処理を表現する

ラが知っているライブラリ関数を、ユーザコードからカインド（型の型）を導入し、型変数を束縛する際に呼び出すコードの生成である。これは、コンパイラをカインド注釈を付加し、そのカインドによって決まる構成する変数の静的環境を、ユーザコードのコンパイ実行時に必要となる属性を受け取るラムダ抽象を導ル環境に追加し、さらに、ユーザレベルでのコンパイ入する。さらに、そのように変換された型抽象式が型ラの関数呼び出しを行う式を生成するコンパイルレ

適用される時、コンパイラは適用されるインスタンスベルの式を導入することによって解決できる。

型から、必要となる属性情報を表現する式を生成し、適用する。この考え方を適用し、上記のラムダ式を、

3. 3 SML#の動的型付け拡張

以下のような形の式にコンパイルすることによって、我々は、これら型理論的な枠組みの構築およびそれこの問題は解決される。

らに基づくコンパイラへの実装を行い、動的型付け

Λt#reify.λT : reifiedTy(t).λx : t.dynamic(x, T ))機構を装備した SML#コンパイラの開発に成功した。

ここで、reifiedTy(t) は型 t の型表現を唯一の値とし

図 2 に、SML#の動的型付けを実現するシステムモてもつ単元型（singleton type)、dynamic(x, T) は、ジュールである Dynamic ストラクチャの一部と、動インスタンス型 τ を持つ値 x と τ の型表現 T を受け的型付け機能のための特殊構文の概要を示す。

取って処理を行う関数である。

実現された動的型付けは、永続性の実現、型依存のSML#コンパイラには、モジュラーな型主導コンパ演算、汎用の値のプリンター、JSON 等の外部データイルフェーズが組み込まれている。この型主導コンパの取り込みや書き出し等多くの実世的な機能の基盤とイルフェーズに、上記の機能を実現するモジュールをなる技術である。Dynamic ストラクチャに定義され組み込むことで、この方式を実装することができる。

た、[’a#reify.’a -> unit] 型を持つ Dynamoc.pp
関数は、汎用のプリティプリンタである。特殊構文で3. 2 型の reify と動的型の値の構築はなく、通常の高階関数であるため、この関数を呼び問題点であげた、型の reify、動的型からの値の構出すだけで、任意の型の値をプリントすることができ築、ユーザ定義のデータ型の扱いの３つ課題の本質る。例えば foldl 関数の引数をトレースしたければ、は、いずれも、再帰的な型の表現、型の実行時表現、以下のように foldl の冒頭で Dynamic.pp 関数を引最適化処理、などのコンパイラの複雑な機能を、コン数に対して呼び出すだけで良い。

パイルされたユーザコードから呼び出すための系統# fun foldl f z l =的機構の開発といえる。そのような機構があれば、適(Dynamic.pp {l=l,z=z};

宜コンパイル機能の呼び出しを行うようにコンパイ

case l ofルすることによって解決できる。このコンパイラ機能

nil => zの呼び出し方式の開発は、コンパイラとユーザコードの関連に依存し、本質的に処理系依存の問題である。

SML#コンパイラは、それ自身 SML#で書かれて| h::t => foldl f (f (h,z)) t);
val foldl = fn
: [’a#reify, ’b#reify.

おり、コンパイラの種々の機能は、SML#のモジュー(’a * ’b -> ’b) -> ’b -> ’a list -> ’b]

ルとして実現されている。さらに、それらモジュール

ここで {l=l,z=z} は、Standard ML のレコード式では、分割コンパイルされ、リンクされてコンパイラがある。以下の例が示すように、この関数は、適用され作られている。この構造は、ユーザコードの構造とる値の型に応じた適切なプリントを行う。

同じである。従って、ユーザコードからのコンパイラ# foldl (fn (h,z) => h + z) 0 [1,2];

コードの呼び出しが、コンパイラが使用するモジュー{l = [1, 2], z = 0}

ル単位であるなら、リンクや実行時の呼び出しに関す{l = [2], z = 1}

る本質的な問題は存在しない。残る課題は、コンパイ{l = [], z = 3}

動的型付けを実現する Dynamic ストラクチャの一部

structure Dynamic =structtype ’a dyn<hidden>type dynamic = void dyndatatype ty =datatype term =exception RuntimeTypeError = PartialDynamic.RuntimeTypeErrorval dynamic = fn : [’a#reify. ’a -> void dyn]val dynamicToString = fn : void dyn -> stringval dynamicToTerm = fn : void dyn -> term
val dynamicToTy = fn : void dyn -> ty
val format = fn : [’a#reify. ’a -> string]
val fromJson = fn : string -> void dyn
val join = fn : void dyn * void dyn -> void dyn
val pp = fn : [’a#reify. ’a -> unit]
val toJson = fn : [’a. ’a dyn -> string]val valueToJson = fn : [’a#reify. ’a -> string]val view = fn : [’a#reify. ’a dyn -> ’a]...
end
動的型付けを操作する特殊構文• dynamic exp as τ

動的型の値への変換•

型の混在を許すパターンマッチング

dynamiccase exp of ruleList

図2

SML#の動的型付け拡張

val it = 3 : int

値として取り込むことができる。Dynamic.fromJSON# foldl (fn (h,z) => h ^ z) "" ["a","b"];関数はそのようにして実現されている。

{l = ["a", "b"], z = ""}{l = ["b"], z = "a"}今後リリース予定のコンパイラ SML# 3.5 版では、この動的型付け機構が提供される予定である。

{l = [], z = "ba"}val it = "ba" : string

4 まとめ

現在の SML#の対話型環境を実現する値のプリンタ

本発表では、静的に型付けされた多相型言語で動的はこの動的型付け機能を用いて実現されている。

型付けを実現する上での技術的課題を論じ、その解決

プリティプリンタに限らず、従来困難であった種々の戦略と、その戦略に基づき実現した SML#の動的型機能が、この動的型付け機構を用いて実現可能である。

付け機能の概要を紹介した。SML#では、一般化さたとえば、SML#の C 言語との直接連携機能と組み合れた自然結合や対話型システムのプリンター始め多

わせれば、C 言語で書かれた JSON パーザ Yajil を直くの機能が、動的型付け機構を用いて実現している。

接呼び出し、結果を動的型付け機構を用いて、ML の今後、動的型付けの機能の拡張やその応用技術の研究を進め、より柔軟で実用的な SML#処理系の開発を進めていく予定である。

参 考 文 献[1] M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin.
Dynamic typing in a statically-typed language.
ACM Transcations on Programming Languages andSystems, 13(2):237–268, 1991.
[2] M. Abadi, L. Cardelli, B. Pierce, and D. Rémy.
Dynamic typing in polymorphic languages. In ACM
SIGPLAN Workshop on ML and its Applications,1992.
[3] M.P. Atkinson and O.P. Buneman. Types andpersistence in database programming languages.
ACM Computing Surveys, June 1987.
[4] X. Leroy and M. Mauny. Dynamics in ml. In Proceedings of the ACM Conference on Functional Programming Languages and Computer Architecture,
1991.
[5] A Ohori. A compilation method for ML-stylepolymorphic record calculi. In Proc. ACM POPL
Symposium, pages 154–165, 1992.
[6] A. Ohori. A polymorphic record calculus and its
compilation. ACM Trans. Prog. Lang. and Syst.,
17(6):844–895, 1995.
[7] SML#. http://www.riec.tohoku.ac.jp/smlsharp/,2006–2019.