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

2018-06-15 07:21:08

有普遍量化的类型变量，并且有存在量化的数据类型。但是，尽管人们给出了伪代码的形式exists a. Int -> a exists a. Int -> a有时可以帮助解释概念，它似乎并不像编译器扩展那样有真正的兴趣。这仅仅是“添加这种类型的东西没有多大价值”（因为它看起来很有价值对我来说），还是有一个问题，如不可判定性，这使得它是不可能的。

编辑：我已经标记viorior的答案是正确的，因为它似乎可能是为什么这不包括在内的实际原因。我想添加一些额外的评论，以防万一有人想帮助澄清这一点。

根据评论的要求，我会举例说明为什么我会认为这很有用。假设我们有一个数据类型如下：

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

因此，我们选择参数化为a ，这是一个命名约定（我知道在这个例子中，为美国“第一，中间，最后一个”，“西班牙裔”名称，父亲制作一个适当的数据构造函数的NamingConvention ADT可能更有意义姓名，母亲名字“等等，但现在，就这样吧）。

所以，我们看到几个函数基本上忽略了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] [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的理论（由viorior发布）有点困难。如果有人能告诉我如何将它应用到Person a给我Person a例子，我会非常感激。谢谢。

这是没有必要的。

通过斯科勒姆定理，我们可以将存在量词转换为具有更高排列类型的普遍量词：

(∃b. F(b)) -> Int   <===>  ∀b. (F(b) -> Int)

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

GHC提供存在量化的类型，所以这个问题是基于一个错误的假设。

链接地址: http://www.djcxy.com/p/43447.html

上一篇: Why aren't there existentially quantified type variables in GHC Haskell

下一篇: Existential vs. Universally quantified types in Haskell