パターン：私は、次のGADTを定義した

Question

：それはない明らかだ場合

data Vector v where 
    Zero :: Num a => Vector a 
    Scalar :: Num a => a -> Vector a 
    Vector :: Num a => [a] -> Vector [a] 
    TVector :: Num a => [a] -> Vector [a] 

、私はシンプルなベクトル空間を実装しようとしています。すべてのベクトル空間にベクトルを追加する必要があるので、VectorとinstanceをNumにして実装します。ベクトル空間では、異なる長さのベクトルを追加するのは意味がありません。これは私が強制したいものです。私はそれがガードを使用することだろう行うことを考えた一つの方法：

instance Num (Vector v) where 
    (Vector a) + (Vector b) | length a == length b = 
           Vector $ zipWith (+) a b 
          | otherwise = 
           error "Only add vectors with the same length." 

あり、このアプローチには、実際には何の問題もありませんが、パターンマッチングでこれを行う方法がなければならないような気がします。それを行うには、おそらく一つの方法は、次のようなものになり、新しいデータ型VectorLength、定義するために次のようになります。そして、

data Length l where 
    AnyLength :: Nat a => Length a 
    FixedLength :: Nat a -> Length a 

を、長さ成分は、Vectorデータ型にこのようなものを追加することができます。

data Vector (Length l) v where 
    Zero :: Num a => Vector AnyLength a 
    -- ... 
    Vector :: Num a => [a] -> Vector (length [a]) [a] 

これは正しい構文ではないことがわかりましたが、これは私がやっている一般的な考えです。最後に、あなたは追加の

instance Num (Vector v) where 
    (Vector l a) + (Vector l b) = Vector $ zipWith (+) a b 

はそのようなことが可能であり、またはこの目的のためにパターンマッチングを使用する他の方法があることを定義することができますか？

Answer 1

あなたが探しているのは、Vectorという名前のものです（この例では混乱します）。あなたは

data Vec (n :: Natural) a where 
    Nil :: Vec 0 a 
    Cons :: a -> Vec n a -> Vec (n + 1) a 

のようなものを書きたいところ一般的に、これらは依存型付け言語で使用されている。しかし、それは、有効なHaskellの（または実際に任意の言語）にはほど遠いです。 GHCへの最近のいくつかの拡張は、この種の表現を可能にし始めていますが、まだありません。

fixed-vectorあなたは比較的安定したGHCで利用可能な固定Vectorの最良の近似を行います。これは、タイプファミリとコンティニュエーションの間にいくつかのトリックを使用して、固定サイズのベクトルのクラスを作成します。コードは罰金コンパイル、それはちょうどあなたが期待したいかなりのように動作していないこと

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators #-} 

import GHC.TypeLits 

data Vector (n :: Nat) a where 
    Nil :: Vector 0 a 
    Cons :: a -> Vector n a -> Vector (n + 1) a 

：GHC 7.6ですでにこのほぼ作品 - ただ、他の回答例に追加する

Answer 2

。のはGHCiの中でそれをチェックしてみましょう：

*Main> :t Nil 
Nil :: Vector 0 a 

グッド

これまで...

*Main> :t Cons "foo" Nil 
Cons "foo" Nil :: Vector (0 + 1) [Char] 

まあ、それは少し奇妙だ...なぜそれが代わりに1の(0 + 1)と言っていますか？

*Main> :t Cons "foo" Nil :: Vector 1 String 

<interactive>:1:1: 
    Couldn't match type `0 + 1' with `1' 
    Expected type: Vector 1 String 
     Actual type: Vector (0 + 1) String 
    In the return type of a call of `Cons' 
    In the expression: Cons "foo" Nil :: Vector 1 String 

ええ。おっとっと。それは1の代わりに(0 + 1)と言われています。それらが同じであることはわかりません。これはGHC 7.8で修正される予定です（少なくともこのケースではこれが予定されています）...数ヶ月のうちに、私は思っていますか？