\section{静的な型エラー検出を考える上でのJulia言語の考察と先行研究} \label{section:2}

このsectionではまずJuliaの重要な性質を概観し，その静的解析に求められる要件を確認する．

その後，他の動的言語における静的解析によるデータ型エラー検出の取り組みと，

現行のエコシステムにおけるJuliaプログラムに対する静的解析の取り組みを紹介し，

本論文において取りうるアプローチを検討する．

\subsection{Julia言語の特徴と静的解析} \label{subsection:2-1}

Juliaは\textbf{generic function（総称関数）ベースのオブジェクト指向言語}である\footnotemark．

数あるJuliaの特徴の中でも，特に以下の2点はJuliaプログラムに対する静的な型解析を考える上で重要である．

\begin{enumerate}

\item generic functionを通じた多相性と最適化

\item 強力なメタプログラミング機能（マクロの頻繁な使用）

\end{enumerate}

このsubsectionではgeneric functionとメタプログラミングという2点からJuliaの性質を概観し，

Juliaプログラムを型レベルで静的解析する必要性と，

その際にどのような困難を生じ得るかをコード例と共に紹介する．

それらのコード例は，subsection~\ref{subsection:experiments-and-comparison}において

型プロファイラを用いて解析される．

\footnotetext{

通常のオブジェクト指向言語だと，

メッセージを受け取るメインのオブジェクトがあり，それによってメッセージの処理方法が定まる．

一方Juliaの場合は，

引数全部のオブジェクトの型によって，

generic functionのどの実装（メソッド）が実行されるかが決まる点（\ref{subsubsection:generic-function}参照）

が異なる．

またJuliaのオブジェクト指向は，

JavaやRubyなどの言語にみられるようなクラスベースのオブジェクト指向ではないことにも

注意されたい．

}

\subsubsection{generic function} \label{subsubsection:generic-function}

Juliaは\textbf{generic function（総称関数）}に対するcode specializationとcode selectionにより，

動的な多相性を保ちつつ，良好なパフォーマンスを得ている\cite{jeff-phd}．

ここで，generic functionは同一の名前の下で多相的な振る舞いをする関数であり，

実行時にある引数型を伴ってはじめて呼ばれたタイミングでコンパイル

（これを\textbf{JITコンパイル}，または単に\textbf{JIT}とよぶ）される．

JITの過程においては，まず引数の型情報を用いてその関数呼び出しに対する型推論が行われ，

呼び出し内で生じる関数（正確にはメソッド）呼び出しのコンパイルタイムにおける決定や，

constant propagation, function inliningなどの標準的な最適化が行われた後，

LLVMフレームワーク\cite{LLVM}を用いた最適化が行われ，

最終的に個々のプラットフォームに対応したマシンコードが生成され実行される．

生成されたコードはキャッシュされ，次回以降の同じ引数型組を伴う呼び出しで使用される．

このgeneric functionのそれぞれの引数型組を伴う呼び出しに対する最適化

のプロセスを\textbf{code specialization}\footnotemark と呼ぶ．

例えば，Juliaに標準で備わっている\verb|sum|関数の呼び出し\verb|sum([1, 0, 1])|は

\verb|Array{Int,1}|（\verb|1|は配列の次元が1次元であることを示す）という引数型に対し最適化されたマシンコードを生成し，

引数型\verb|Array{Float64,1}|を伴う呼び出し\verb|sum([1., 0., 1.])|はまた別に最適化されたコードを生成する．

\footnotetext{

ただし，全ての引数型に対してcode specializationが行われるわけではない．

ヒューリスティック的にある種の引数型に対するcode specializationを制限することで，

過剰なcode generation（\hyperref[subsubsection:eval-process]{Juliaの実行プロセス}参照）が行われてしまうことを避けている．

% IDEA: ヒューリスティックの中身を説明しても面白いかも．

ヒューリスティックの具体的な内容については\cite[p.~11]{jeff-master}が詳しい．

}

また，1つのgeneric functionは複数の実装を持つことができ，

プログラマはgeneric functionの定義時に，引数に型アノテーションを付けることで，その実装

（これを\textbf{メソッド}と呼ぶ）が適用され得る引数型組の集合を記述することができる．

generic functionが呼ばれた時，そのgeneric functionが持つメソッドの中から

