13

DataKinds私は、新しい拡張機能を使用して、サイズがタイプにエンコードされているベクトルと行列で遊んでいます。基本的には次のようになります。

data Nat = Zero | Succ Nat

data Vector :: Nat -> * -> * where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

Functorここで、とのような典型的なインスタンスが必要ですApplicative。Functorは簡単だ：

instance Functor (Vector n) where
    fmap f VNil = VNil
    fmap f (VCons a v) = VCons (f a) (fmap f v)

しかし、Applicativeインスタンスには問題があります。純粋にどのタイプを返すかがわかりません。ただし、ベクトルのサイズで帰納的にインスタンスを定義できます。

instance Applicative (Vector Zero) where
    pure = const VNil
    VNil <*> VNil = VNil

instance Applicative (Vector n) => Applicative (Vector (Succ n)) where
    pure a = VCons a (pure a)
    VCons f fv <*> VCons a v = VCons (f a) (fv <*> v)

ただし、このインスタンスはすべてのベクトルに適用されますが、型チェッカーはこれを認識しないためApplicative、インスタンスを使用するたびに制約を実行する必要があります。

さて、これがインスタンスにのみ適用される場合Applicativeは問題にはなりませんが、このような型でプログラミングする場合は、再帰的なインスタンス宣言のトリックが不可欠であることがわかります。たとえば、TypeComposeライブラリを使用して行列を行ベクトルのベクトルとして定義すると、

type Matrix nx ny a = (Vector nx :. Vector ny) a

型クラスを定義し、再帰的なインスタンス宣言を追加して、転置と行列の乗算の両方を実装する必要があります。これにより、インスタンスが実際にはすべてのベクトルと行列に適用される場合でも、コードを使用するたびに実行しなければならない制約が大幅に増加します（制約が役に立たなくなります）。

これらすべての制約を回避する必要を回避する方法はありますか？タイプチェッカーを拡張して、そのような帰納的構造を検出できるようにすることは可能でしょうか？

4

1 に答える 1

15

の定義pureはまさに問題の核心です。そのタイプは、完全に定量化され、修飾されている必要がありますか?

pure :: forall (n :: Nat) (x :: *). x -> Vector n x            -- (X)

実行時に をpure発行するVNilかVCons. それに対応して、現状では、ただ持つことはできません

instance Applicative (Vector n)                                -- (X)

あなたは何ができますか？Strathclyde Haskell Enhancementを使用して、Vec.lhsサンプル ファイルで、pure

vec :: forall x. pi (n :: Nat). x -> Vector {n} x
vec {Zero}    x = VNil
vec {Succ n}  x = VCons x (vec n x)

のpiコピーをn実行時に渡す必要があります。これpi (n :: Nat).は次のように脱糖します

forall n. Natty n ->

どこでNatty、実生活ではより平凡な名前で、によって与えられるシングルトンGADTです

data Natty n where
  Zeroy :: Natty Zero
  Succy :: Natty n -> Natty (Succ n)

コンストラクターをコンストラクターにvec変換するだけの方程式の中括弧。次に、次の悪魔的なインスタンスを定義します (デフォルトの Functor インスタンスをオフに切り替えます)NatNatty

instance {:n :: Nat:} => Applicative (Vec {n}) where
  hiding instance Functor
  pure = vec {:n :: Nat:} where
  (<*>) = vapp where
    vapp :: Vec {m} (s -> t) -> Vec {m} s -> Vec {m} t
    vapp  VNil          VNil          = VNil
    vapp  (VCons f fs)  (VCons s ss)  = VCons (f s) vapp fs ss

さらなる技術が必要です。制約{:n :: Nat:}は、証人が存在することを必要とする何かに脱糖しNatty n、スコープ型変数の力によって、{:n :: Nat:}明示的に証人するのと同じ召喚状です。手書き、それは

class HasNatty n where
  natty :: Natty n
instance HasNatty Zero where
  natty = Zeroy
instance HasNatty n => HasNatty (Succ n) where
  natty = Succy natty

制約を に置き換え、{:n :: Nat:}対応HasNatty nする項を に置き換え(natty :: Natty n)ます。この構造を体系的に行うことは、タイプ クラス Prolog で Haskell タイプチェッカーのフラグメントを記述することになります。これは私の喜びの考えではないため、コンピューターを使用します。

Traversableインスタンス (私の慣用句のブラケットと、サイレントなデフォルトの Functor および Foldable インスタンスを許してください) は、そのようなおかしな突っ込みを必要としないことに注意してください。

instance Traversable (Vector n) where
  traverse f VNil         = (|VNil|)
  traverse f (VCons x xs) = (|VCons (f x) (traverse f xs)|)

それ以上の明示的な再帰なしで行列の乗算を取得するために必要な構造はこれだけです。

TL;DR シングルトン構造とそれに関連付けられた型クラスを使用して、再帰的に定義されたすべてのインスタンスを、明示的な再帰によって計算できる型レベル データのランタイム監視の存在にまとめます。

設計上の意味は何ですか？

GHC 7.4 には型昇格の技術がありますが、SHE にはまだシングルトン構造のpi型が用意されています。昇格されたデータ型について明らかに重要なことの 1 つは、それらが close であることですが、それはまだはっきりとは現れていません。どういうわけか、forall (n :: Nat).シングルトンを要求することは常に合理的ですが、そうすることで生成されたコードに違いが生じます: 私のpi構造のように明示的であるか、辞書のように暗黙的であるかにかかわらず{:n :: Nat:}、追加の実行時情報がありますスリングアラウンド、それに応じて弱い自由定理。

GHC の将来のバージョンに対する未解決の設計上の問題は、型レベル データに対するランタイム監視の存在と非存在の間のこの区別をどのように管理するかということです。一方では、制約の中でそれらが必要です。一方で、それらをパターンマッチする必要があります。たとえば、pi (n :: Nat).明示的なものを意味する必要があります

forall (n :: Nat). Natty n ->

または暗黙の

forall (n :: Nat). {:n :: Nat:} =>

? もちろん、Agda や Coq などの言語には両方の形式があるため、Haskell もそれに倣う必要があります。確かに進歩の余地はあり、私たちはそれに取り組んでいます!

于 2012-05-10T09:22:00.293 に答える