RankNTypes：什么导致这个错误？ [英] RankNTypes: What is causing this error?

问题描述

我刚刚在探索Rank2Types和RankNTypes以尝试熟悉它们。但我无法弄清为什么以下方法无效。

  g ::（forall a。forall b。a  - > b） - > x  - > y  - > （u，v）
gpxy =（px，py）
  

这个定义被编译器，但是当我尝试使用它时失败：

  ghci> g id 1 2 
 
< interactive>：35：3：
无法将类型'a'与'b'匹配
`a'是一个刚性类型变量bound由上下文预期的
a类型：a  - > b在< interactive>：35：1 
`b'是一个刚性类型变量，由
绑定，上下文期望类型：a  - > b在< interactive>：35：1 
预期类型：a  - > b 
实际类型：a  - > a 
在`g'的第一个参数中，即`id'
在表达式中：g id 1 2 
  

我很难理解为什么 a-> a 对于预期的 a->是不可接受的类型; b 。

解决方案

对于所有类型 a 和 b 类型为的函数forall a。 forall b。 a - > b 必须能够取得类型 a 的值并产生一个类型为 b 。因此，它必须能够放入 Int 并获得 String 。

如果您放入 id ，则无法获得字符串一个 Int - 你只会回到你输入的相同类型。所以 id 不是<$ code> forall a。 forall b。 a - > B'/ code>。事实上，如果没有类型类型约束，就不会有这个类型的总功能。

---

事实证明，您可以排序-sind-of使用ConstraintKinds做你想要的东西close（ish），但它不漂亮也不好用。

想法是参数化 g ，其中约束指定了需要满足哪些条件 x ， y ， u 和 v 以及 x 和 u 之间以及 y 和 v 需要。由于我们在所有情况下都不需要所有这些约束，因此我们还引入了两个虚拟类型类（一个用于个别参数的约束，另一个用于关系约束），以便我们可以在不需要约束的情况下将它们用作约束如果我们没有自己指定它，GHC是无法推断约束的）。

一些示例约束使得这个更加清晰：

• 如果我们传入 id 作为函数， x 必须等于 u 和 y 必须等于 v 。对于 x ， y ， u 或 v 。


• 如果我们传入 show ， x 和 y 必须是显示和 u 和 v 必须等于 String 。介于 x 和 u 或 y 和<$ c $之间c> v 。


• 如果我们传入读取。 show ， x 和 y 需要是的实例显示和 u 和 v 需要是的实例。如果我们有一个类型的类 Convert a b where convert :: a - > b ，我们传入 convert ，然后我们需要转换xu 和转换yv 并且不对各个参数设置约束。



所以这里是实现这个的代码： / b>

  { - ＃LANGUAGE Rank2Types，ConstraintKinds，FlexibleInstances，MultiParamTypeClasses＃ - } 
 
 class Dummy a 
实例Dummy a 
 
类Dummy2 ab 
实例Dummy2 ab 
 $ b $ :: forall c。 forall d。全部e。 forall x。你好。你好吗？所有v。
（c x，c y，d u，d v，e x u，e y v）=> （a，b，e，b）=> a→b）→b> x  - > y  - > （u，v）
gpxy =（px，py）
  

以下是如何使用它：

使用 show。阅读以在不同类型的数字之间进行转换：

 > （g ::（Show x，Show y，Read u，Read v，Dummy2 xu，Dummy2 yv）=>（全部a。全部b。（显示a，读取b，Dummy2 ab）=> a  - > （Double，Int）
（1.0,2）
  id ：
 
 
  $ b> 
 
 
 > （g ::（Dummy x，Dummy y，x〜u，y〜v）=>（forall a。forall b。（Dummy a，Dummy b，a〜b）=> a  - > b） - > x  - > y  - >（u，v））id 1 2.0 
（1,2.0）
  
使用 show ：
 > （g ::（Show x，Show y，String〜u，String〜v，Dummy2 xu，Dummy2 xy）=>（forall a.forall b。（Show a，String〜b，Dummy2 ab）=> a （u，v））显示1 2.0 
