受约束的异构列表

Question

我搜索了Hackage,找不到类似下面的东西,但它似乎相当简单和有用.是否有包含各种数据类型的库？

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

我找到的所有HLists都可以有任何类型,并且不受约束.

如果没有我会上传我自己的.

Answer 1

我不确定这种数据类型是否有用......

• 如果你真的想要a存在资格,我认为你应该使用常规列表.这里有更多有趣的数据类型Exists,虽然我确定它已经存在于Hackage 包中的各种变体:

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

  然后,你HList c是同构的[Exists c],你仍然可以使用所有常见的基于列表的函数.

• 另一方面,如果你不一定希望a在(:-) :: c a => a -> HList c存在方面具有限定性(让它成为这样的一种蔑视HList),你应该改为定义以下内容:

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

  然后,如果你想要求的所有条目HList满足c,你可以做一个类型类从见证注入HList as到[Exists c]其实例分辨率只有在所有类型的作品HList满足约束:

  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套装提供开箱即用的功能.

可以定义在异构列表generics-sop通过使用

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

并将其实例化为标识类型构造函数I(from generics-sop)或Identity(from Data.Functor.Identity).

然后,库提供约束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给定共同约束的情况下遍历和转换s.