基于类型级谓词的实例？
若要创建接受类型级自然值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的nats对创建实例。
在Haskell中有类似的符号吗？如果没有，这样的事情会如何实现呢？
编辑:这篇文章启发了Haskell wiki关于智能构造函数的文章，其中声明了一个类型类InBounds来静态地验证传递给智能构造函数的幻影类型参数是否在Nat的某个范围内，智能构造函数是：
resistor :: InBounds size => size -> Resistor size
resistor _ = Resistor在我的示例中尝试执行类似的操作(在使用了左方的答案之后)给了我一个错误：
construct :: (Type a b) => a -> b -> MyType a b
construct _ _ = MyType
>>> Expected a type, but a has kind Nat…Haskell的例子之所以有效，是因为它不使用DataKinds，是否有可能将一种类型的Nat传递给值级函数？
回答 2
Stack Overflow用户
发布于 2014-11-06 23:10:53
您需要使用的不是相等谓词，而是相等约束(这是在语言中编写的，使用-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仍然只是某种程度上依赖于类型化的特性才能使它真正发挥作用。
Stack Overflow用户
发布于 2014-11-07 09:22:17
您可以编写类型级别函数。
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)问题。
https://stackoverflow.com/questions/26790910
复制相似问题
腾讯云开发者
