Haskell のData.Typeable
.
どのような問題をどのように解決しますか?
Haskell のData.Typeable
.
どのような問題をどのように解決しますか?
Data.Typeable
は、静的型付け言語で遅延(動的)型チェックを実装するためのよく知られたアプローチ(Harperなどを参照)のエンコーディングです-ユニバーサル型を使用します。
このような型は、後のフェーズまで型チェックが成功しないコードをラップします。コンパイラーは、プログラムが正しく入力されていないものとして拒否するのではなく、実行時チェックのためにプログラムを渡します。
このスタイルはAbadietal。に端を発し、CheneyとHinzeによってHaskellのために開発され、すべての動的タイプを表すラッパーとして使用され、Typeable
クラスはSPJとLammelのSYB作業の一部として表示されます。
参照
教科書でも:動的型(入力可能な表現付き)は静的に型付けされた言語であり、Harperch20の1つの型のみです。
20.4型なしとは単一型を意味します
型なしのラムダ計算は、再帰型を使用して型付き言語に忠実に埋め込むことができます。これは、すべての型指定されていないλ-termが、λ-termの表現の実行が用語自体の実行に対応するように、型付き式としての表現を持っていることを意味します。この埋め込みは、ℒ{+×⇀µ}でのλ-calculusのインタープリターを作成することではなく(確実に実行できます)、再帰型の言語で型付き式として型なしλ-termを直接表現します。 。
重要な観察は、型なしのλ計算は実際には単一型のλ計算であるということです! 力を与えるのは型 がないということではなく、再帰型という1つの型しかないということです。
D = µt.t→t。
これは、とりわけ型の命名を可能にするライブラリです。型a
が宣言されている場合、型の任意の値であるwhereTypeable
を使用してその名前を取得できます。また、限定された型キャストも特徴です。show $ typeOf x
x
a
(これは、C++ の RTTI または動的言語のリフレクションに多少似ています。)
Data.Typeable
Haskell の のようなライブラリについて私が見つけた最も初期の記述の 1 つは、 1992 年の John Peterson によるものです: http://www.cs.yale.edu/publications/techreports/tr1022.pdf
私が知っている、実際のData.Typeable
ライブラリを紹介した最初の「公式」論文は、2003 年の Scrap Your Boilerplate の最初の論文です。
私は、ここの誰かがチャイムを鳴らすことができる介在する歴史がたくさんあると確信しています!
Data.Typeableクラスは、主にScrap Your Boilerplate (SYB) スタイルの汎用プログラミングに使用されます。こちらもご覧くださいData.Data
SYB は、ユーザーが作成したさまざまな型に対して、印刷、カウント、検索、置換などの操作を一様に実行するためのコレクション コンビネータを定義するという考え方です。Typeable
型クラスは必要な配管を提供します。
deriving Data.Typeable
現代の GHC では、必要なインスタンスを提供するために独自の型を定義するときに、単に言うことができます。