\section{型プロファイラの設計} \label{section:3}

このsectionでは，

まず本論文の取り組みとして型プロファイリングによる解析手法を採用する理由を

subsection~\ref{subsection:prev-reseaches}の先行研究を踏まえて説明する．

次に，Juliaの型推論システムについて，そのアルゴリズムや収束性などに関する基本的な性質を説明する．

というのは，本論文で提案する型プロファイラの設計方針や性質は，

結局その抽象解釈のメインルーチンとなるJuliaの型推論システムにより決まるからである．

そして最後に型プロファイラの実装であるTypeProfiler.jlの設計とその性質を説明する．

\subsection{Why "type profiler" ?}

Juliaプログラムに対する静的な型エラー解析の手法として，

本論文で抽象解釈による型プロファイリングを採用した理由は次の3点である．

\begin{enumerate}

\item Juliaの言語機能として実装されている型推論システムをそのまま利用することができる．\\

Juliaの型推論は実用上のJITコンパイルに耐え得る正確性とスケーラビリティをすでに備えており，

また今後も発展していくことが期待される．

この型推論システムを利用することで，

抽象解釈を用いた型プロファイリング（\ref{subsubsection:type-profiling}）において

問題となりやすいスケーラビリティを保ちつつ，型プロファイラを比較的容易に実装できる．

　\item Julia言語のプログラミングパターンと，追加的な型アノテーションによる検査方式

（\ref{subsubsection:type-check-with-annotation}）

との相性が良くないと思われる．

% REVIEW: これいる？

\item 型プロファイラは，素のJuliaプログラムに対して解析を行うことができるため，

気軽に導入を試すことができる．

そのためまだ静的な型エラー解析が広く行われていない現行のエコシステムにおいても受け入れやすいと思われる．

将来的なJuliaプログラムに対する静的な型エラー解析の必要性を考える上での，足がかりと捉えることもできる．

\end{enumerate}

2点目に関して，本論文執筆時点ではまだ理解が未整理であるが，ここでは現状における理解を説明しておく．

先述したように，ソースプログラムに対する型アノテーションは既にJuliaの言語機能として存在し，

型アノテーションの導入自体は自然に行うことができる．

一方で，Juliaプログラムにおいて型アノテーションは

generic functionのdispatchをコントロールする上で非常に重要な意味を持っている．

つまり，code selectionのメカニズムにおいて型アノテーションはJuliaプログラムの多相性を大きく左右し\footnotemark

，プログラムの意味論に根本的な影響を与える．

そのため，intra-proceduralな解析が可能な程度に引数型を限定できるような形で

追加的な型アノテーションを与える場合，

Juliaプログラムが本来持ちうる多相性を保つのは難しく，

Juliaの言語機能を大きく損なってしまう可能性が高い．

\footnotetext{

型アノテーションを付けないことは，\texttt{Any}型のアノテーションを施すことと同義である．

関数の引数に型アノテーションを施さないことは最もgenericな場合に対応するメソッドを定義する

ことを意味し，引数に型アノテーションを施すことは一般にそのメソッドの多相性を低下させる．

このことから，プログラマは型アノテーションによりJuliaプログラムの多相性を調整していると

考えることもできる．

}

\subsection{Juliaの型推論システム} \label{subsection:julia-type-inference}

Juliaの実行過程においては，generic functionの呼び出し時，

与えられた引数達がdispatchされるメソッドのcode specializationがまだ行われていない場合

（つまり，そのメソッドの，その引数型組に対する最適化のキャッシュがまだ存在しない場合），

型推論が行われ，その結果に基づいて最適化が行われる

（\hyperref[subsubsection:eval-process]{Juliaの実行プロセス}参照）．

Juliaのプログラムの式や変数の型は，プログラムを型レベルで抽象解釈することで推論される．

Juliaの型推論に用いられている解析手法は元々，

\cite{abstract-interpretation, scheme-for-automatic-inference}で提唱されたものであり，

Bezansonらによる論文~\cite{jeff-phd, jeff-master, julia-2012}ではこの手法のことを指して，

\textbf{data-flow analysis}という用語を用いており，以降本論文においても使用する．

