确保异构列表包含一个类型类

Question

我写我自己的异类列表实现(我第一次读到异类列表在这里和我的实现非常相似,他们的)

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

data HList a where
  (:>) :: a -> HList b -> HList (a ': b)
  Nil  :: HList '[]
infixr 6 :>

这很棒; 然而,一旦我发现自己正在使用这些异构列表,我发现自己经常想要表达一个每个类型属于特定类型类的想法.我天真的第一个解决方案是HList完全为每个新类型类重写数据类型.这是它的Eq(例如,它不是我唯一关注的类型类):

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

data EqHList a where
  (:>) :: (Eq a) => a -> EqHList b -> EqHList (a ': b)
  Nil :: EqHList '[]
infixr 6 :>

这有很多问题.首先,我需要在每次需要新类型时重写它.此外,在我的旧异构列表上工作的函数不适用于新的异构列表.

我的下一个解决方案是使用空类型.

{-# LANGUAGE GADTs, DataKinds, TypeOperators, FlexibleInstances, FlexibleContexts #-}

data HList a where
  (:>) :: a -> HList b -> HList (a ': b)
  Nil :: HList '[]
infixr 6 :>

class Eqed a

instance Eqed (HList '[])
instance (Eq a, Eqed (HList b)) => Eqed (HList (a ': b))

这里的一个实例Eqed是HList其所有元素都是其实例Eq.这肯定比上一个解决方案更好,但我仍然觉得它缺乏.每次我想谈论不同类型的类时,我仍然会复制粘贴一堆代码.我觉得这是可以通过更多类型级编程解决的问题类型.

有没有更好的办法？

Answer 1

您可以Eqed通过参数化来概括(需要一些扩展,GHC的错误消息将告诉):

import Data.Kind (Constraint)

class CMap (c :: * -> Constraint) (xs :: [*])
instance CMap c '[]
instance (c x, CMap c xs) => CMap c (x ': xs)

然而,这并不是很好,因为CMap c (x ': xs)并不意味着c x,它只是相反的方式.一种方法可能是添加一种方法,该方法可以使用那些单独的约束但看起来很毛茸茸.另一种是使用类型系列:

type family CMap (c :: * -> Constraint) (xs :: [*]) :: Constraint where
  CMap c '[] = ()
  CMap c (x ': xs) = (c x, CMap c xs)