为什么在GHC Haskell中没有存在量化的类型变量

Question

存在普遍量化的类型变量,并且存在存在量化的数据类型.然而,尽管人们exists a. Int -> a有时会给出形式的伪代码以帮助解释概念,但它似乎并不像编译器扩展那样真正引起人们的兴趣.这只是"添加这种东西没什么价值"的东西(因为它对我来说确实很有价值),或者是否存在像不确定性这样的问题,这使得它真的变得不可能.

编辑:我已经将viorior的答案标记为正确,因为它似乎可能是为什么不包含这个问题的实际原因.我想补充一些额外的评论,以防万一有人想帮助澄清这一点.

根据评论中的要求,我将举例说明为什么我认为这有用.假设我们有一个数据类型如下:

data Person a = Person
  { age: Int
  , height: Double
  , weight: Int
  , name: a
  }

所以我们选择参数化a,这是一个命名约定(我知道在这个例子中,NamingConvention使用适当的数据构造函数为美国"第一,中间,最后",西班牙语"名称,父亲姓名,母亲的名字",等等.但是现在,就这样吧."

因此,我们看到有几个函数基本上忽略了Person参数化的类型.例子就是

age :: Person a -> Int
height :: Person a -> Double
weight :: Person a -> Int

在这些基础之上构建的任何函数都可以类似地忽略该a类型.例如:

atRiskForDiabetes :: Person a -> Bool
atRiskForDiabetes p = age p + weight p > 200
--Clearly, I am not actually a doctor

现在,如果我们有一个异类的人员列表(类型[exists a. Person a]),我们希望能够在列表中映射我们的一些功能.当然,有一些无用的方法来映射:

heteroList :: [exists a. Person a]
heteroList = [Person 20 30.0 170 "Bob Jones", Person 50 32.0 140 3451115332]
extractedNames = map name heteroList

在这个例子中,extractedNames当然没用,因为它有类型[exists a. a].但是,如果我们使用其他功能:

totalWeight :: [exists a. Person a] -> Int
totalWeight = sum . map age

numberAtRisk :: [exists a. Person a] -> Int
numberAtRisk = length . filter id . map atRiskForDiabetes

现在,我们有一些在异构集合上运行的有用的东西(而且,我们甚至没有涉及类型类).请注意,我们能够重用现有的功能.使用存在数据类型将如下所示:

data SomePerson = forall a. SomePerson (Person a) --fixed, thanks viorior

但是现在,我们如何使用age和atRiskForDiabetes？我们做不到.我认为你必须做这样的事情:

someAge :: SomePerson -> Int
someAge (SomePerson p) = age p

这真的很蹩脚,因为你必须为新类型重写所有组合器.如果要使用通过多个​​类型变量参数化的数据类型来执行此操作,情况会更糟.想象一下:

somewhatHeteroPipeList :: forall a b. [exists c d. Pipe a b c d]

我不会再进一步​​解释这一思路,但只要注意你将使用存在数据类型重写许多组合器来做这样的事情.

话虽如此,我希望我有一个有说服力的用法,这可能是有用的.如果它似乎没用(或者如果示例看起来太做作),请随时告诉我.另外,由于我是程序员,并且没有类型理论方面的训练,所以我在这里看到如何使用Skolem的theorum(由viorior发布)有点困难.如果有人能告诉我如何将它应用到Person a我给出的例子中,我将非常感激.谢谢.

Answer 1

这是不必要的.

通过Skolem的定理,我们可以将存在量词转换为具有更高等级类型的通用量词:

(?b. F(b)) -> Int   <===>  ?b. (F(b) -> Int)

每个存在量化类型的秩n + 1可以被编码为通用量化类型的秩n