全ての引数の実行時の型\footnote{

Juliaの実行時において，全てのオブジェクトの型は\textbf{concrete type（具体型）}である．

一方，\textbf{abstract type（抽象型）}は

各concrete typeの関係性を記述し型システムの階層性を表現する上での

（type latticeのnodeとしての）役割だけを持ち，実行時にインスタンス化されることはない．

}を考慮した上で，

その引数型組に対し最も「特化した（"specific"\footnotemark な）」ものが選択され実行される．

この\textbf{dynamic multiple dispatch}によるメソッドの選択を

\textbf{code selection}と呼ぶ．

\footnotetext{

この「最も"specific"なメソッド」の選択はJuliaの言語機能の中でも特に重要なものの1つであり，

generic functionのメソッドテーブルを引数型組の"specificity"によりソートすることにより

自然に実装することができる．

しかし，一方の引数型組がもう一方のsubtypeである場合など"specificity"が明らかな場合だけでなく，

Juliaの型システム内で表現しうる\textbf{全ての}引数型組の組み合わせに対して適用できる"specificity"は自明ではない．

そのアルゴリズムは現在のところ経験的に実装されており，

その形式はinformalにしか与えられていない\cite{jeff-phd}．

}

具体例として，\verb|sum|関数に対するcode selectionを考えてみる．

Julia v1.5においては\verb|sum|関数には標準ライブラリを含めて計14個のメソッドが与えられている．

そのうちの3つを抜粋する（読みやすさのためにやや改変している）．

\inputminted[frame=lines, linenos]{julia}{code/sums_method.jl}

1行目のメソッドが最もgenericな場合を扱う実装であり，

2行目のメソッドがgenericな配列型に対する実装，

そして3行目のメソッドが特に\verb|Bool|型の要素を持つ配列に特化した実装となっている．

5行目の呼び出しは\verb|(1, 0, 1)|の型\verb|Tuple{Int,Int,Int}|に合うメソッドシグネチャが

\verb|sum(a)|の他に存在しないため，1行目のメソッドにdispatchされる．

次に，6行目の呼び出しは一般的な配列型の引数に特化した2行目のメソッドにdispatchされる．

最後に7行目の呼び出しは，特に\verb|BitArray|型の要素を持つ配列の効率的なメモリレイアウトを利用する

\verb|count|関数を呼び出す3行目のメソッドにdispatchされる．

ここで注意するべきなのは，型アノテーションは基本的にメソッドのdispatchをコントロールする目的のため\kenten{だけ}に用いられるということである．

例えば，上述の\verb|sum(a::AbstractArray; dims=:)|は配列の和を取る次元を指定するキーワード引数\verb|dims|を受け取るため，

型アノテーションを用いて最もgenericなメソッド\verb|sum(a)|とは異なるメソッドとして定義される必要がある

\footnote{

キーワード引数はdispatchにおいて考慮されないため，位置引数の型に対するdispatchを用いる必要がある．

}．

一方，引数\verb|a|を受け取り\verb|a|の各要素に対して\verb|a|の和を足す以下のような

generic function \verb|add_sum|を定義することを考えたとき，

\begin{minted}{julia}

add_sum(a) = a .+ sum(a)

\end{minted}

型アノテーションの有無に関わらず，

実行時に\verb|add_sum|が呼び出された時の引数の型に応じたcode specializationが自動的に行われるため，

例えば\verb|BitArray|型の引数に対して\verb|add_sum|を最適化するために

\jlinline{add_sum(a::BitArray)}のようなアノテーションを付ける必要は\textbf{ない}．

むしろこの場合，\jlinline{add_sum(a::BitArray)}という型アノテーションを付けることで，

例えば，本来ならば問題なく動作する\verb|Tuple{Int,Int,Int}|型の引数に対して\verb|add_sum|を適用できなくなるため，

型アノテーションを付けることはパフォーマンスの向上には繋がらないばかりか，

いたずらにこの関数が持ちうる多相性を損なってしまうことになる

