3

タイプレベルでリストを作成しようとしていますが、制約を適用する方法を理解するのに問題があります。

私のベースコードは次のとおりです。

data Foo z q = Foo1 (z q)
             | Foo2 (z q)

class Qux q -- where ...
class Baz z -- where ...

class Bar a where             -- a has kind *->*
  type BCtx a q :: Constraint -- using ConstraintKinds to allow constraints on the concrete type
  f :: (BCtx a q) => a q -> a q -> a q
  g :: (BCtx a q, BCtx a q') => a q -> a q'

instance (Baz z) => Bar (Foo z) where
  type BCtx (Foo z) q = (Num (z q), Qux q) -- for example
  f (Foo1 x) (Foo1 y) = Foo1 $ x+y -- these functions need access to the type q to do arithmetic mod q
  f (Foo1 x) (Foo2 y) = Foo2 $ x-y
  -- ...

q上記のsは素数冪を表すと考えることができます。また、sの型リストを使用して合成数を表現したいと思いqiます。私は次のようなものを想像しています：

data QList qi qs = QCons qi qs
                 | QNil

データで

data FList c q = FNil 
               | FCons (c (Head q)) (FList c (Tail q))

に(Head q)対応する必要があり、に対応する必要がqiあります。のパラメータは（必然的に）aではなく、のリストであることに注意してください。（これは私が提起している設計上の問題の1つであるため、このリストについてこれ以上具体化したくありません）。私は「モジュラスワイズ」で作業したいと思います：(Tail q)qsqFList(Qux q)(Qux qi)FList

instance (Bar c) => Bar (FList c) where
   type BCtx (FList c) q = () -- Anything I put here is not enough
   f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)
   -- the left call to `f` calls a concrete instance, the right call to `f` is a recursive call on the rest of the list
   -- ...

これらのコードスニペットをGHCで一緒にコンパイルすると、（モジュロ転写、抽象化、および入力エラー）が発生します。

Could not deduce (BCtx c (Head q), BCtx c (Tail q))

その後

Could not deduce (BCtx c (Head (Tail q)), BCtx c (Tail (Tail q)))

等

このエラーが発生する理由はわかりますが、修正方法はわかりません。

具体的には、とのタイプを期待していますFList c q。もちろん、私のリストは、すべてのレベルですべてのBCtx制約を満たします。c~Foo zq~QCons q1 (QCons q2 QNil)

これらの特定のエラーを修正するとコードがコンパイルされるかどうかはわかりませんが、それは始まりです。Barクラス全体は基本的に固定されています（Constraintの種類が必要であり、Barのインスタンスの種類は*-> *である必要があります）。qiパラメータにアクセスする必要があるため、実存型を使用してジェネリックオブジェクトのリストを作成できるとは思いません。種類を変更してFList、バーのコレクションでモジュラス単位で作業QListできるようにします。

御時間ありがとうございます！

4

1 に答える 1

2

タイプリストを処理するには、空のリストと空でないリストを区別し、それらを別々に処理する必要があります。実際にはリストが空である場合と空でない場合があるにもかかわらず、インスタンスが空でないリストを想定しているため、コードで「推測できませんでした」エラーが発生します。拡張子、、、、およびを使用したソリューションをTypeFamilies次に示しTypeOperatorsます。DataKindsGADTs

を使用DataKindsすると、タイプリストが事前定義されます。それらには種類[*]がありますが、種類が期待されるコンテキストで使用される*ため、オペレーターがそれらをキャストする必要があります。

data InjList (qs :: [*])

タイプリストを使用すると、FList次のように定義されます。

data FList c q where
  FNil :: FList c (InjList '[])
  FCons :: c h -> FList c (InjList t) -> FList c (InjList (h ': t))

これはGADTとして定義されており、あるタイプリストFListのタイプに対してのみsを作成できる方法を表現しています。たとえば、この用語のタイプはです。一方、は形式ではないため、タイプの用語（⊥を除く）はありません。のパターンマッチングにより、関数は⊥以外の引数が与えられていることを確認し、さらに空の型リストが渡されているかどうかを判断できます。InjList q'q'FCons [True] FNilFList [] (InjList (Bool ': '[]))BoolInjList q'FList [] BoolFList

Barfor sのインスタンスは、 FListnilリストとconsリストを別々に処理する必要があります。nilリストには空のコンテキストがあります。短所リストには、リストの先頭と末尾のコンポーネントがあります。これは、の関連する型インスタンスの型リストでのパターンマッチングによって表されますBCtx。この関数fは引数を調べて、それが⊥ではないことを確認し、それが空のリストであるかどうかを判断します。

instance (Bar c) => Bar (FList c) where
  -- Empty context for '[]
  type BCtx (FList c) (InjList '[]) = ()
  -- Context includes components for head and tail of list
  type BCtx (FList c) (InjList (h ': t)) = (BCtx c h, BCtx (FList c) (InjList t))

  f FNil FNil = FNil
  f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)

コードをGHCiにロードして、機能することを確認できます。

instance Bar [] where
  type BCtx [] q = Num q
  f xs ys = zipWith (+) xs ys

instance Show (FList c (InjList '[])) where
  show FNil = "FNil"

instance (Show (c h), Show (FList c (InjList t))) => Show (FList c (InjList (h ': t))) where
  show (FCons h t) = "FCons (" ++ show h ++ ") (" ++ show t ++ ")"

$ ghci

> :load Test
> f (FCons [1,2] FNil) (FCons [3,4] FNil)
FCons ([4,6]) (FNil)
于 2013-01-10T06:03:07.877 に答える