具有类型约束的Haskell类型系列实例 [英] Haskell type family instance with type constraints

问题描述

我试图用类型族来表示表达式，但我似乎无法弄清楚如何编写我想要的约束，而我开始觉得这是不可能的。这里是我的代码：

  class可评估的c其中
类型返回c :: * 
评估:: c  - >返回c 
 
数据否定n =否定n 
 
实例（可评估n，返回n〜Int）=>可评估的（Negate n）其中
类型Return（Negate n）=返回n 
评估（Negative n）=否定（评估n）
  

这一切都编译得很好，但它并不能完全表达我想要的内容。在 Negative >可评估的实例的约束中，我说<$ c $中的表达式的返回类型c> Negate 必须是 Int （带 Return n〜Int ），这样我可以称之为否定，但这太严格了。返回类型实际上只需要是 Num 类型的实例，它具有 negate 函数。这样 Double s，整数 s，或任何其他 Num 也可以被否定，而不仅仅是 Int s。但我不能只写
$ b $ pre $ 返回n〜Num


代替，因为 Num 是一个类型类，返回n 是一种类型。我也不能把

  Num（Return n）
  

而不是因为返回n 是一个类型而不是类型变量。

<我正试图用Haskell做什么？如果不是，应该是，还是我误解了它背后的一些理论？我觉得Java可以添加这样的约束。让我知道这个问题是否可以变得更清晰。

编辑：谢谢你们，这些回应正在帮助我们，并获得我怀疑的结果。看起来，类型检查器无法处理我想要做的事情，如果没有UndecidableInstances，所以我的问题是，我想表达的是真正不可判定的？这是对Haskell编译器的，但它是一般的吗？即可能存在一个约束，即检查返回n是否为Num的一个实例，这是可判定为更高级的类型检查器？

解决方案

  { - ＃LANGUAGE TypeFamilies，FlexibleContexts，UndecidableInstances＃ - } 
 
 class可评估的c，其中
类型返回c :: * 
评估:: c  - >返回c 
 
 data否定n =否定n 
 
实例（可评估n，Num（返回n））=>可评估的（Negate n）其中
类型Return（Negate n）=返回n 
评估（Negative n）=否定（评估n）
  

返回n 当然是一个类型，它可以是一个类的实例，就像 Int 可以。你的困惑可能是什么可以成为约束的论据。答案是任何正确的东西。 Int 的种类是 * ，就像 Return n 。 Num has kind * - >约束，因此类型 * 的任何东西都可以作为它的参数。以 Num（a :: *）相同的方式写 Num Int 作为约束是完全合法的$ c>是合法的。

I am trying to represent expressions with type families, but I cannot seem to figure out how to write the constraints that I want, and I'm starting to feel like it's just not possible. Here is my code:

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Return n ~ Int) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

This all compiles fine, but it doesn't express exactly what I want. In the constraints of the Negate instance of Evaluable, I say that the return type of the expression inside Negate must be an Int (with Return n ~ Int) so that I can call negate on it, but that is too restrictive. The return type actually only needs to be an instance of the Num type class which has the negate function. That way Doubles, Integers, or any other instance of Num could also be negated and not just Ints. But I can't just write

Return n ~ Num

instead because Num is a type class and Return n is a type. I also cannot put

Num (Return n)

instead because Return n is a type not a type variable.

Is what I'm trying to do even possible with Haskell? If not, should it be, or am I misunderstanding some theory behind it? I feel like Java could add a constraint like this. Let me know if this question could be clearer.

Edit: Thanks guys, the responses are helping and are getting at what I suspected. It appears that the type checker isn't able to handle what I'd like to do without UndecidableInstances, so my question is, is what I'd like to express really undecidable? It is to the Haskell compiler, but is it in general? i.e. could a constraint even exist that means "check that Return n is an instance of Num" which is decidable to a more advanced type checker?

解决方案

Actually, you can do exactly what you mentioned:

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-}

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Num (Return n)) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

Return n certainly is a type, which can be an instance of a class just like Int can. Your confusion might be about what can be the argument of a constraint. The answer is "anything with the correct kind". The kind of Int is *, as is the kind of Return n. Num has kind * -> Constraint, so anything of kind * can be its argument. It perfectly legal (though vacuous) to write Num Int as a constraint, in the same way that Num (a :: *) is legal.

这篇关于具有类型约束的Haskell类型系列实例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！