为什么不通过存在和约束进行子类型工作？

Question

我一直试图看看Haskell如何处理子类型,所以我想出了以下片段:

{-# LANGUAGE RankNTypes #-}

f1 :: () -> Int
f1 _ = 5

f2 :: () -> (forall a. Integral a => a)
f2 = f1

该行f2 = f1失败,出现意外错误消息:

Couldn't match type ‘a’ with ‘Int’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      f2 :: forall a. Integral a => () -> a

似乎存在主义已被提升为普遍存在,这当然是无意的.

我的猜测是,在实现中,术语f2需要返回一个值和一个相应的字典,而f1只返回一个类型的值Int.然而,从逻辑的角度来看,契约f2是"从一个()未知的实例到一个未知的实例Integral",f1并且完美地满足它.

GHC应该做一些隐含的魔术来使其发挥作用还是我错过了什么？

Answer 1

a您拥有的类型f2是普遍量化的,而不是存在量化的.GHC并不直接支持您正在寻找的存在类型.

但是,您可以通过将其包装在新数据类型中来获得类似的内容:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds           #-}

data Constrained c = forall a. c a => Constrained a

f1 :: () -> Int
f1 _ = 5

f2 :: () -> Constrained Integral
f2 unit = Constrained (f1 unit)

现在,这通常不是非常有用,因为所有已经完成的是我们抛弃了所有(类型)信息,f2 ()除了它的类型是一个实例Integral.你不再知道它了Int.也可以跟踪这些信息,但根据您正在做的事情,这可能有用也可能没用.

更多关于你正在做什么以及你希望看到什么的背景会让我更容易获得关于我应该添加的那些事情的信息.

作为旁注:没有必要将它们变成带参数的函数.你可以拥有f1 :: Int和f2 :: Constrained Integral.

另外,如果我没有提到这一点,我会觉得有点疏忽,尽管在这个答案的早些时候在Haskell中淡化了这些类型的实用程序,我写了一个答案,描述了约束存在类型的一些潜在的实际用途.虽然我们对ConstraintKinds某个主题有所了解,但也许值得指出的是,这是一个强大的扩展,它的使用超出了受限制的存在.

Answer 2

你正在阅读f2错误的方式.

f2所说的类型"如果你给我一个(),我会给你一个(forall a. Integral a => a).也就是说,f2承诺给你一个可以用作任何类型的成员的价值Integral.

然而,实施f2说它将通过简单的调用实现这一目标f1.但f1只返回Int!这确实是一个成员Integral,但它不能作为任何类型的成员使用Integral.

实际上,类型f1实际上是类型的子f2类型,而不是相反!这实际上有效:

{-# LANGUAGE RankNTypes #-}

f1 :: () -> Int
f1 = f2

f2 :: () -> (forall a. Integral a => a)
f2 _ = 5

它的工作原理是因为数字文字是多态的,所以a 5可以是任何Num类型(并且Num是超类Integral,所以如果它可以是任何类型,Num它也可以是任何类型Integral).f1然后调用f2请求Int作为选择a.

您注意到GHC似乎正在转换您写的类型f2 :: forall a. Integral a => () -> a,而您是对的; 它不会真的规范化你所写的那种类型.原因是这两种类型实际上与GHC类型系统的工作方式相同.调用者实例化在整个类型上量化的任何类型变量f2,调用者也将是接收返回值的那个,因此实例化仅在返回值上量化的任何类型变量.forall如果您在整个类型上或仅仅在函数的返回类型上进行范围调整,则引入类型变量是相同的; 如果它的范围是箭头的左侧(这是更高级别的类型进入的地方),它只会产生影响.