为什么在GHC Haskell中不存在本质上量化的类型变量 [英] Why aren't there existentially quantified type variables in GHC Haskell

问题描述

存在通用量化的类型变量，并且存在定量存在的数据类型.但是，尽管人们有时会提供exists a. Int -> a形式的伪代码来帮助解释概念，但似乎并没有真正感兴趣的编译器扩展.这仅仅是添加此内容没有太多价值"这类事情(因为它对我来说确实有价值)，或者是否存在诸如不确定性之类的问题，这使它真正变得不可能.

There are universally quantified type variables, and there are existentially quantified data types. However, despite that people give pseudocode of the form exists a. Int -> a to help explain concepts sometimes, it doesn't seem like a compiler extension that there's any real interest in. Is this just a "there isn't much value in adding this" kind of thing (because it does seem valuable to me), or is there a problem like undecidability that's makes it truly impossible.

我将viorior的回答标记为正确，因为似乎这可能是未包含此问题的实际原因.我想添加一些其他评论，以防万一有人想进一步澄清这一点.

I've marked viorior's answer as correct because it seems like it is probably the actual reason why this was not included. I'd like to add some additional commentary though just in case anyone would want to help clarify this more.

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

As requested in the comments, I'll give an example of why I would consider this useful. Suppose we have a data type as follows:

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

因此，我们选择参数化而不是a，这是一个命名约定(我知道在此示例中，为带有美国"first，middle，last"的适当数据构造函数的NamingConvention ADT可能更有意义，西班牙裔的姓名，父亲姓名，母亲姓名"等.但就目前而言，就使用此名称).

So we choose parameterize over a, which is a naming convention (I know that it probably makes more sense in this example to make a NamingConvention ADT with appropriate data constructors for the American "first,middle,last", the hispanic "name,paternal name,maternal name", etc. But for now, just go with this).

因此，我们看到一些函数基本上忽略了Person被参数化的类型.例子是

So, there are several functions we see that basically ignore the type that Person is parameterized over. Examples would be

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

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

And any function built on top of these could similarly ignore the a type. For example:

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

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

Now, if we have a heterogeneous list of people (of type [exists a. Person a]), we would like to be able to map some of our functions over the list. Of course, there are some useless ways to map:

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].但是，如果我们使用其他功能:

In this example, extractedNames is of course useless because it has type [exists a. a]. However, if we use our other functions:

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

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

现在，我们有一些有用的东西可以对异构集合进行操作(而且，我们甚至都没有涉及类型类).注意，我们能够重用我们现有的功能.使用现存数据类型将如下:

Now, we have something useful that operates over a heterogeneous collection (And, we didn't even involve typeclasses). Notice that we were able to reuse our existing functions. Using an existential data type would go as follows:

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

但是现在，我们如何使用age和atRiskForDiabetes?我们不能.我认为您将必须执行以下操作:

But now, how can we use age and atRiskForDiabetes? We can't. I think that you would have to do something like this:

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

这真的很la脚，因为您必须为新类型重写所有组合器.如果要使用在多个类型变量上参数化的数据类型来执行此操作，则情况甚至更糟.想象一下:

Which is really lame because you have to rewrite all of your combinators for a new type. It gets even worse if you want to do this with a data type that's parameterized over several type variables. Imagine this:

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

我将不再进一步解释这种思路，只是请注意，您将重写大量的组合器，以仅使用现有的数据类型来执行此类操作.

I won't explain this line of thought any further, but just notice that you'd be rewriting a lot of combinators to do anything like this using just existential data types.

话虽这么说，但我希望我能提出一个有说服力的用法，以证明这可能有用.如果它似乎没有用(或者该示例看起来太虚构)，请随时告诉我.另外，由于我首先是一名程序员，并且没有任何类型理论方面的培训，所以我很难在这里看到如何使用Skolem定理(由viorior发布).如果有人可以告诉我如何将其应用到我给出的Person a示例中，我将不胜感激.谢谢.

That being said, I hope I've give a mildly convincing use that this could be useful. If it doesn't seem useful (or if the example seems too contrived), feel free to let me know. Also, since I am firstly a programmer and have no training in type theory, it's a little difficult for me to see how to use Skolem's theorum (as posted by viorior) here. If anyone could show me how to apply it to the Person a example I gave, I would be very grateful. Thanks.

推荐答案

这是不必要的.

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

By Skolem's Theorem we could convert existential quantifier into universal quantifier with higher rank types:

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

等级n + 1的每个存在量化类型都可以编码为等级n的普遍量化类型

Every existentially quantified type of rank n+1 can be encoded as a universally quantified type of rank n

这篇关于为什么在GHC Haskell中不存在本质上量化的类型变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！