\footnote{

また型アノテーションにより，JITコンパイルの速度面でのパフォーマンスが向上することもない:

\url{https://discourse.julialang.org/t/type-annotation-make-jit-compile-faster/31906/2}

}．

これらの例からも分かるように，様々なユースケースに対して効果的に動作するgeneric functionを用意するために

言語のコア機能やパッケージの開発において型アノテーションを行うことはあっても，

そのエンドユーザがパフォーマンスを得るためにプログラムにアノテーションを付けなくてはならない場面はほとんどない

\footnote{

型アノテーションがcode selection以外の目的で用いられる場面としては，

プログラム中の，型推論で型が決定されない部分に型アノテーションをつけることで，

コンパイラがコードを最適化する上でのヒントを与えるというものがある\cite{type-annotation}．

コンパイラはアノテーションされた型情報を使ってコード生成を行い，

実行時にはアノテーションされた型と実際の型が一致することを確かめるアサーションが行われる．

% IDEA: assignmentのlhsに::が付けられた場合は，

% 実行時型をensureする（必要に応じて\texttt{convert}する）ことも触れる？

}．

以上のような言語設計により，

プログラマは演算子や関数の複雑な振る舞いをgeneric functionのメソッドとして自然にプログラミングすることができ\footnotemark，

またそのそれぞれの振る舞いは実行時の型に応じて決定され最適化されるため，

科学計算の動的な性質に対応しつつかつ効率的に実行されるプログラムを書くことができる．

\footnotetext{

\begin{quote}

Mathematics is the art of giving the same name to different things.

\end{quote}

という，Jules-Henri Poincaréの有名な警句に表されるように，

数学において同一の名前の演算子は使用される文脈により多様かつ複雑な振る舞いをみせる．

Juliaのプログラミングパターンにおいては，その名前から「連想される」振る舞いを行う限り

様々な実装（メソッド）を同一のgeneric functionに追加するが，

そのそれぞれのメソッドが全ての引数の実行時型に応じて動的に呼ばれることで，

そうした数学の複雑な振る舞いを自然にプログラミングすることができる．

}

一方でJuliaのこうした強力な多相性はduck typingにより暗黙的にもたらされるため，バグの温床にもなりうる．

というのも，Juliaのプログラミングパターンにおいては，

良くも悪くもプログラマはgeneric functionがある種out-of-boxに動くことを想定しつつプログラミングをすることになるからである．

Juliaの言語実装の大部分は自身で記述されているおり，言語のコア機能から各パッケージに至るまで様々なレイヤーのコードが多相的にプログラムされている．

Juliaの洗練された言語設計によりそれらのコードは多くの場合でプログラマの期待通りに動くものの，

そうでない場合に発生するエラーをプログラマが事前に予想することは難しい．

例えば，以下のようなコマンドライン引数（文字列型の要素を持つ配列型）を整数にパースし，

それらの和を返す関数\verb|parse_sum|があるとする．

\begin{listing}[ht]

\inputminted[frame=lines]{julia}{code/parse_sum.jl}

\caption{poorly typed code}

\label{lst:target1}

\end{listing}

このプログラムは一見するとバグが含まれていないように見え，実際に\verb|ARGS|の長さが1以上の時は正常に動作する．

しかし，\verb|ints|の型が\verb|Array{Any,1}|であるため

\footnotemark % TODO: たぶん3章でも説明することになる？

，\verb|ARGS|が空の配列である場合に，

4行目の\verb|sum(ints)|の内部における関数呼び出し\verb|zero(T)|

（\verb|T|は\verb|ints|の要素型，この場合は\verb|Any|である）

において，\jlinline{zero(::Type{Any})} という呼び出しのシグネチャが

dispatchされ得るメソッドが存在しないことに起因するエラーが発生する．

この場合，\verb|zero|をオーバーロードし \jlinline{zero(::Type{Any})} に対応するメソッドを追加するか，

2行目を \jlinline{ints = Int[]} として\verb|ints|の要素型まで指定して宣言することでエラーは避けられるものの，

\verb|sum|が引数の要素型に制限を設けず多相的に定義されている以上，

\verb|sum|がgenericな配列型に対して動作すると期待するプログラマがこうしたエラーを事前に予測することは簡単ではない．

\footnotetext{

Juliaは現在のところ逆方向の型推論（"backwards type flow"）を行うことができない\cite{julia-2012}（\ref{subsubsection:inference-algorithm}も参照せよ）．

そのため，

コンテナ型の変数のパラメータ型を変数宣言以降のコードの操作から推論することはできず，

この場合\texttt{ints}には\texttt{[]}の型\texttt{Array\{Any,1\}}がそのまま与えられる．

}

また，こうしたエラーを実行時前に静的に検出することも容易ではない．

というのは，一般にJuliaのgeneric functionの挙動は，その呼び出し時に与えられた引数型に従って決定されるため，

それぞれの関数や変数の定義だけを見て行うシンタックスレベルの解析では，このような型エラーの検出はできないからである．

型アノテーションを付けることでメソッドの引数の型が静的に（型検査可能な程度に）決定される場合，

静的型付けの言語で用いられるようなintra-procedualな型解析を行うことができるが，

上述したようにJuliaの型アノテーションは

generic functionのdispatchをコントロールするために用いられるものであり，

静的解析のために型アノテーションをつけることにより，

元のgeneric functionが持っている多相性が損なわれることがあってはならない．

\subsubsection{メタプログラミング} \label{subsubsection:metaprogramming}

また，Juliaはそのメタプログラミング機能によっても特徴付けられる．

メタプログラミングはJuliaプログラムのいたるところで用いられる．

例えば，上述の\\\verb|sum(a::AbstractArray; dims = :)|メソッドも

実際にはメタプログラミングを用いて，同様の構造を持つ他の関数とまとめて定義されている

\footnote{

\url{https://github.com/JuliaLang/julia/blob/a7cd97a293df20b0f05c5ad864556938d91dcdea/base/reducedim.jl\#L648-L659}

より抜粋．

}．

\inputminted[frame=lines, firstline=3, lastline=12, breaklines]{julia}{code/sums_def.jl}

こうした文字操作的なメタプログラミングは他の動的言語でもよく見られる機能であるが，

Juliaのメタプログラミング機能は，プログラマが（いわゆる「Lispスタイル」の）マクロを通じて

パースタイムにおいてあらゆるプログラムをデータ構造として扱い操作することができるという点で，

\textbf{より}強力である．

上のプログラムにおける\verb|@inline|など\verb|@|から始まるコードがマクロに相当し，

例えば\verb|@inline|マクロは関数定義の式を受け取り，

最適化の過程においてその関数をinliningするように促す「ヒント」をJITコンパイラに与えるメタ情報を関数定義に付与する．

言語のコア機能に限らずJuliaのエコシステムにおいてもマクロは頻繁に用いられており，

例えばJuliaの数理最適化分野のエコシステムにおけるデファクトスタンダードなパッケージである

JuMP.jl\cite{DunningHuchetteLubin2017}

は独自のマクロを効果的に定義し，以下のような明瞭で簡潔なモデリング記法を提供している．

\begin{listing}[ht]

\inputminted[frame=lines, linenos, firstnumber=1, firstline=4, lastline=10]{julia}{code/jump.jl}

\caption{code including macros}

\label{lst:target2}

\end{listing}

このようにJuliaのプログラミングパターンにおいては，

いたるところでメタプログラミングが使用され\footnotemark，

冗長なコードをより簡潔に記述できる他，

科学計算の各分野におけるドメイン特化的な記法を単一の汎用言語のシンタックスの中で表現することができる\cite{jeff-phd}．

\footnotetext{

こうしたパースタイムにおけるマクロ展開

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

によるシンタックスレベルのメタプログラミングの他，

関数のコンパイル時に引数の型情報を用いて新たにコードを生成しそれを実行するstaged programmingも可能である．

Juliaのstaged programmingは上述したgeneric functionのdispatchのメカニズムを用いた非常に自然な言語機能として提供されている．

コードを生成する関数自身がその他のgeneric functionと同じように呼び出され，

生成されたコードは通常の関数呼び出しと同じようにJITコンパイルによる最適化が行われた後，実行される．

}

その一方で，一般にコードを生成するコード，つまりマクロ（あるいはstaged programmmingにおけるcode generator）は

それ自体がバグを含みやすく，またメタプログラミングは適切でない場面で使用された場合，

プログラムの可読性を著しく下げてしまうこともある．

しかも，メタプログラミングされたコードを含むプログラムを静的に解析することは難しい．

というのは，

\verb|eval|のように実行時の値がなければ原理的に解析が不可能なメタプログラミング機能が存在する他，

マクロを含むプログラムの正確な意味を得るためには，

マクロ展開を行った後のプログラムに対する解析を行う必要があるが，

マクロ展開にかかるプロセスは静的解析の実装における1つの障壁になりうる

（paragraph~\ref{paragraph:analyse-code-including-macro}参照）

からである．

\subsubsection*{Juliaの実行プロセスと中間表現} \label{subsubsection:eval-process}

\addcontentsline{toc}{subsubsection}{\nameref{subsubsection:eval-process}}

最後に，以降の説明を容易にするため，Juliaプログラムが実行されるプロセスを大まかにまとめ，

各実行段階におけるプログラムの中間表現を指す用語を導入する\cite{eval-of-julia-code, julia-asts}．\\

以下の操作は全て，実行されるプログラムにおけるそれぞれのプログラム片

（Juliaの実行における単位となる各プログラム部分）に対して行われるものである．

\begin{enumerate}

\item プログラム片をパースし\textbf{surface AST}\footnote{

ASTは"Abstract Syntax Tree"（抽象構文木）の略．

}を得る．

\item surface ASTに含まれるマクロを全て展開（\textbf{マクロ展開}）し，

さらに\textbf{lowering}\footnote{

ここで"lowering"とは，型推論などの解析がしやすいように，

マクロ展開後のsurface ASTをSSA形式\cite{julia-ssa}を取る

lowered form（または単にIR，Intermediate Representationと呼ぶ）

にさらに変換することを指す．

}を行い\textbf{lowered form}を得る．

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

"toplevel action"をインタープリタにより実行する．

以下は関数呼び出しなど"toplevel action"ではない場合の実行プロセスとする．

\item 簡単なヒューリスティック\footnote{

このヒューリスティックの具体的な内容については，

\url{https://github.com/JuliaLang/julia/blob/master/code/toplevel.c\#L588-L819}

を参照せよ．

}を用いて

lowered formをインタープリタにより実行するか，JITコンパイルを行うかを決定する．

以下はJITコンパイルされる場合のプロセスとする．

\item lowered formに対して型推論と最適化を行い，\textbf{typed lowered form}を得る．

\item type lowered formからLLVM命令列を生成する．

\item LLVMがnative codeを生成する．

\item native codeが実行される．

\end{enumerate}

特に5から7のプロセスを指して，\textbf{code generation}と呼ぶ．

\subsection{先行研究} \label{subsection:prev-reseaches}

プログラムの堅牢性よりも記述性を優先し，duck-typingにより強力で柔軟なアドホック多相性を得るという思想は，

他のいくつかの動的型付け言語においても核となるパラダイムであり，

そのトレードオフとして生じるプログラムの品質保証に伴う困難さについてはそれらの言語においても同様の問題意識が存在する．

そうした動的言語で書かれたプログラムに対する型レベルでの解析の取り組みとしては，

これまで大きく以下の2つのアプローチが取られてきた．

\begin{enumerate}

\item プログラムに追加的な型シグネチャを与えることにより，型検査を行う方針

\item 素のプログラムに対し抽象解釈を行い，型を「プロファイリング」する方針

\end{enumerate}

以下ではそれぞれのアプローチについて，適宜既存の具体的なプロジェクトについて言及しつつ，

それぞれの方式におけるトレードオフを考える．

また，最後に現行のJuliaエコシステムにおける静的解析によるバグ検出の試みの例として，

StaticLint.jlを紹介し，本論文の取り組みと比較する上で重要な相違点を説明する．

\subsubsection{追加的な型シグネチャによる型検査} \label{subsubsection:type-check-with-annotation}

この方式では，\textbf{漸進的型付け}\cite{gradual-typing}の考えに基づき，

たとえ動的型付けの言語で記述されたプログラムであっても，

定義が完了したクラスや関数においてはある種の静的なシグネチャが存在することを期待し，

その型シグネチャをプログラマに記述させることで，

ライブラリの実装と使用（呼び出し）がそのシグネチャと矛盾していないか検査を行う\cite{ruby-progress-report}．

検査において多相性は，部分型多相やパラメータ多相の他，

duck-typingに相当するものとしてstructural typingを使用する\footnote{

structural subtypingの表現方法として，mypyは

\href{https://mypy.readthedocs.io/en/latest/protocols.html\#protocols-and-structural-subtyping}{"Protocol"}

と呼ばれるある種のインターフェースを明示的に指定させるが，

Steepはクラスシグネチャのメソッド集合の包含関係から部分型関係を判断する．% REVIEW: 自動でやってくれるのか

}ことで表現され，いずれの場合もプログラマが与えるシグネチャにより明示的に導入される．

この方式を採用する多くのシステムは，静的に型が決定できない場合，

\textbf{動的型}\footnote{

ここで「動的型」は，\href{https://www.typescriptlang.org/docs/handbook/basic-types.html\#any}{TypeScriptにおける\texttt{any}型}

のような，静的に型を決定できない場合に型システムあるいはプログラマが導入し，

以降型システムはその型に対する操作について型検査をスキップするような，特殊な型を指す．

漸進的型付けの考えに基づく型システムにおいては，

動的型を導入することで，静的な型検査を部分的に無視し，

既存のコードに対する型付けを徐々に行うことができるようになるため，

ほとんどのシステムで動的型を導入する．

} を表す特殊な型を導入し検査を続ける．

動的型が導入された場合，型システムは通常何らかの警告を出すが，

以降その動的型に対する操作についての検査は行われないため，

動的型を許容する限り，この方式で導入される型システムは健全ではない．

型シグネチャの記述方法としては，プログラムの実行には関与しない形で追加的に与える方法

\footnote{

例えば，mypyはPython3の標準機能であるdocstringを用いてプログラム中にシグネチャを記述するが，

Steepはプログラム本体とは別のファイルを用意しそこにシグネチャを記述する．

どちらの場合も，型シグネチャはそれぞれの言語との前方互換性を保つ形で与えられるため，

型検査システムを導入したプログラムは元の言語処理系でそのまま動かすことができる．

} の他，

TypeScriptのように元の言語との互換性を保たない拡張言語において

型に関する記述を言語の標準機能として行えるようにするというものがある．

この検査方式を採用したプロジェクトは数多く存在し，

mypy（Python）~\cite{mypy}，Steep（Ruby）~\cite{steep}，TypeScript（JavaScript）~\cite{typescript}など，

既に商用ソフトウェアの場面で実際に広く運用されているものもある．

この方式を採用することのメリットは様々ある．ここではその中でも重要と思われるものを述べる．

\begin{itemize}

\item おおよそ安全な型システムを得ることができる．

\item 型検査はクラスや関数を単位として\textbf{intra-procedural}に行われるため，実用的なパフォーマンスを得やすい．

具体例として，mypyプロジェクトはincremental checkingなど様々なエンジニアリングを経て

Dropbox社の400万行ものコードベースに対し数分で検査可能なパフォーマンスを得ている\cite{dropbox}．

また同様の理由から編集中のコードに対してリアルタイムに型検査を行うことで，

自動補完や推論された型情報のフィードバックなどのプログラマ支援に応用することも

可能である\cite{flow, typescript}．

\item \cite{ruby-progress-report}で触れられているように，

型検査に用いられる型シグネチャ自体がそのライブラリのAPIのある種のドキュメントとして機能しうる．

\item 型アノテーションを元のプログラムのパフォーマンスの向上に用いることが可能な場合がある．

具体例として，mypyの型検査器はそれ自身mypyの型アノテーションが施されたPythonコードで記述されており，

その型情報を用いて専用のコンパイラでCPythonのC拡張モジュールへコンパイルすることで，

元のプログラムと比較して約4倍のパフォーマンスの向上を達成している\cite{dropbox}．

\end{itemize}

次に，この方式のデメリットを考える．

まず，最大のデメリットは，静的な型付けを意識し型シグネチャを書かかなくてはならないことによるプログラマ負担という1点になるだろう．

つまり，動的言語はそもそも

（おおよそ）その動的機能がもたらす柔軟な挙動と簡潔な記述性を目指して設計されているにも関わらず，

この方式においてはプログラマは静的な型付けを意識しつつ，型の記述にかかる冗長性を受け入れなくてはならない\footnote{

もっとも，

型推論を用いる場合プログラマは必要最低限の型を与えればよいことや，

型シグネチャ自体がある種のドキュメンテーションとしての役割を果たし得ること

を考えると，

型の記述に伴う冗長性はそこまで大きな問題としてみなされない場合もあるだろう．

その意味で，静的な型検査に伴う最大のデメリットは，

静的な型付けを意識しなくてはならないことそのものであると考えることもできる\cite{what-is-gradual-typing}．

プログラムの型検査を通すために，プログラマの思考方式は良くも悪くも変化させられ，

また場合によっては型検査を通すためだけのテクニックを覚えなくてはならない

（"Expression Problem"\cite{wadler1998expression}のように，

型システムが自然かつ明快に表現することができない問題が存在する）．

漸進的型付けは，前述の動的型を許すことによりこの問題にアプローチしているとも言えるが，

後述するように動的型の存在自体が漸進的型付けにおける問題点であるとみなすこともできる．

}．

次に，漸進的型付けの性質上，健全な型システムを期待することが難しいということが挙げられる．

動的型の存在の他に，そもそも型システムを与える型シグネチャ自体がプログラマ自身によって与えられることが多く，

それ自体が誤りを含んでいる場合，型検査に意味がなくなってしまう．

後者に関しては，後述する型プロファイリングなど，素の動的型付け言語プログラムからその型情報を

自動生成する手法を組み合わせて用いることで改善できる可能性がある\footnotemark．

\subsubsection{抽象解釈による型プロファイリング} \label{subsubsection:type-profiling}

「型プロファイリング」は素の動的型付け言語で記述されたプログラムを受け取り，

プログラムの実行を型レベルで\textbf{抽象解釈}~\cite{abstract-interpretation, scheme-for-automatic-inference}し，

その過程で発見した型エラーやトレースされた型情報そのものを報告するような手法を指す．

プログラムをそのまま実行するのではなく，あくまで型レベルに抽象化した上で解釈することにより，

実際の実行における制御フローでは到達できないプログラム部分の解析や，

終了しないプログラムやプログラマが予期しない副作用を伴うプログラムなどのプロファイリングも可能であり，

プログラムを実行するよりも有用な情報を引き出し，

バグの発見や，出力された型情報をコード理解に役立てることができる

などの恩恵が期待される\footnotemark[\value{footnote}]．

\footnotetext{

コード理解の応用例として，

遠藤らは型プロファイラの出力を上述の漸進的型付けによる型検査で必要となる

型シグネチャとして利用できる可能性を指摘している\cite{ruby-progress-report}．

}

解析の正確性と実行速度は抽象化の程度に依存し，トレードオフをなす．

追加的な型シグネチャによる型検査（\ref{subsubsection:type-check-with-annotation}）

とは異なり，この方式の先行事例は比較的少なく，

RubyやJavaScriptでの取り組み~\cite{ruby-type-profiler, type-analysis-for-javascript, type-inference-for-javascript}

があるが，いまだ広く実用に用いられているものはないように思われる．\

この方式における利点は次の1点に集約される．

つまり，型プロファイラは追加的な型注釈を必要とせずに行われるため，

動的言語本来のプログラミングスタイルを保ったまま，何らかの型解析を行うことができるということである．

一方で抽象解釈に伴う困難は様々に存在する．

ここではruby-type-profiler~\cite{ruby-progress-report, ruby-type-profiler}で報告されているものを中心に紹介する．

これらの問題点はsection~\ref{section:3}のTypeProfiler.jlの設計においても重要となる．

\paragraph{トップレベルスクリプトの必要性}

基本的に型プロファイリングは\textbf{inter-procedural}に行われる．

そのため，関数やメソッドを定義するプログラムだけでは解析を行うことができず，

それらを起動するエントリポイントとなるトップレベルのスクリプトも含めて与えられることにより解析が可能となる．

そもそも，型解析がもたらすプログラムの品質保証は

パッケージやライブラリの開発において必要とされることが多く，

そのような場面では一般にテストコードが充実していることが期待される．

そのため，そうしたテストコードを

型プロファイリングを行うためのトップレベルスクリプトとして用いることができるものの，

そのテストコードが（抽象解釈する上で）到達しない関数やメソッドは解析することができない．

関数やメソッドの引数として擬似的な入力を与えることで解析を行い，

タイポや未定義エラーなど比較的簡単なエラーを検出するような工夫は考えられるが，

その場合解析の正確性は大きく下がらざるを得ない．

\paragraph{抽象化の程度とスケーラビリティ}

型プロファイリングも含め，一般にinter-proceduralな解析手法はスケーラビリティに問題を持つ．

具体的には，プログラムの抽象解釈では型を一意に決定できない場合，union型などを導入し解釈を続行するが，

条件分岐が続いた場合解析するべき状態の数が増大し，解析に時間がかかってしまう可能性がある．

また，型として（そのパラメータ型がネストしうる）コンテナ型が存在する場合，

そのままでは存在しうる型が有限にならず，抽象解釈のアルゴリズムの停止性を保証できなくなる．

これらの問題は，何らかのヒューリスティックを用いて，

抽象解釈中の状態や抽象値の数を制限することで対処することが多いが，

状態がより抽象化される分だけ解析の正確性は失われてしまうため，

解析の正確性とスケーラビリティはトレードオフの関係をなしている．

実用上必要な解析の正確性を保ちつつ，同時に実用的なスケーラビリティも保てるように

抽象化の程度を調整する必要がある．

\subsubsection{現行のエコシステムにおけるエラーチェッカー: StaticLint.jl} \label{subsubsection:staticlint}

StaticLint.jl~\cite{staticlint}は

Juliaプログラムに対する静的な解析を行いエラーを検出する，

主にエディタのlinting機能のバックエンドとして使用されることを想定したパッケージである．

Juliaプログラム中に含まれる，シンタックスレベルでの解析により検出可能なエラーを，

\date{\today}現在のJuliaエコシステムにおいて最も正確に検出することができ，

また，編集中のコードに対してリアルタイムにlintingした結果をフィードバックすることができる

程度のパフォーマンスを備えている．

ここで，シンタックスレベルの解析とは，surface AST

（\hyperref[subsubsection:eval-process]{Juliaの実行プロセスと中間表現}参照）

の段階のプログラム表現から得られる情報を用いた解析を意味し，

つまりStaticLint.jlは実行プロセス2以降の段階のプログラム表現から得られる情報を用いた解析は行わない．

解析をシンタックスレベルに留めることで，編集中のコードに対するlinterとして機能し得る

パフォーマンスを獲得している一方，

以下で例にあげるような型レベルのエラーやマクロ展開に伴うエラーは検知できない．

\paragraph{シンタックスレベルの解析で検知できないエラー} \label{paragraph:syntax-analysis-limitation}

シンタックスレベルでの解析では検知できないエラーは様々ある．

以下のような非常に簡単なtypoも，型レベルでの解析を行わない場合，検出することはできない．

\begin{listing}[ht]

\inputminted[frame=lines, linenos, firstnumber=1, firstline=23, lastline=33]{julia}{./code/typo.jl}

\caption{typo}

\label{lst:target3}

\end{listing}

このコードでは6行目にtypoが含まれており，

実行すると11行目において\verb|F2|型のオブジェクトに

field \verb|bar|が定義されていないことに起因するエラーが発生する．

しかし，StaticLint.jlはこのプログラムに含まれるエラーを報告しない\footnote{

2020年2月5日時点でのJuliaレポジトリのmasterブランチからビルドしたJuliaを用いて，

StaticLint.jl v3.0.0がlinterとして使用されているjulia-vscode v0.13.1上で動作確認を行った:\

\url{https://github.com/julia-vscode/julia-vscode}

}．

というのは，関数\verb|get_bar|の定義だけを見るとその引数\verb|foo|として実際にどのような

型のオブジェクトが渡されるのか決定できず\footnote{

\texttt{Foo}がabstract typeであることに注意せよ．

}，

また上述したパフォーマンス上の理由から，

エラーが発生する呼び出し\verb|get_bar(F2(1))|までも含めて解析する

inter-proceduralなプログラム解釈は行えないからである．

\paragraph{マクロを含むコードの解析} \label{paragraph:analyse-code-including-macro}

同様にパフォーマンス上の理由からStaticLint.jlは完全なマクロ展開をサポートしていない\footnote{

パッケージ著者と私信にて確認:\\

\url{https://github.com/julia-vscode/StaticLint.jl/pull/64\#issuecomment-575801768}

}．

マクロ展開ではマクロが使われている場所とマクロの定義式の両方を参照しなくてはならず，

ここでもinter-proceduralなプログラム解釈が必要となる．

StaticLint.jlは現状ではエコシステムにおける重要度の高いパッケージのマクロのみを

それぞれ個別にspecial caseすることで部分的に対応している\footnote{

例えば，listing~\ref{lst:target2}の3行目の\texttt{@variable}マクロは，

引数式　\jlinline{0 <= x <= 2} \textbf{だけ}を見ると，

まだ定義されていない変数\texttt{x}を参照しているように見えるが，

実際にはマクロ展開時に，引数式のそれぞれの形式に対応してJuMP.jlの内部的なデータとして

変数（この場合は\texttt{x}）を定義するようなコードを生成するためもちろんエラーは起きない．

一方StaticLint.jlはマクロ展開をサポートしていないため，

v3.0.0まではこの場合に未定義変数の参照エラーを報告していたが，

現在は対応されている:\\

\url{https://github.com/julia-vscode/StaticLint.jl/pull/72}

}．