Juliaの型推論は，MLなどの静的型付け言語における型推論とは根本的に異なる．

静的型付け言語においては通常，

unificationベースの型推論\cite{milner}が用いられ，

コンパイル時におけるプログラムの正しさの証明の一環として

ソースレベルの型システムからでは自明に得られないプログラムの性質を発見するために推論が行われる．

一方Juliaの型推論は，もとよりcode specializationによるパフォーマンス向上を目的として，

プログラムの性質を「できる限りの範囲で詳細に\cite{jeff-phd}」調べるために行われる．

data-flow analysisは以下のような性質を持つ．

\begin{enumerate}

\item 推論が柔軟である．

例えば，

変数は（明示的なキャストをせずとも）プログラムの各時点において異なる型を持つことができ，

また推論により型は必ずしも決定されなくてもよいなど，

より動的型付けに即した性質を備えている．

\item 型システムが表現可能な型の数が有限でない場合においても，

\textbf{widening}と呼ばれる手法を用いることでアルゴリズムの収束性を保つことができる．

また，ヒューリスティックを用いて推論中の型をナイーブな実装よりも早くより抽象的な型へ遷移させることで，

推論の収束を早めることができる．

\item 型推論の実装と言語仕様とを切り離すことが可能である．

% REVIEW: Juliaの型推論ルーチンを明示的に呼び出すようなコードの場合もこれで合ってる？

例えばJuliaにおいては，推論のcorrectnessを保つ限り，

型推論の結果によってJuliaプログラムの意味論が変わることはなく，

ただそのパフォーマンスが変わるだけである.

このことはつまり，

型推論のルーチンを改善しようとするときに言語仕様の変更を気にする必要がないことを意味し，

結果としてコンパイラの開発スピードを早めることができる．

\end{enumerate}

以下では，まずこのJuliaの型推論システムの基本的なアルゴリズムを説明する．

その次にwideningを導入することによりこのアルゴリズムの収束性が与えられることを説明し，

最後にJuliaの型推論ルーチンの推論結果のcorrectnessについて言及する．

\subsubsection{アルゴリズム} \label{subsubsection:inference-algorithm}

\hyperref[subsubsection:eval-process]{Juliaの実行プロセス}で述べたように，

型推論はある引数型組に対するメソッドのcode generationがまだ行われていないときに引き起こされ，

Juliaプログラムを

\textbf{SSA形式（Static Single Assignment Form）}\cite{julia-ssa}

に変換したlowered formに対して行われる．

このSSA形式はsurface ASTとは異なり，木構造のデータ構造ではなく，

関数呼び出しや条件分岐など「ある1つのことを行う」\textbf{statement}の連なりである．

SSA形式においては，各変数は使用される前に必ず定義され，また一度しか代入されない\footnote{

ここで，SSA形式中の「変数」は元のプログラム中の変数と必ずしも一対一に対応しない．

例えば，元のプログラム中における変数の再代入は，SSA形式においては新たな変数への代入として変換される．

}上，control flowはネストせず，分岐先と対応する

