基于类型级别谓词的实例？

Question

要创建一个接受类型级自然Z,(SZ),(S(SZ))...等的类型类,您可以简单地递归声明实例:

data Z
data S a

class Type a

instance Type Z
instance Type (S a)

是否可以基于类型级谓词创建类型类实例？例如,我希望能够说:

{-# LANGUAGE MultiParamTypeClasses #-}
class Type a b
instance Type x y when (x :+: y == 8)

:+:类型级别添加在哪里,并且==是类型级别相等Data.Type.Equality,因此仅为最多为8的nat对创建实例.

Haskell中的符号是否与此类似？如果没有,这样的事情将如何实现？

编辑:这篇文章的灵感来自关于智能构造函数的Haskell wiki文章,其中InBounds声明了一个类型类以静态验证传递给智能构造函数的幻像类型参数是在某些范围的Nats中,智能构造函数是:

resistor :: InBounds size => size -> Resistor size
resistor _ = Resistor

在我的例子中尝试做类似的事情(在使用leftaroundabout的答案之后)给了我一个错误:

construct :: (Type a b) => a -> b -> MyType a b
construct _ _ = MyType

>>> Expected a type, but a has kind Nat…

来自Haskell wiki的示例可以工作,因为它不使用DataKinds,是否可以将类型类型传递Nat给值级函数？

Answer 1

您不需要使用等式谓词,而是使用等式约束(将其括在语言中,启用-XGADTs).

{-# LANGUAGE KindSignatures, DataKinds, MultiParamTypeClasses, FlexibleInstances, GADTs #-}

import GHC.TypeLits

class Type (a :: Nat) (b :: Nat)

instance (a + b) ~ 8 => Type a b

请注意,这不一定像它看起来那样有用 - 等式约束不会以某种方式枚举所有组合,最多可以添加8,而是它允许所有组成Nat为实例,只需要一个证明它们加起来8.你可以使用这个证明,但我怀疑Haskell仍然只是一种独立的类型性质使得这项工作非常好.