haskell - 带有约束的类型列表

Question

我正在尝试在类型级别构建一个列表，但在弄清楚如何强制执行约束时遇到了一些麻烦。

我的基本代码是:

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代表素数幂。我还想使用 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，(Tail q)应对应于qs。请注意，FList 的 q 参数(不一定)不是 (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 类型，其中 c~Foo z 和 q~QCons q1 (QCons q2 QNil)，当然，我的列表将满足每个级别的所有 BCtx 约束。

我不确定修复这些特定错误是否会导致编译代码，但这是一个开始。整个Bar类基本是固定的(需要Constraint种类，并且Bar的实例必须有kind * -> *)。我不相信我可以使用存在类型来创建通用对象列表，因为我需要访问 qi 参数。我愿意更改 FList 和 QList 的类型，以允许我在一组 Bar 上按模进行工作。

感谢您的宝贵时间!

Answer 1

要处理类型列表，有必要区分空列表和非空列表并分别处理它们。代码中出现“无法推断”错误是因为您的实例假定一个非空列表，而实际上该列表可能为空，也可能不为空。这是使用扩展 TypeFamilies 的解决方案, TypeOperators , DataKinds ，和GADTs .

与 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超过类型InjList q'对于某些类型列表 q' 。例如，术语 FCons [True] FNil类型为FList [] (InjList (Bool ': '[])) 。另一方面，由于Bool不是 InjList q' 形式，没有 FList [] Bool 类型的项(⊥ 除外) 。通过 FList 上的模式匹配，函数可以验证它是否被赋予了非⊥参数，并进一步确定它是否被传递了一个空类型列表。

Bar 的一个实例对于 FList s 必须分别处理 nil 列表和 cons 列表。 nil 列表有一个空的上下文。 cons 列表具有列表头部和尾部的组件。这是通过 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)