\href{https://en.wikipedia.org/wiki/Basic_block}{basic block}

へのgotoとして表現される．

こうした性質からSSA形式は，

constant propagation（定数伝播）やdead code elimination（デッドコード削除）等

といった最適化を行うための分析に適している．

以下，単に"statement"という場合，このSSA形式のプログラム表現におけるstatementを意味する．

Juliaの型推論は，\cite{graph-free-data-flow-analysis}で提案されたgraph freeな最大不動点計算の

フレームワークを相互再帰関数も扱えるように拡張したアルゴリズムにより実装されている．

ベースとなるアイディアは，

プログラムを型レベルで（単方向に）仮想実行する（foward data-flow analysis）というものである．

型レベルでの仮想実行は，それぞれのstatementの副作用を決定し，

その型情報を，そのstatementからcontrol flowにより到達可能な全てのstatementに伝播させ，

プログラムの各時点おける状態をトレースすることで行われる．

以下にその基本的なアルゴリズムを説明する\cite{jameson, julia-2012}．

Juliaの型推論は，

1つの関数呼び出し内におけるプロセス（local type inference）と，

複数の関数呼び出しにまたがって行われるプロセス（inter-procedural type inference）

の2つに分けて説明することができる

\footnote{

正確には，この2つとは別に，comprehension（内包表記）に対する推論のサブルーチンが

ある種のspecial caseとして存在する\cite{jameson}．

comprehension式の型は，comprehension式に対する操作を全て考慮した上で推論される必要があり，

この手続きは単純な単方向解析（forward data-flow analysis）では可能でないためspecial caseされる．

}．

\paragraph{local type inference}

\(W\)を次に推論されるべきstatementの集合とする． % REVIEW: 元の説明通りprogram counterとするべき？

まず，推論が始まる前に，推論されるメソッド内の状態を次のように初期化する．

\begin{itemize}

\item メソッドのエントリポイントとなるstatementを\(W\)に追加する．

\item メソッドの引数それぞれの型は推論時に与えられている型をそのままセットする．

\item 全てのローカル変数の型とメソッドの返り値型を\textbf{\texttt{Bottom}}型\footnotemark にセットする．

\end{itemize}

\footnotetext{

\texttt{Bottom}型は，Juliaのtype latticeの最も底に位置する型であり，

Juliaの型システムにおけるその他すべての型のsubtypeとして機能する．

\texttt{Bottom}型と任意の型\(T\)をmergeして得られるunion型は常に\(T\)となるため，

型推論において\texttt{Bottom}型は

まだ初期化されていない変数の型やまだリターンされていないメソッドの返り値型として用いられる．

また，\texttt{Bottom}は型推論アルゴリズムがエラーの発生を検出した場合にも導入される．

Juliaのプログラムにおいては，\texttt{Union\{\}}型が\texttt{Bottom}型のエイリアスとして

用いられる．

}

その後，以下のプロセスを\(W\)が空になるまで繰り返す．

\begin{enumerate}

\item \(W\)に残っているstatementを1つ取り出す（以下このstatementを"currrent statement"と呼ぶ）．

\item current statementの副作用を決定する．

例えば代入は変数の型を変化させる．

もしcurrent statementが関数呼び出しである場合，

推論を再帰的に行い，その関数の返り値型を決定する（このサブルーチンについては後述する）．

\item current statementから到達可能な\textbf{全ての}statement

（以下そのそれぞれを"next statement"と呼ぶ）

を\(W\)に追加し，そのそれぞれに対しcurrent statementの型情報を伝播させる．

このプロセスは2つのstatementの変数の型を\textbf{merge}させることで行われる．

無限ループを避けるため，

current statementとのtype mergeによりnext statementに含まれるいずれかの変数の型が変化する場合にのみ，

next statementは\(W\)に追加される．

このtype mergeにおいて，アルゴリズムの収束を保証するため，

widening（\ref{subsubsection:inference-convergence-and-heuristic}）

と呼ばれる手法が用いられる．

\end{enumerate}

current statementが関数呼び出しである場合，以下のサブルーチンにより関数呼び出しの返り値型が推論される．

\begin{itemize}

\item generic functionの呼び出しである場合，

まず推論されている引数組型とマッチするメソッドを求める．マッチするメソッドは，

引数組型と，そのgeneric functionが持つメソッドそれぞれのシグネチャ型を

\textbf{meet}させ得られるintersection型

（greatest lower bound，または交差型）\footnotemark

が\texttt{Bottom}型とはならないものとして求まる．

マッチしたメソッドのそれぞれに対して同様の型推論を行い，

推論結果として得られるそれらの返り値型達をmergeして求まる型を

そのgeneric functionの返り値型とする．

\item 呼び出される関数がgeneric functionでない場合，それはbuiltin functionの呼び出しである．

builtin functionの数は限られており，その返り値型はhard codeされた型遷移関数により計算される．

\end{itemize}

\(T\)をこのサブルーチンの型遷移関数とし，

\(f\)をgeneric function，

\(t_{arg}\)を推論された引数組型，\(s\)と\(g\)をそれぞれ\(f\)のメソッドの引数の型シグネチャと実装本体とすると，

generic functionの呼び出しに対するサブルーチンは以下の式で表される．

ここで，\(\sqcup\)，\(\sqcap\)はそれぞれtype mergeとtype meetに対応する演算である．

\footnotetext{

このintersection型を求めるmeetを厳密に実装することは難しい\cite{jeff-phd}．

Juliaは現在のところ，intersectionが過大に評価されることを許す

（真のintersectionよりも広い範囲の型を返す）形でmeetを実装しているが，

それでも型推論の収束性とcorrectnessは保たれる．

なぜならば，type meetは型推論においてメソッドのマッチングにのみ用いられているため，

intersectionが過大に評価されたとしても，マッチするメソッドの数が増え推論の結果が粗くなるだけで，

推論の単調性と有限性（\ref{subsubsection:inference-convergence-and-heuristic}は失われないからである．

}

\paragraph{inter-procedural type inference}

さらに，再帰関数の呼び出しに対応するため，

以上のプロセスをgeneric functionの呼び出しにまたがってinter-proceduralに管理する，

次のような手続きを考える必要がある．

推論の過程において，呼び出しが生じたgeneric functionとその引数型組の組み合わせを保持しておく．

同一の組み合わせの呼び出しが生じた場合，

それらの呼び出し間で生じる全ての関数呼び出しを相互再帰関数呼び出しとして記録し，

それらの返り値型がまだ完全に推論されていないことを示す\textit{incomplete}タグを付与する．

\textit{incomplete}タグが付与されている全ての関数の返り値型がfix-pointに至るまで，

この相互再帰関数呼び出しのサイクルに対して推論のプロセスを繰り返す\footnote{

このinter-procedural type inferenceの実装は，

特に複数の相互再帰呼び出しのサイクルが同一の推論プロセス中に存在する場合などで，

型推論のパフォーマンスに大きな影響を与える．

Juliaの型推論アルゴリズムにおいてそれが実際どのように実装され，技術的な課題点がいかに克服されているかについては

\cite{jameson, jameson-revisited}が詳しいが，ここでは詳細な説明は避ける．

}．

\subsubsection{収束性とヒューリスティック} \label{subsubsection:inference-convergence-and-heuristic}

このsubsubsectionでは，Juliaの型推論アルゴリズムの収束性がいかに保たれているか，

そしてその収束を早める各種のヒューリスティックについて説明する．

\paragraph{収束性} \label{paragraph:inference-convergence}

上記のアルゴリズムを使用したdata-flow analysisは以下の性質を満たす場合に，

必ず収束することが保証される\cite{graph-free-data-flow-analysis, jameson}．

\begin{description}

\item [単調性（monotonicity）]

2つの型をmergeしたときに必ずより抽象的な型にならなければならない．

また，data-flow analysisにおける関数呼び出しは単調でなければならない．

つまり関数呼び出しの引数型が抽象的であるほど，推論される返り値型も抽象的にならなければならない．

\item [有限性（finiteness）] 型システムにおいて作られ得る型が有限である．

\end{description}

まず，単調性については，

上述したbuiltin functionの型遷移関数を正確に実装することで満たすことができる．

また，型\(S\)と型\(T\)をmergeして得られる\verb|Union|型\(U\)\footnotemark はJuliaの型システムにおいて\(S\)と\(T\)よりも常に抽象的である．

\footnotetext{

また，\(S\)か\(T\)がもう一方のsubtypeである場合，\(U\)を単により抽象的な方の型とし，

\texttt{Union}型を作らない単純化も行われる．

}

有限性に関して，

Juliaの型システムは\verb|Union|型や\verb|Tuple|型，そしてコンテナ型の存在により，

無限の型が作られ得るため，そのままではこの条件を満たさない．

そこで，\textbf{widening}と呼ばれる手法を用いて

型推論時に作られ得る型の数が有限となるように強制する

\footnote{

言い換えると，wideningを使用することにより，

高さが有限でない元のtype latticeを型推論時においては高さが有限となるように強制している．

}．

以下，\verb|Tuple|と\verb|Union|型のパラメータの数を「長さ」と呼び，

コンテナ型のパラメータがネストしている深さを単に「深さ」と呼ぶ\footnote{

これをJuliaプログラムで表現すると以下のようになる．

\begin{itemize}

\item \mintinline{julia}{length(type) = length(type.parameters)}

\item \mintinline{julia}{depth(type) = isempty(type.parameters) ? 1 : 1 + maximum(depth, type.parameters)}

\end{itemize}

}．

wideningは次の3つの場合で使用される．

\begin{itemize}

\item generic functionの呼び出しの引数型が，推論の再帰呼び出しごとに長く，あるいは深くなる場合\footnotemark．

\item ある型のfieldの型を計算するとき．

fieldの型は任意の型を作り得るため，そのままでは無限ループが生じる可能性がある．

\item type mergeが起こる場合．type mergeは次の場合に生じる．

% REVIEW: もっとあるかも

\begin{itemize}

\item current statementからnext statementに型情報を伝播させるとき．

これには変数やメソッドの返り値の型の更新も含まれる．

\item 分岐していたcontrol flowを合流させるとき．

\item generic functionの呼び出しにおいてマッチしたメソッドが複数あり，

それらの返り値の推論結果のunion型を求め，

そのgeneric functionの返り値型の推論値とするとき．

\end{itemize}

\end{itemize}

\footnotetext{

このパターンは，例えば以下の関数に対する推論で生じる．

\begin{itemize}

\item \mintinline{julia}{longer(args...) = longer(sum(args), args...)}

\item \mintinline{julia}{deeper(type) = deeper(Type{type})}

\end{itemize}

これらの関数呼び出しは実行時必ずしも終了しないが，型推論はそうしたプログラムに対しても停止する．

}

wideningはそれぞれの型に応じて以下のように行われる．

\begin{description}

\item [\texttt{Union}型の長さ]

\texttt{Union}型の長さが大きくなった場合，いくつかの要素型をそれらの共通抽象型にまとめる\footnote{

e.g.: \texttt{Union\{Int, Float16, Float32, Float64\} -> Union\{Int, AbstractFloat\}}

}．

\item [\texttt{Tuple}型の長さ]

\texttt{Tuple}型の長さが大きくなった場合，末尾の型達を可変長型としてまとめる\footnote{

e.g.: \texttt{Tuple\{Int,Int,Int,Int\} -> Tuple\{Int,Vararg\{Int\}\}}

}．

\item [コンテナ型の深さ]

コンテナ型のパラメータ型がネストし深さが大きくなった場合，

置き換えられることになる型達を包含する型変数を持つ\texttt{UnionAll}型を導入する\footnote{

e.g.: \texttt{Type\{Type\{Type\{Type\{Int\}\}\}\} -> Type\{Type\{T where T<:Type\}\}}\\

ここで\texttt{T where T<:Type}は\texttt{UnionAll}型である．

その型変数\texttt{T<:Type}は置き換えられた型\texttt{Type\{Type\{Int\}\}}を包含する．

}．

\end{description}

以上に説明したwideningによりJuliaの型推論の収束性が保証され，つまりJITの停止性が保証される．

\paragraph{ヒューリスティック} \label{paragraph:inference-heuristic}

また，Juliaの型推論においては，様々なヒューリスティックを用いることで，

推論中の型をより早く抽象的な型に遷移させ，型推論の収束を早めている．

wideningが行われる長さや深さの閾値も，ヒューリスティックにより決まると言える．

それらのヒューリスティックのうちのいくつかの具体的な内容については，

paragraph~\ref{paragraph:type-profiler-heuristic}で説明する．

\subsubsection{correctness} \label{subsubsection:inference-correctness}

\cite{graph-free-data-flow-analysis}のアルゴリズムを用いたdata-flow analysisに対しては，

次の性質が成り立つ\cite{jeff-master}．

\begin{theorem*}[correctness]

\label{theorem:inference-correctness}

% > Dynamic type inference schemes obey a correctness property that inferred types must subsume all possible run-time types.

プログラム中のある式\(Expr\)に対して推論された型\(T_{infer}\)は，

\(Expr\)が実行時において取りうるあらゆる型\(T_{runtime}\)を全て含んでいる．

\[

\end{theorem*}

この性質から，

ある式がconcreteな型\(T\)を取ると推論された場合，その式の型は実行時においても必ず\(T\)となり\footnote{

% TODO: more valid way to say this

Juliaの型システムにおいてconcrete typeは（\texttt{Bottom}型以外には）subtypeを持たない．

つまり，concrete typeが含む型はそれ自身のみである．

}，

コンパイラは実行時の型アサーションなしに\(T\)型に対して最適化されたルーチンを呼ぶコードを生成することができる．

\subsection{TypeProfiler.jlの設計と性質} \label{subsection:type-profiler-design-and-property}

このsubsectionでは本論文で提案する型プロファイラの実装であるTypeProfiler.jlの設計と，その性質に関する説明を行う．

\subsubsection{設計} \label{subsubsection:type-profiler-design}

このsubsubsectionでは本論文で提案する型プロファイラの実装であるTypeProfiler.jlの

設計について説明する．

実際の実装は\url{https://github.com/aviatesk/TypeProfiler.jl}で公開している．

\paragraph{TypeProfiler.jlが報告するエラー} \label{paragraph:type-profiler-error-statement}

TypeProfiler.jlは以下のエラーを報告する．

\begin{description}

\item [\texttt{UndefVarError}] 未定義の変数を参照した場合に報告する

\item [\texttt{NoMethodError}] generic functionの呼び出しにおいて，

推論されている引数組型に対してdispatchされうるメソッドが存在しない場合に報告

\item [\texttt{MethodAmbiguityError}] generic functionの呼び出しにおいて，

推論されている引数達の型が全てconcrete typeであり，かつそれらのdispatchに

method ambiguity\footnote{

method ambiguityについては，

\url{https://docs.julialang.org/en/v1/manual/methods/\#man-ambiguities-1}

を参照せよ．

}がある場合に報告

\item [\texttt{ConditionError}] 条件分岐式の条件として，

\verb|Bool|型以外のオブジェクトが推論されたときに報告

\item [\texttt{InvalidBuiltinCallError}] builtin functionの呼び出しにおいて，

推論されている引数組型が型エラーが生じうるものである場合に報告

\end{description}

\paragraph{基本的な実装} \label{paragraph:type-profiler-basic-implementation}

TypeProfiler.jlは以下のように実装されている．

まず，入力として受け取ったプログラムのそれぞれのプログラム片

（Juliaの実行における単位となる各コード部分）に対して，

次のようなトップレベルの操作を行い，プログラムを型レベルで仮想実行する．

\begin{enumerate}

\item プログラム辺をパースしsurface ASTを得る．

さらにsurface ASTに含まれるマクロを全て展開し，lowered formを得る．

% TODO: もっと正確に記述する

\item モジュールの使用や，型・generic function・マクロの定義などの

"toplevel action"については通常のJuliaの実行プロセスに従って実行する．

以降のプロセスはそれ以外の場合とする．

\item lowered formの各statementを走査しエラーが発生しうる箇所を記録する．

\begin{itemize}

\item トップレベルの変数への代入は型レベルで行う．

\item 変数参照が含まれている場合，その変数がすでに定義されているか確かめる．

そうでない場合，\verb|UndefVarError|を記録する．

\item 条件分岐が含まれている場合，その条件式の型が\verb|Bool|ないとき，

\verb|ConditionError|を記録する．

\item 関数呼び出しが含まれている場合，後述する型プロファイリングを行い，

推論された型をその関数呼び出しの返り値型とする．

\end{itemize}

\end{enumerate}

関数呼び出しに対しては，次のような型プロファイリングを行う．

\begin{enumerate}

\item 関数呼び出しがbuiltin-functionの呼び出しである場合，

TypeProfiler.jlが実装する型検査関数（paragraph~\ref{paragraph:type-check-function}参照）

を用いてその呼び出しのプロファイリングを行い，

型エラーが生じうる引数型が与えられている場合，

\verb|InvalidBuiltinCallError|を記録する．

以降の操作はgeneric functionの呼び出しの場合とする．

\item まず推論されている引数組型を用いて，マッチするメソッドを求める．

マッチするメソッドがない場合，\verb|NoMethodError|を記録する．

推論されている引数達の型が全てconcreteでかつ，マッチしたメソッド達に

method ambiguityがある場合，\verb|MethodAmbiguityError|を記録する．

それ以外の時，マッチしたそれぞれのメソッドに対して以下の操作を行う．

\item その時点で得られている引数達の型を用いて，

そのメソッドの呼び出しに対しJuliaの型推論ルーチンを走らせ，

\kenten{そのメソッド呼び出しの}typed lowered formを得る．

\item 3.で得られるtyped lowered formの各statementを走査し，

エラーが発生しうる箇所を記録する．

この操作はトップレベルのlowered formに対するものとほぼ同様である．

statementにgeneric function呼び出しが含まれる場合，

この型プロファイリングを再帰的に行うが，

そのgeneric functionと推論されている引数組型の組み合わせに対して

既にプロファイリングが行われている場合は，

プロファイリングを行わない．

\end{enumerate}

以上のプロセスにおいて，エラーが生じるのが確定している場合，

TypeProfiler.jlは特殊な型\verb|Unknown|を導入し，

以降\verb|Unknown|が含まれる式に関してはプロファイリングは行われない\footnote{

この\texttt{Unknown}型は，Juliaの型推論ルーチンにおける\texttt{Bottom}型に相当する．

}．

入力のプログラム中の全てのプログラム片に対して以上のプロセスを順に行った後，

最後に記録された全てエラーを仮想的なコールスタックとともに報告する．

\paragraph{型検査関数} \label{paragraph:type-check-function}

Juliaの型推論システムはもともとエラー検出を目的に作られていないため，

Julia本体が実装しているbuiltin functionの型遷移関数は，

たとえ与えられた引数型組が型エラーを起こし得るものであってもその情報を伝播させない場合がある．

例えば，builtin function \verb|isa(a, t)|は

第2引数として\verb|Type|型をsupertypeとする型\footnote{

具体的には，

\texttt{Core.TypeofBottom}型（\texttt{Union\{\}}の型）と

\texttt{DataType}型，

\texttt{Union}型，

そして\texttt{UnionAll}型の4つである．

}のオブジェクト\verb|t|を受け取り，

第1引数\verb|a|が\verb|t|のインスタンスであるかどうかのboolean値を返す．

\verb|t|が\verb|Type|型をsupertypeとする型のオブジェクト\kenten{ではない}場合，エラーとなる．

その遷移関数\verb|Core.Compiler.isa_tfunc|は，

例えば第2引数が\verb|Any|であっても正しい返り値型\verb|Bool|を返す

\footnote{

\url{https://github.com/JuliaLang/julia/blob/3720edfc06ee8687b54ee7fbb908c9f03f4fc557/base/compiler/tfuncs.jl\#L502-L536}

で動作確認．

}が，

当然\verb|Any|のインスタンスには\verb|Type|型をsupertypeとする型以外の型のオブジェクト

も含まれる（例えば\verb|1|がそうである）．

Juliaの型推論がもっぱらパフォーマンスの向上を目的として行われていることを考えれば，

わざわざ実際には発生しないかもしれないエラーの情報を伝播させる必要はないため，

この挙動は自然である．

一方でTypeProfiler.jlはエラーの検出を目的としているため，

こうした場合により保守的にエラーの可能性を報告する方が好ましい．

そのため，builtin-functionの呼び出しについては，

Julia本体に実装されている型遷移関数の返り値型によりエラーの検出とするのではなく，

builtin-functionの呼び出しにおける型エラーの可能性を判定する関数

（これを便宜上\textbf{型検査関数}と呼ぶ）を独自に実装する．

\paragraph{ヒューリスティックの調節} \label{paragraph:type-profiler-heuristic}

subsubsection~\ref{subsubsection:inference-convergence-and-heuristic}でも述べたように，

wideningによる推論型の抽象化は，Juliaの型推論ルーチンの収束性を保証する上で必要不可欠であり，

TypeProfiler.jlが行う型プロファイリングにおいても欠かすことはできない．

一方で，wideningを行う\textbf{程度}については，必ずしもJuliaの型推論と型プロファイリングで一致している必要はないため，

型プロファイリングの実行速度と，型エラー検出の正確性のトレードオフを検証しつつ，

wideningの程度を調整するヒューリスティックについて再調節することができる．

また，paragraph~\ref{paragraph:inference-heuristic}で言及した

Juliaの型推論の収束を早める各種のヒューリスティックについても，同様のことが言える．

ここではそれらのヒューリスティックのうち，TypeProfiler.jlの実装において

Juliaの型推論ルーチンとは異なるアプローチを取っているものについて説明する

\footnote{

これらのヒューリスティックは，\href

{https://github.com/JuliaLang/julia/tree/3720edfc06ee8687b54ee7fbb908c9f03f4fc557}

% NOTE: update this date when you edit this section

{2020年2月5日時点でのJuliaレポジトリのmasterブランチ}

で実装されているものである．

}．

\begin{itemize}

\item generic functionの呼び出し時，マッチしたメソッドが5つ以上である場合，

それらのメソッドに対する型推論は行わず，直ちにそのgeneric functionの返り値型を

\verb|Any|とする．

\end{itemize}

TypeProfiler.jlはマッチしたメソッドの全てに対して型プロファイリングを行う．

\subsubsection{性質} \label{subsubsection:type-profiler-property}

\paragraph{型安全性}

TypeProfiler.jlの性質として，

\ref{theorem:inference-correctness}を解釈しなおすことで，次の系を与えることができる．

\begin{corollary*}[型プロファイリングによる型安全性]

\label{corollary:type-profiler-type-safety}

型プロファイリングのプロセスが到達したあるstatementに対して

型エラーが報告されない場合，そのstatementは型安全である．

\end{corollary*}

\paragraph{マクロを含むコードに対する解析}

TypeProfiler.jlはマクロ展開後のプログラム表現に対して解析を行うため，

マクロを含むプログラムも問題なくプロファイリングすることができる\footnote{

マクロ展開そのものに対する解析は今後の課題である（subsection~\ref{subsection:issues}参照）．

}．

\paragraph*{type stability}

型推論によりプログラム中の式の型がconcrete typeに決定されることを，

\textbf{type-stability}\cite{type-stability}という．

型プロファイリングされるプログラム中の式の型がconcrete typeに推論されやすい場合，

つまりプログラムがtype-stableであるほど，

TypeProfiler.jlは上述した型プロファイリングによる型安全性を示しやすい．

逆に，型推論の過程において型が抽象的になればなるほど，

TypeProfiler.jlは型エラーを報告しやすくなり

\footnote{

型プロファイリングにおいて，推論型は最終的にbuiltin functionの呼び出しに伝播する．

型検査関数は型が抽象的であるほど，型エラーを報告しやすい．

}，

型安全性を示すのは難しくなる．

ここではTypeProfiler.jlがどの程度型安全性を示すことができるのかに関する参考として，

Bezansonらが行った実験\cite{julia-2012}を紹介する．

Juliaの（Julia自身で実装されている）コア機能と標準ライブラリのテストコードを走らせたとき，

プログラム中の式がどの程度concrete typeに推論されたかを調べたところ，

以下のような結果が得られたという\footnotemark．

\begin{enumerate}

\item 推論が行われた式は合計で135375個であった．

\item そのうち，84127個（62\%）の式が\texttt{Any}型よりもspecificな型を持つと推論された．

\item 2.の式のうち，80874個（96\%）の式がconcrete typeに推論された．

\end{enumerate}

この結果から，TypeProfiler.jlはプログラム中のおおよそ60\%程度の部分に対してその型安全性を

示せることが期待できる．

\footnotetext{

もっとも，この数値は2012年のJuliaのコードベースに対して行われた実験で得られたものである

ことには注意が必要である．

また，コードベース中に含まれるdead codeや，

特定のコードがその他のコードに比べて使用されやすい

（そして使用されやすいコードは一般によく型が付くように書かれる）

ことによる影響，

そしてコア機能や標準ライブラリのコード自体が一般にユーザコードよりもtype-stableに

書かれているというバイアスにも注意を払わなくてはならない．

}