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

【问题标题】：Type level predicate based instances?基于类型级别谓词的实例？
【发布时间】：2015-01-03 15:14:09
【问题描述】：

要创建一个接受类型级自然值 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，以静态验证传递给智能构造函数的幻像类型参数是否在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 传递给值级函数？

【问题讨论】：

标签： haskell types

【解决方案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例如，只需要一个 proof 他们加起来是 8。这个证明你可以使用，但我怀疑 Haskell 仍然只是 sort-of 依赖类型的性质使得这个工作得很好。

【讨论】：

感谢您的回答，但这并不完全适合我尝试做的事情，因此我更新了我的问题以包含更多上下文。
Wiki 上的那个例子以一种无用的方式使用幻像类型：你根本不需要resistor 的任何参数，只需将其设为resistor :: InBounds size => Resistor size、resistor = Resistor。如果您确实需要在参数中包含数据类型的值，请使用Tagged（我不是很喜欢，但有时它是正确的）。
将我的代码更改为 construct :: (Type a b) => MyType a b ,construct = MyType 仍然会出现同样的错误。
您没有在data MyType (a::Nat) (b::Nat) ... 中编写必要的类型签名——没有它们，GHC 假定MyType :: * -> * -> *，除非您设置-XPolyKinds（您可能应该这样做）。

【解决方案2】：

你可以写一个类型级别的函数

type family NatEq (a :: Nat) (b :: Nat) :: Bool
type instance NatEq 0 0 = True
...

然后

instance Type' (NatEq (a + b) 8) a b => Type a b
class Type' (x :: Bool) (a :: Nat) (b :: Nat) where ...
instance Type' True a b where ...
-- If you wanted a different behaviour otherwise:
-- instance Type' False a b where ...

当然，您需要启用一堆扩展。

如果a 和b 是常量，这可以正常工作，因此a+b 可以简化为8（或其他常量）。如果它们不是常数，不要指望 GHC 会为您证明方程。那就是（使用Int而不是Nat），不要指望Type x (8-x)会被解决。

【讨论】：