Haskellの多次元配列

Question

私は強い型付けに興味をそそられたので、私はいくつかのHaskellのをしようとしてきた、と私はこれに対処する最善の方法について困惑している：

で定義されたベクトルデータ型Data.Vectorでは、ネストされた配列を使用して多次元配列を使用できます。しかし、これらはリストから構成され、さまざまな長さのリストは同じデータ型とみなされます（さまざまな長さのタプルとは異なります）。

どのようにこのデータ型を拡張（または類似のものを書き込み）可能性があるのと同じように機能し、異なる長さのベクトルが異なるデータ型であると考えられ、そう有する多次元アレイ/マトリックスを作成しようとしている除きます異なる長さの行（たとえば）はコンパイル時にエラーを起こすでしょうか？

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

1）「型付け」方法：依存型を使用して

Answer 1

は、私がこれを行うための2つの方法を参照してください。これは、ある程度まで、Haskellで可能であり、最近のGHCの拡張子はDataKinds *です。さらに、という高度なタイプのシステム（Agdaなど）の言語を使用することもできます。

2）他の方法：、そして

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

ようなあなたのベクトルをエンコードエクスポートのみ

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

と、例えば、同じ長さのベクトルを使用する他の機能で正しい長さを確認行列関数内の同じ長さのベクトルを保証するか、またはVec追加で保証する。それ以上の場合：行列用に別のカスタムビルダー/ ctorを提供してください。

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

Answer 2

タイプが値に依存するタイプのタイプは、しばしば依存型プログラミングと呼ばれ、運があるので、Wolfgang JeltschはGADTとTypeFamiliesを使用してHaskellの従属型についてa blog postを書きました。

ブログ投稿の要点は、我々は自然数を表す2つのタイプがある場合ということです：

data Zero 
data Succ nat 

1をタイプしてリストを作成することができますが、次のように長さを施行：

data List el len where 
    Empty :: List el Zero 
    cons :: el -> List el nat -> List el (Succ nat)