6

私は次のGADTを持っています

data Vec n a where
    T    :: Vec VZero a
    (:.) :: (VNat n) => a -> (Vec n a) -> (Vec (VSucc n) a)

クラスを使用して、固定長ベクトルをモデル化する

class VNat n

data VZero
instance VNat VZero

data VSucc n
instance (VNat n) => VNat (VSucc n)

ベクトルに追加関数をプログラムしようとしました：

vAppend :: Vec n b -> Vec m b -> Vec nm b
vAppend T T = T   -- nonsense, -- its just a minimal def for testing purposes

タイプチェッカーはそれが好きではありません：

 Could not deduce (nm ~ VZero)
    from the context (n ~ VZero)
      bound by a pattern with constructor
                 T :: forall a. Vec VZero a,
               in an equation for `vAppend'
      at VArrow.hs:20:9
    or from (m ~ VZero)
      bound by a pattern with constructor
                 T :: forall a. Vec VZero a,
               in an equation for `vAppend'
      at VArrow.hs:20:11
      `nm' is a rigid type variable bound by
           the type signature for vAppend :: Vec n b -> Vec m b -> Vec nm b
           at VArrow.hs:20:1
    Expected type: Vec nm b
      Actual type: Vec VZero b
    In the expression: T
    In an equation for `vAppend': vAppend T T = T
Failed, modules loaded: Vectors.

型変数に関する GHC の問題を説明できる人はいますnmか? そして~、エラーメッセージの正確な意味は何ですか?

4

3 に答える 3

10

現状では、任意の2 つのベクトルを追加することで、任意の長さのベクトルを取得できると言っています。任意の 2 つのベクトルが与えられた場合に長さ VZero のベクトルを生成するはずの署名推論を破棄すると、それは理にかなっていますが、必要なものではありません。ベクトルの結果の型を制約するには、s に関連付けられた型が必要です。自然な方法は、ある種の型ファミリーになりますが、クラスの下にそれを取得できませんでした。いずれにせよ、この種のアイデア全体は、 (ghc-7.4 以降の) 拡張機能のプロモートされた型でより明確に実現されます。これにより、不快な閉じられていない文字が取り除かれますghcvAppendPlusVNatvAppendVNatDataKindsVSuccなどを認めVSucc Charます。回避しようとしていない場合DataKinds、モジュールは次のようになります。

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

data Vec n a where                 -- or: data Vec :: VNat -> * -> * where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a 
                                   -- no class constraint

data VNat  =  VZero |  VSucc VNat  -- standard naturals

type family n :+ m :: VNat         -- note the kind of a ":+" is a promoted VNat
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

vAppend :: Vec n b -> Vec m b -> Vec (n :+ m) b
vAppend T v = v  
vAppend (a :. u) v  = a :. (vAppend u v)

編集: これを見て、Plus- または:+- 型ファミリの行は、引数の種類を明示的に制限する必要があることがわかりました

type family (n::VNat) :+ (m::VNat) :: VNat

などのガベージ型を除外します。つまり、 のような型Char :+ VZeroを好むのと同じ原則に基づいています。また、コンパイラがこれをどの程度利用できるかはわかりませんが、2 つのインスタンスがそれを完全に指定していることがわかります。DataKindsdata VSucc n

于 2012-08-22T15:06:46.197 に答える
9

型シグネチャのすべての型変数は、普遍的に量化されます。これは、関数に型があると言う場合、

Vec n b -> Vec m b -> Vec nm b

n、m、nmおよびの任意の選択に対してb、このタイプは有効でなければなりません。特に、例えば、

Vec VZero Int -> Vec VZero Int -> Vec (VSucc VZero) Int

また、関数の有効な型である必要があります。ただし、2 つのベクトルの追加には、そのような一般的な型はありません。には制約がありますnm。つまり、それnmは型レベルの数値nとの合計ですm。これらの制約を関数の型で表現する必要があります。そうしないと、型エラーが発生します。

あなたの場合、GHCはあなたの定義でnmは実際には であると不平を言っているので、あなたのタイプがあなたが作ることを許可されていないことを示しているVZeroという仮定をしています。nmは~、型の等価性を表す GHC の記号です。

于 2012-08-22T14:33:35.440 に答える
6

GADT の値のパターンマッチングによって関数を書くとき、GHC は各句の型チェック時に、関数の実行時に期待される動作に関する情報を使用します。vAppend関数には句が 1 つしかありません。そのパターンは、 type の値と type の別の値に一致しVec n bますVec m b。GHC の理由は、 が実行時vAppendに両方とも pattern に一致する実引数に適用される場合、実引数の実際の型はorよりも有益な型であるT形式でなければならないからです。この推論が GHC で実装されている方法は、 の一意の節の RHS を型チェックするときに、確かに実際に であり、書かれており、同様にVec VZero bVec n bVec m bvAppendnVZeron ~ VZerom ~ VZero.

関数に対して記述する型は、それが満たす必要のある契約を設定します。表示されるエラー メッセージは、 の実装によって満たされなければならないコントラクトがvAppend一般的すぎるためです。nある長さとmの2 つのベクトルが与えられた場合、任意のサイズvAppendと見なすことができるベクトルを生成する必要があると言っています。実際、GHC は、あなたの RHS の型 が RHSの期待される型 と一致せず、. 実際、利用可能な唯一の仮定は、GHC によると、前の段落のものです。Vec VZero bVec nm bnm ~ VZero

この契約を履行できる唯一の方法undefinedは、条項の右辺として書くことです。それは明らかにあなたが望むものではありません。適切な型を取得する秘訣vAppendは、出力ベクトルのサイズを 2 つの入力ベクトルのそれぞれのサイズに関連付けることです。それは次のようになります。

type family Plus n m
type instance Plus VZero m = m
type instance Plus (VSucc n) m = VSucc (Plus n m)

vAppend :: Vec n b -> Vec m b -> Vec (Plus n m) b
vAppend T T = T

ここで行ったことは、長さは、vAppendと呼ばれる型に対する何らかの関数を介して、への入力の長さによって決定されると言われていますPlus。両方の入力長が である場合、それはsinceおよび と同じVZeroであることがわかります。は第1型族実体の形なので、GHCはそれが と同じであることを知っている。したがって、このブランチでは、GHC はタイプ の RHS を期待しますが、これは簡単に構築できます!Plus n mPlus VZero VZeron ~ VZerom ~ VZeroPlus VZero VZeroVZeroVec VZero b

于 2012-08-22T15:31:23.837 に答える