3

強力な型付けに興味をそそられたので、いくつかの Haskell を試してみましたが、これに取り組む最善の方法について混乱しています。

Data.Vector で定義されている Vector データ型では、ネストされた配列を使用して多次元配列を使用できます。ただし、これらはリストから構築され、さまざまな長さのリストは同じデータ型と見なされます (さまざまな長さのタプルとは異なります)。

同じように機能するこのデータ型をどのように拡張する (または類似のものを作成する) ことができるでしょうか。例) コンパイル時にエラーが発生しますか?

タプルは 63 の異なる定義 (有効な長さごとに 1 つ) を書き出すことでこれを管理しているようですが、可能であれば任意の長さのベクトルを処理できるようにしたいと考えています。

4

2 に答える 2

2

これを行うには2つの方法があります。

1）「型付き」の方法：依存型を使用します。これは、Haskellで*の最近のGHC拡張機能を使用してある程度可能DataKindsです。さらに良いことに、 Agdaのような非常に高度な型システムで言語を使用すること。

2）他の方法：次のようにベクトルをエンコードします

data Vec a = {values :: [a], len :: [Int]}

次に、エクスポートのみ

buildVec :: [a] -> Vec a
buildVec as = Vec as (length as)

また、同じ長さのベクトルを使用する他の関数で正しい長さを確認します。たとえば、行列関数またはVec加算で同じ長さのベクトルを確認します。またはさらに良い：マトリックス用の別のカスタムビルダー/コンストラクターを提供します。

*私はちょうど見ました：まさにあなたが望んでいるのはの標準的な例ですDataKinds。

于 2012-05-14T05:57:22.463 に答える
2

型が値に依存するこの形式の型付けは、依存型型プログラミングと呼ばれることが多く、幸運にも、Wolfgang Jeltsch がGADT と TypeFamilies を使用した Haskell の依存型に関するブログ投稿を書きました。

ブログ投稿の要点は、自然数を表す 2 つの型がある場合:

data Zero
data Succ nat

次の方法で、タイプが強制された長さのリストを作成できます。

data List el len where
   Empty :: List el Zero
   cons  :: el -> List el nat -> List el (Succ nat)
于 2012-05-14T07:48:34.833 に答える