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

Question

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

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 中是否有类似的表示法？如果没有，这样的事情将如何完成？

编辑:这篇文章的灵感来自 by the Haskell wiki article on smart constructors , 其中类型类 InBounds被声明为静态验证传递给智能构造函数的幻像类型参数是否在 Nat 的某个范围内s，智能构造函数是:

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到值(value)级别的功能？

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 -pairs 是实例，只需要证明它们加起来为 8。这个证明你可以使用，但我怀疑 Haskell 仍然只是依赖类型的性质使得这项工作非常好。