HaskellでHaskellタイプを生成するための施設（「Second Order Haskell」）？

Question

この質問が少しあいまいである場合、事前に謝罪します。週末の空想の結果です。

Haskellの素晴らしいタイプシステムにより、数学的（特に代数的）構造をタイプクラスとして表現することは楽しいことです。つまり、見てください 数値処理！しかし、実際にそのような素晴らしいタイプ構造を利用することは、私にとって常に難しいと思われました。

あなたはそれを表現するための素敵なタイプシステムの方法を持っています v1 と v2 ベクトル空間の要素です V そしてそれ w ベクトル空間の要素です W. 。タイプシステムを使用すると、プログラムの追加を作成できます v1 と v2, 、 だがしかし v1 と w. 。素晴らしい！しかし、実際には、潜在的に数百のベクトル空間で遊びたいと思うかもしれませんし、タイプを作成したくないことは確かです V1, V2, ..., V100 ベクトル空間タイプクラスのインスタンスを宣言します！または、シンボルをもたらす現実世界のデータを読んでいるかもしれません a, b と c - これらのシンボル上の自由ベクトル空間が本当にベクトル空間であることを表現することをお勧めします！

だからあなたは立ち往生していますよね？科学的なコンピューティング設定でベクトル空間でやりたいことの多くを行うには、ベクトル空間タイプクラスを前述し、代わりにランタイム互換性チェックを行う関数があることにより、タイプシステムを放棄する必要があります。あなたはしなければならないべきですか？ Haskellが純粋に機能的であるという事実を使用して、必要なすべてのタイプを生成し、実際のプログラムに挿入するプログラムを作成することは可能ではありませんか？そのようなテクニックは存在しますか？私がここで基本的なものを見落としているだけなら（私はおそらく私は）:-)

編集： ちょうど今私は発見しました Fundeps. 。私は彼らが私の質問とどのように関係するかについて少し考えなければなりません（これに関して啓発するコメントは感謝されています）。

Answer 1

テンプレートhaskell これを許可します。 wikiページ いくつかの有用なリンクがあります。特に ブラット チュートリアル.

トップレベルの宣言構文はあなたが望むものです。入力すること：

mkFoo = [d| data Foo = Foo Int |]

テンプレートのhaskellスプライス（コンパイル時間関数のような）を生成し、宣言を作成します data Foo = Foo Int ラインを挿入するだけです $(mkFoo).

この小さな例はあまり有用ではありませんが、MKFOOに引数を提供して、必要な宣言の数を制御できます。今a $(mkFoo 100) 100個の新しいデータ宣言を作成します。 THを使用して、タイプクラスインスタンスを生成することもできます。私の アダプティブタプル パッケージは、テンプレートHaskellを使用して同様のことを行う非常に小さなプロジェクトです。

別のアプローチは使用することです 派生する, 、タイプクラスインスタンスを自動的に導出します。インスタンスのみが必要な場合、これは簡単かもしれません。

Answer 2

また、Haskellにはいくつかのシンプルなタイプレベルのプログラミング手法があります。標準的な例が次のとおりです。

-- A family of types for the natural numbers
data Zero
data Succ n

-- A family of vectors parameterized over the naturals (using GADTs extension)
data Vector :: * -> * -> * where
    -- empty is a vector with length zero
    Empty :: Vector Zero a
    -- given a vector of length n and an a, produce a vector of length n+1
    Cons  :: a -> Vector n a -> Vector (Succ n) a

-- A type-level adder for natural numbers (using TypeFamilies extension)
type family Plus n m :: *
type instance Plus Zero n = n
type instance Plus (Succ m) n = Succ (Plus m n)

-- Typesafe concatenation of vectors:
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a
concatV Empty ys = ys
concatV (Cons x xs) ys = Cons x (concatV xs ys)

それを取り入れるために少し時間を取ってください。それが機能するのはかなり魔法のようだと思います。

ただし、Haskellのタイプレベルのプログラミングは、機能の不自然な谷にあります。のような依存型の言語 Agda, coq, 、 と 警句 このスタイルをその限界と完全なパワーにしてください。

テンプレートHaskellは、通常のLisp-Macroスタイルのコード生成によく似ています。いくつかのコードを記述してコードを記述し、「ここに生成されたコードを挿入する」と言います。上記の手法とは異なり、計算可能に指定されたコードをそのように記述することはできますが、見られるように非常に一般的なタイプチェックは得られません concatV その上。

したがって、あなたが望むことをするためのいくつかのオプションがあります。メタプログラムは本当に興味深い空間であり、ある意味ではまだ非常に若いと思います。探索して楽しんでください。 :-)