4

私はこのデータ型を持っています。これはテーブルを表す必要があります。

data R = R [Bool]  deriving Eq -- Row
data T = T [R]     deriving Eq -- Table

問題は、異なる長さの行のテーブルを作成できることです。例：

tab =T [R [True, False, True, True],
        R [False, False, True, False],
        R [False, False, False, True],
        R [False, False]]

のデータ定義を変更してT、すべてのR要素が同じ長さになるようにすることは可能ですか？

4

4 に答える 4

10

うん、それを達成するためのかなり標準的な方法があります。ただし、その代償として、標準のリスト機能を使用できません (標準のリストを使用しないため)。アイデアは次のようになります。最初にすべての「リスト」の長さを示す背骨を作成し、次に背骨の下部に実際のリストを作成します。リストの長さはさまざまな方法でエンコードできます。以下では、単純な単項番号付けシステムを使用してそれを行う方法を示しますが、もちろん、他の番号付けシステムを使用してより効率的なバージョンを設計することもできます。

data BalancedLists_ a as
    = Nil [as]
    | Cons (BalancedLists_ a (a, as))

type BalancedLists a = BalancedLists_ a ()

たとえば、2 つの長さ 3 のリストを含むバランスの取れたリストは次のようになります。

Cons (Cons (Cons (Nil [(1, (2, (3, ()))), (4, (5, (6, ())))])))

Ralf Hinze によるManufacturing Datatypesと呼ばれる、この手法を 100 の異なる方向に拡張した素晴らしい論文があります。

于 2012-09-19T13:16:12.217 に答える
8

でできますDataKinds。ただし、これは複雑すぎる可能性があります。

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
-- requires 7.4.1, I think

data Nat = S Nat | Z

infixr 0 :.
data R (n :: Nat) where
  Nil :: R Z                     -- like []
  (:.) :: Bool -> R n -> R (S n) -- and (:)

data T (n :: Nat) = T [R n]

-- OK
test1 = T [(True :. True :. Nil), (True :. False :. Nil)]

-- will fail
test2 = T [(True :. True :. Nil), (False :. Nil)]

スマートコンストラクターを使用した @MathematicalOrchids 代替アプローチをお勧めします。

編集：何DataKindsをしますか。

拡張機能により、コンパイラは、書き込む各データ型DataKinds以外の*新しい種類と、コンストラクターからこの種類に存在する新しい型を自動的に作成できます。

したがってNat、 は単純な ADT であるだけでなく、 kind Nat、型コンストラクターZ :: Nat、および も生成しS :: Nat -> Natます。これは、すべての種類の種類を使用するのではなく、自然数の表現のみが存在する新しい種類を使用することSに匹敵します。Maybe :: * -> *Nat

ポイントは、混合型の型コンストラクターも定義できるようになったことです。これの古典的な例は次のVecとおりです。

data Vec (n :: Nat) (a :: *) where {-...-}

種類がありVec :: Nat -> * -> *ます。同様に、Thas kind がありT :: Nat -> *ます。これにより、型エンコードされた定数の長さで使用でき、異なる長さの 2 つの行が一緒に配置されると、型エラーが発生します。

これは非常に強力に見えますが、実際には制限されています。このような表現からすべてを引き出すには、Agdaのような依存型言語を使用する必要があります。

于 2012-09-19T10:41:46.377 に答える
4

リスト型は、任意のサイズのコンテナーを表します。タプルを使用して特定のサイズを強制することができますが、実際には「小さい」サイズに対してのみ実行可能です。例えば：

data R = R (Bool, Bool, Bool, Bool) deriving Eq

これで、各行には常に正確に 4 つのセルが含まれます。

実際に必要なのは、テーブル内のすべての行で同じである限り、行を任意のサイズにできるようにすることです...それははるかに困難です。型システムでこれをエンコードする方法はいくつかありますが、どれも特に「単純」ではありません。

もう 1 つの方法は、コンパイル時に条件を保証しようとするのではなく、実行時に条件を強制することです。行とテーブルの型を定義するモジュールを書くことができますが、それらの定義を隠し、これらの型を操作する関数のみを公開して、必要な不変変数 (つまり、すべての行が同じ長さ) を保持します。

于 2012-09-19T09:58:49.143 に答える
1

さらに別の方法は、を使用することData.Arrayです。良い点の 1 つは、配列の配列ではなく、真の多次元配列を使用できることです。タプルを使用してArray.

于 2012-09-19T22:47:14.547 に答える