（1，2.0）
    - > x  - > y  - > / pre> 
 
 
正如您所看到的，这非常详细且不可读，因为您需要指定 g 每次使用它。如果没有这个，我不认为有可能让GHC正确地推断出约束条件（或者至少我不知道如何）。
I've just been exploring Rank2Types and RankNTypes to try to get familiar with them. But I can't work out why the following does not work.
g :: (forall a. forall b. a -> b) -> x -> y -> (u,v)
g p x y = (p x, p y)
This definition  is accepted by the compiler, but it fails when I try to use it:
ghci> g id 1 2

<interactive>:35:3:
    Couldn't match type `a' with `b'
      `a' is a rigid type variable bound by
          a type expected by the context: a -> b at <interactive>:35:1
      `b' is a rigid type variable bound by
          a type expected by the context: a -> b at <interactive>:35:1
    Expected type: a -> b
      Actual type: a -> a
    In the first argument of `g', namely `id'
    In the expression: g id 1 2
I'm struggling to understand why a->a is not acceptable type for the expected a->b.
解决方案
For all types a and b a function of type forall a. forall b. a -> b must be able to take a value of type a and produce a value of type b. So it must, for example, be possible to put in an Int and get out a String.

You can not get a String out of id if you put in an Int - you only ever get back the same type that you put in. So id is not of type forall a. forall b. a -> b. In fact there can be no total function of that type without typeclass constraints.



It turns out, you can sort-of-kind-of do something close(ish) to what you want using ConstraintKinds, but it's neither pretty to write nor pretty to use:

The idea is to parametrize g with constraints which specify which conditions need to be met by x, y, u and v and what the relationships between x and u and between y and v need to be. Since we don't need all those constraints in all cases, we also introduce two dummy typeclasses (one for constraints on individual parameters and one for the "relationship constraints), so that we can use those as the constraints where no constraints are needed (GHC is not able to infer constraints if we don't specify them ourselves).

Some example constraints to make this more clear:


If we pass in id as the function, x must be equal to u and y must be equal to v. There are no constraints on x, y, u or v individually.
If we pass in show, x and y must be instances of Show and u and v must be equal to String. There are no constraints on the relationship between x and u or y and v.
If we pass in read . show, x and y need to be instances of Show and u and v need to be instances of Read. Again no constraints on the relationships between them.
If we have a type class Convert a b where convert :: a -> b and we pass in convert, then we need Convert x u and Convert y v and no constraints on individual parameters.


So here's the code to implement this:
{-# LANGUAGE Rank2Types, ConstraintKinds, FlexibleInstances, MultiParamTypeClasses #-}

class Dummy a
instance Dummy a

class Dummy2 a b
instance Dummy2 a b

g :: forall c. forall d. forall e. forall x. forall y. forall u. forall v.
     (c x, c y, d u, d v, e x u, e y v) =>
     (forall a. forall b. (c a, d b, e a b) => a -> b) -> x -> y -> (u,v)
g p x y = (p x, p y)
And here's how to use it:

Using show . read to convert between different types of numbers:
> (g :: (Show x, Show y, Read u, Read v, Dummy2 x u, Dummy2 y v) => (forall a. forall b. (Show a, Read b, Dummy2 a b) => a -> b) -> x -> y -> (u,v)) (read . show) 1 2 :: (Double, Int)
(1.0,2)
Using id:
> (g :: (Dummy x, Dummy y, x~u, y~v) => (forall a. forall b. (Dummy a, Dummy b, a~b) => a -> b) -> x -> y -> (u,v)) id 1 2.0
(1,2.0)
Using show:
> (g :: (Show x, Show y, String~u, String~v, Dummy2 x u, Dummy2 x y) => (forall a. forall b. (Show a, String~b, Dummy2 a b) => a -> b) -> x -> y -> (u,v)) show 1 2.0
("1","2.0")
As you can see, this is horribly verbose and unreadable because you need to specify a signature for g every time you use it. Without this, I don't think it's possible to get GHC to correctly infer the constraints (or at least I don't know how).

                        
这篇关于RankNTypes：什么导致这个错误？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！