制約のある異種リスト

Question

Hackageを検索したところ、次のようなものは見つかりませんでしたが、それはかなりシンプルで便利です。ある種のデータ型を含むライブラリはありますか？

data HList c where 
    (:-) :: c a => a -> HList c 
    Nil :: HList c 

私が見つけたすべてのHListは、任意のタイプを持つことができ、制約されませんでした。

私は自分自身をアップロードします。

Answer 1

私はこのデータ型が有用であるかわからない...

• あなたは本当にaは実存資格になりたい場合は、私はあなたが定期的にリストを使用すべきだと思います。あなたのHList cが[Exists c]に同型であり、あなたがまだのすべてを使用することができ、その後

  data Exists c where 
      Exists :: c a => a -> Exists c 
  

  ：ここより興味深いデータ型は、私は確信しているが、それはすべての変異体はすでにパッケージ Hackageの上にあり、Existsだろう通常のリストベースの関数です。一方

• あなたは必ずしも(:-) :: c a => a -> HList cでaは（HListのポイントを挑発するように一種としてそれを持つ）実存的修飾にしたくない場合は、あなたの代わりに、以下を定義する必要があります。

  あなたがHListのすべてのエントリがcを満たすことを要求する場合

  data HList (as :: [*]) where 
      (:-) :: a -> HList as -> HList (a ': as) 
      Nil :: HList '[] 
  

  その後、あなたは、そのインスタンス解像度HListのすべての種類の制約を満たしている場合にのみ機能します[Exists c]にHList asからの注入を目撃するタイプのクラスを作ることができます。

  class ForallC as c where 
      asList :: HList as -> [Exists c] 
  
  instance ForallC '[] c where 
      asList Nil = [] 
  
  instance (c a, ForallC as c) => ForallC (a ': as) c where 
      asList (x :- xs) = Exists x : asList xs 
  

Answer 2

generics-sopパッケージは、箱から出して、これを提供しています。

異種リストは

data NP :: (k -> *) -> [k] -> * where 
    Nil :: NP f '[] 
    (:*) :: f x -> NP f xs -> NP f (x ': xs) 

を使用し、（Data.Functor.Identityから）同一タイプ（generics-sopから）コンストラクタI又はIdentityにそれをインスタンス化することによってgenerics-sopに定義することができます。

この場合、ライブラリは制約Allを提供します。

All Show xs => NP I xs 

はすべて含まれているタイプがShowクラスである異種リストのタイプです。概念的には、Allはタイプレベルのリスト内のすべての要素についての制約を計算タイプの家族である：

type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where 
    All c '[]  =() 
    All c (x ': xs) = (c x, All c xs) 

（それは部分的にできるように実際の定義では、Allを追加型クラスに包まれているだけということ適用されます）。

さらにライブラリには、共通の制約がある場合、NPを走査して変換するあらゆる種類の関数が用意されています。

Answer 3

何が本当にしたいことは

あなたはどちらか通常の異質リスト

type HList = HKList Identity 

または一部の各値に添付定数型e（または他の興味深いの追加情報と同様に使用することができます

data HKList :: (k -> *) -> [k] -> * where 
    Nil :: HKList f '[] 
    (:*) :: f x -> HKList f xs -> HKList f (x ': xs) 

ですファンクタ）

HKList ((,) e) 

または追加情報辞書

data Has c a where 
    Has :: c a => a -> Has c a 

type ConstrainedList c = HKList (Has c) 

でキャプチャそれとも、制約

class All c xs where 
    dicts :: HKList (Dict1 c) xs 

instance All c '[] where 
    dicts = Nil 

instance (All c xs, c x) => All c (x ': xs) where 
    dicts = Dict1 :* dicts 

満たすタイプのリストのすべてのアイデアを定義するために使用できる唯一の捕獲制約

data Dict1 :: (k -> Constraint) -> k -> * where 
    Dict1 :: c k => Dict1 c k 

のリストを維持する上で

または種類でできることその他のものk -> *

あなたは自由にすることができますエリーAll c xs => HList xsとHKList (Has c) xs

zipHKList :: (forall k. f k -> g k -> h k) -> HKList f xs -> HKList g xs -> HKList h xs 
zipHKList _ Nil Nil = Nil 
zipHKList f (x :* xs) (y :* ys) = f x y :* zipHKList f xs ys 

allToHas :: All c xs => HKList Identity xs -> HKList (Has c) xs 
allToHas xs = zipHKList f dicts xs 
    where 
    f :: Dict1 c k -> Identity k -> Has c k 
    f Dict1 (Identity x) = Has x 

hasToAll :: HKList (Has c) xs -> Dict (All c xs) 
hasToAll Nil = Dict 
hasToAll (Has x :* xs) = 
    case hasToAll xs of 
    Dict -> Dict 

full code

での作業の間の変換私は、様々なプロジェクトのために数回前にこれを書いたが、私はそれがどこかKosmikus pointed out that it's in generics-sopまでライブラリに知りませんでした。