我可以参数化空的约束类型吗？ [英] Can I parameterise the empty constraint type?

问题描述

我有一个队列类，允许实例定义它放在元素上的约束。例如，优先级队列要求其元素是可订购的：

  { - ＃LANGUAGE MultiParamTypeClasses，ConstraintKinds，FunctionalDependencies＃ - } 
 
 class Queue qc | q  - > c其中
为空：q a 
 qpop :: c a => q a  - >也许（a，q a）
 qpush :: c a => a  - > q a  - > qa 
 
 data PriorityQueue a = ... 
 
实例队列PriorityQueue Ord其中
 ... 
  

这是一个魅力：在 PriorityQueue 的实例声明中，我可以使用队列的元素 Ord ，例如（>）。

---

我试图定义一个对它的元素没有要求的队列：\\ b

  newtype LIFO a = LIFO [a] 
 
实例队列LIFO（）其中
 empty = LIFO [] 
 qpop（LIFO []）= Nothing 
 qpop （LIFO（x：xs））= Just（x，LIFO xs）
 qpush x（LIFO xs）= LIFO $ x：xs 
  

这会失败，并从GHC收到以下错误消息：

 第二个参数`队列'应该有`*  - >约束'，
但是`（）'具有种类`*'
在`Queue LIFO（）'
  

的实例声明中，

这个错误信息对我有意义。 （code> Eq ）接受一个类型参数>（）没有参数 - 这是一个普通的旧类型不匹配。

---

在编写一个忽略其第二个参数的类型函数时会出现裂缝，这将允许我编写实例Queue LIFO（Const（））：

  { - ＃LANGUAGE TypeFamilies，KindSignatures，PolyKinds＃ - } 
 
类型系列Const ab :: k  - > k2  - > k 
类型实例Const ab = a 
  

我发现这种类型族和类型多态性非常漂亮，所以当它不起作用时我感到非常失望（我真的认为它会！）：

 期待更多'a'的参数
'Const'的第一个参数应该有`*'，
，但`a'有kind`k0  - > k1  - > k0'
在类型'a'中
在`Const'类型实例声明中
  

我有一种感觉，这个最后一个例子像一个语法错误是愚蠢的（我是新来的类型家庭）。我怎样才能写一个约束，它对它的参数没有任何限制？ div>

  class NoConstraint a其中
实例NoConstraint a其中
 
实例Queue LIFO NoConstraint其中
 ... 
  

上面定义了一个约束，它满足所有类型。因此，总是可以解除 c a 其中 c = NoConstraint 的义务。
另外，由于该类中没有成员，因此它应该具有零（或几乎为零）的运行时成本。

约束<$您试图使用的c $ c>（）不被视为由GHC设置的空约束，而是作为单位类型（）:: * 。这导致 Const（）:: k2 - > * ，这会触发类错误。

如果您不想使用自定义类，则可以尝试 Const（Eq（））或 Const（Num Int），它们有正确的类型 k2 - >约束。但我不推荐这样做，因为我发现它比使用自定义类更不可读。

（这需要启用一些扩展，正如Benjamin Hodgson在下面指出的那样评论。）

I have a class for queues which allows the instance to define the constraints it places on the elements. For example, a priority queue requires its elements to be orderable:

{-# LANGUAGE MultiParamTypeClasses, ConstraintKinds, FunctionalDependencies #-}

class Queue q c | q -> c where
    empty :: q a
    qpop :: c a => q a -> Maybe (a, q a)
    qpush :: c a => a -> q a -> q a

data PriorityQueue a = ...

instance Queue PriorityQueue Ord where
    ...

This works a charm: inside the instance declaration for PriorityQueue I can operate on elements of the queue using members of Ord such as (>).

---

I've got stuck trying to define a queue which places no requirements on its elements:

newtype LIFO a = LIFO [a]

instance Queue LIFO () where
    empty = LIFO []
    qpop (LIFO []) = Nothing
    qpop (LIFO (x:xs)) = Just (x, LIFO xs)
    qpush x (LIFO xs) = LIFO $ x:xs

This fails, with the following error message from GHC:

The second argument of `Queue' should have kind `* -> Constraint',
  but `()' has kind `*'
In the instance declaration for `Queue LIFO ()'

This error message makes sense to me. Eq accepts a type parameter (we typically write Eq a => ...) whereas () has no parameters - it's a plain old kind mismatch.

---

I had a crack at writing a type function which ignores its second argument, which would allow me to write instance Queue LIFO (Const ()):

{-# LANGUAGE TypeFamilies, KindSignatures, PolyKinds #-}

type family Const a b :: k -> k2 -> k
type instance Const a b = a

I find this interaction of type families and kind polymorphism quite beautiful, so I was rather disappointed when it didn't work (I really thought it would!):

Expecting two more arguments to `a'
The first argument of `Const' should have kind `*',
  but `a' has kind `k0 -> k1 -> k0'
In the type `a'
In the type instance declaration for `Const'

I have a feeling this last example is something stupid like a syntax mistake (I'm new to type families). How can I write a Constraint which doesn't place any restrictions on its argument?

解决方案

This should work:

class NoConstraint a where
instance NoConstraint a where

instance Queue LIFO NoConstraint where
  ...

The above defines a constraint which is satisfied by all types. As such, the obligations c a where c = NoConstraint can always be discharged. Also, since there are no members in that class, it should have zero (or nearly zero) run-time cost.

The "constraint" () you are trying to use is not seen as an empty constraint set by GHC, but as the unit type () :: *. This causes Const () :: k2 -> *, which triggers the kind error.

If you do not want to use a custom class, you might try e.g. Const (Eq ()) or Const (Num Int), which have the right kind k2 -> Constraint. I do not recommend this, though, since I find it less readable than using a custom class.

(This requires to enable some extensions, as Benjamin Hodgson points out below in a comment.)

这篇关于我可以参数化空的约束类型吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！