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 代表主要权力。我还想使用qis 的类型列表来表示合数。我在想像：

data QList qi qs = QCons qi qs
                 | QNil

与数据

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

where(Head q)应该对应qi和(Tail q)应该对应qs。请注意，q参数 forFList不是（必然） a (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类型 wherec~Foo z和q~QCons q1 (QCons q2 QNil)，当然我的列表将满足每个级别的所有 BCtx 约束。

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

谢谢你的时间！

4

1 回答 1

2

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

使用DataKinds，类型列表是预定义的。它们有 kind [*]，但它们将在需要 kind 的上下文中使用*，因此需要一个运算符来转换它们：

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 来表达如何只能在某些 type-listFList的类型上构造 s 。例如，术语具有类型。另一方面，因为is 不是 形式，所以没有类型的项（⊥ 除外）。通过对 an 进行模式匹配，函数可以验证它是否被赋予了一个非⊥ 参数，并进一步确定它是否被传递给一个空类型列表。InjList q'q'FCons [True] FNilFList [] (InjList (Bool ': '[]))BoolInjList q'FList [] BoolFList

Barfor s的实例FList必须分别处理 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)
于 2013-01-10T06:03:07.877 回答