6

我想表达一个Constraint关于 kind 的类型k -> k -> Type，用英语可以表述为：

一种类型s，使得, forall x x', y, and y'where Coercible x x'and Coercible y y',Coercible (s x y) (s x' y')

或者用更简单的英语：

如果它的两个参数是可强制的，则该类型s始终是可强制的。

后者似乎已经非常接近haskell，而且我有一些看起来确实应该这样做的代码：

type Representational2 (s :: k -> k -> Type) =
  forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y')

然而这不起作用，ghc 想Coercible (s x y) (s x' y')成为一个类型，但它是一个Constraint（ConstraintKinds并且QuantifiedConstraints在）。

• Expected a type, but
  ‘Coercible (s x y) (s x' y')’ has kind
  ‘Constraint’
• In the type ‘forall x x' y y'.
               (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y')’
  In the type declaration for ‘Representational2’

我不完全理解发生了什么，但我认为 ghc 不喜欢 aConstraint右侧的=>存在type。由于我可以使用 kind 创建类型别名，Constraint并且可以使用 创建type别名=>，所以没问题。

问题是什么，我如何以它接受的方式向 ghc 表达这种约束？

4

1 回答 1

6

这有效：

{-# LANGUAGE ConstraintKinds, PolyKinds, RankNTypes, QuantifiedConstraints #-}

import Data.Kind
import Data.Coerce

type Representational2 (s :: k -> k -> Type) =
  forall x x' y y'. (Coercible x x', Coercible y y') => Coercible (s x y) (s x' y') :: Constraint

我所做的只是添加:: Constraint到您的类型中。由于 GHC 已经知道 RHS 的类型Constraint（由于错误消息），我真的没有很好的解释为什么它可以工作。

编辑：我有一个部分解释：通过向 RHS 添加那种签名，您的类型同义词现在有一个 CUSK（请参阅GHC wiki）：

  • 当且仅当它的所有类型变量和它的 RHS 都用种类注释时，类型同义词才有 CUSK。
于 2020-02-26T04:08:04.020 回答