存在主义是如何存在的?

对于存在量化，数据定义中的foralls意味着 即，所包含的值可以是任何合适的类型，而不是 它必须是所有合适的类型。 ——yachiru的回答

为什么forall在数据定义是同构的(存在a. a)(伪Haskell)可以在wikibooks的“Haskell/存在量化类型”中找到解释。

以下是简要的逐字摘要:

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

当模式匹配/解构MkT x时，x的类型是什么?

foo (MkT x) = ... -- -- what is the type of x?

X可以是任何类型(如forall中所述)，因此它的类型是:

x :: exists a. a -- (pseudo-Haskell)

因此，以下是同构的:

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

福拉尔意味着福拉尔

我对这一切的简单解释是，“forall”实际上意味着“为所有人”。 一个重要的区别是forall对定义和函数应用程序的影响。

forall意味着值或函数的定义必须是多态的。

如果被定义的东西是一个多态值，那么它意味着该值必须对所有合适的a有效，这是非常严格的。

如果被定义的是一个多态函数，那么它意味着这个函数必须对所有合适的a都有效，这并不是限制性的，因为仅仅因为函数是多态的并不意味着应用的参数必须是多态的。也就是说，如果函数对所有a都有效，那么反过来，任何合适的a都可以应用于该函数。但是，在函数定义中，参数的类型只能选择一次。

如果forall在函数参数的类型中(即Rank2Type)，那么它意味着应用的参数必须是真正多态的，与forall的思想一致，意味着定义是多态的。在这种情况下，在函数定义中可以多次选择形参的类型(正如Norman所指出的，“并且由函数的实现选择”)。

因此，存在数据定义允许任何a的原因是因为数据构造函数是一个多态函数:

MkT :: forall a. a -> T

kind of MkT:: a -> *

这意味着任何a都可以作用于这个函数。与之相反的是，例如，一个多态值:

valueT :: forall a. [a]

类型值et:: a

这意味着valueT的定义必须是多态的。在这种情况下，valueT可以定义为所有类型的空列表[]。

[] :: [t]

差异

尽管在ExistentialQuantification和RankNType中forall的含义是一致的，但existentials有区别，因为数据构造函数可以用于模式匹配。如ghc用户指南中所述:

当进行模式匹配时，每个模式匹配都会为每个存在类型变量引入一个新的、不同的类型。这些类型不能与任何其他类型统一，也不能逃脱模式匹配的范围。

这个关键字之所以有不同的用法，是因为它实际上至少在两种不同的类型系统扩展中使用:高级类型和存在型。

最好是分别阅读和理解这两件事，而不是试图解释为什么'forall'同时在这两件事上都是合适的语法。

存在主义是如何存在的?

对于存在量化，数据定义中的foralls意味着 即，所包含的值可以是任何合适的类型，而不是 它必须是所有合适的类型。 ——yachiru的回答

为什么forall在数据定义是同构的(存在a. a)(伪Haskell)可以在wikibooks的“Haskell/存在量化类型”中找到解释。

以下是简要的逐字摘要:

data T = forall a. MkT a -- an existential datatype
MkT :: forall a. a -> T -- the type of the existential constructor

当模式匹配/解构MkT x时，x的类型是什么?

foo (MkT x) = ... -- -- what is the type of x?

X可以是任何类型(如forall中所述)，因此它的类型是:

x :: exists a. a -- (pseudo-Haskell)

因此，以下是同构的:

data T = forall a. MkT a -- an existential datatype
data T = MkT (exists a. a) -- (pseudo-Haskell)

福拉尔意味着福拉尔

我对这一切的简单解释是，“forall”实际上意味着“为所有人”。 一个重要的区别是forall对定义和函数应用程序的影响。

forall意味着值或函数的定义必须是多态的。

如果被定义的东西是一个多态值，那么它意味着该值必须对所有合适的a有效，这是非常严格的。

如果被定义的是一个多态函数，那么它意味着这个函数必须对所有合适的a都有效，这并不是限制性的，因为仅仅因为函数是多态的并不意味着应用的参数必须是多态的。也就是说，如果函数对所有a都有效，那么反过来，任何合适的a都可以应用于该函数。但是，在函数定义中，参数的类型只能选择一次。

如果forall在函数参数的类型中(即Rank2Type)，那么它意味着应用的参数必须是真正多态的，与forall的思想一致，意味着定义是多态的。在这种情况下，在函数定义中可以多次选择形参的类型(正如Norman所指出的，“并且由函数的实现选择”)。

因此，存在数据定义允许任何a的原因是因为数据构造函数是一个多态函数:

MkT :: forall a. a -> T

kind of MkT:: a -> *

这意味着任何a都可以作用于这个函数。与之相反的是，例如，一个多态值:

valueT :: forall a. [a]

类型值et:: a

这意味着valueT的定义必须是多态的。在这种情况下，valueT可以定义为所有类型的空列表[]。

[] :: [t]

差异

尽管在ExistentialQuantification和RankNType中forall的含义是一致的，但existentials有区别，因为数据构造函数可以用于模式匹配。如ghc用户指南中所述:

当进行模式匹配时，每个模式匹配都会为每个存在类型变量引入一个新的、不同的类型。这些类型不能与任何其他类型统一，也不能逃脱模式匹配的范围。

它们密密麻麻地塞满了假设，即我已经阅读了本周最流行的离散数学、范畴理论或抽象代数的任何分支的最新研究成果。(如果我再也没有读过“关于实施细节，无论如何，请查阅报纸”这句话，那就为时过早了。)

那么简单的一阶逻辑呢?Forall很明显是指普遍量化，在这种情况下，术语存在主义也更有意义，尽管如果有一个存在关键字就不那么尴尬了。量化是普遍的还是存在的取决于量词相对于变量在函数箭头的哪一边使用的位置，这有点令人困惑。

因此，如果这没有帮助，或者如果您只是不喜欢符号逻辑，从更函数式编程的角度来看，您可以将类型变量视为函数的(隐式)类型参数。在这种意义上，接受类型参数的函数通常使用大写lambda来编写，不管出于什么原因，我将其写成/\。

所以，考虑id函数:

id :: forall a. a -> a
id x = x

我们可以将其重写为lambdas，将“type parameter”移出类型签名，并添加内联类型注释:

id = /\a -> (\x -> x) :: a -> a

这是对const做的同样的事情:

const = /\a b -> (\x y -> x) :: a -> b -> a

所以你的杆函数可能是这样的

bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)

注意，作为参数赋给bar的函数类型取决于bar的类型形参。考虑一下如果你有这样的东西:

bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)

这里bar2将函数应用于Char类型的对象，因此给bar2除Char以外的任何类型参数都会导致类型错误。

另一方面，下面是foo的样子:

foo = (\f -> (f Char 't', f Bool True))

与bar不同，foo实际上根本不接受任何类型参数!它接受一个自身接受类型形参的函数，然后将该函数应用于两个不同的类型。

因此，当你在类型签名中看到forall时，就把它看作是类型签名的lambda表达式。就像正则lambda一样，forall的作用域尽可能向右扩展，一直延伸到圆括号，就像正则lambda中绑定的变量一样，由forall绑定的类型变量仅在量化表达式的作用域内。

---

Post scriptum:也许您会想——既然我们正在考虑函数接受类型参数，为什么我们不能对这些参数做一些更有趣的事情，而不是将它们放入类型签名中呢?答案是我们可以!

将类型变量与标签放在一起并返回新类型的函数是类型构造函数，你可以这样写:

Either = /\a b -> ...

但我们需要全新的符号，因为这种类型的书写方式，比如Either a b，已经暗示了“将函数Either应用于这些参数”。

另一方面，在类型参数上进行“模式匹配”，为不同类型返回不同值的函数是类型类的方法。稍微扩展一下上面的/\语法，就像这样:

fmap = /\ f a b -> case f of
    Maybe -> (\g x -> case x of
        Just y -> Just b g y
        Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
    [] -> (\g x -> case x of
        (y:ys) -> g y : fmap [] a b g ys 
        []     -> [] b) :: (a -> b) -> [a] -> [b]

就我个人而言，我更喜欢Haskell的实际语法……

“模式匹配”其类型参数并返回任意现有类型的函数是类型族或函数依赖项——在前一种情况下，它甚至看起来已经非常像函数定义了。

有谁能用清楚明了的英语完全解释forall关键字吗?

不。(嗯，也许唐·斯图尔特(Don Stewart)可以。)

以下是一个简单明了的解释或所有解释的障碍:

It's a quantifier. You have a to have at least a little logic (predicate calculus) to have seen a universal or existential quantifier. If you've never seen predicate calculus or are not comfortable with quantifiers (and I have seen students during PhD qualifying exams who are not comfortable), then for you, there's no easy explanation of forall. It's a type quantifier. If you haven't seen System F and gotten some practice writing polymorphic types, you're going to find forall confusing. Experience with Haskell or ML is not enough, because normally these languages omit the forall from polymorphic types. (In my mind, this is a language-design mistake.) In Haskell in particular, forall is used in ways that I find confusing. (I'm not a type theorist, but my work brings me in contact with a lot of type theory, and I'm quite comfortable with it.) For me, the main source of confusion is that forall is used to encode a type that I myself would prefer to write with exists. It's justified by a tricky bit of type isomorphism involving quantifiers and arrows, and every time I want to understand it, I have to look things up and work out the isomorphism myself. If you are not comfortable with the idea of type isomorphism, or if you don't have any practice thinking about type isomorphisms, this use of forall is going to stymie you. While the general concept of forall is always the same (binding to introduce a type variable), the details of different uses can vary significantly. Informal English is not a very good tool for explaining the variations. To really understand what's going on, you need some mathematics. In this case the relevant mathematics can be found in Benjamin Pierce's introductory text Types and Programming Languages, which is a very good book.

至于你的具体例子，

runST should make your head hurt. Higher-rank types (forall to the left of an arrow) are rarely found in the wild. I encourage you to read the paper that introduced runST: "Lazy Functional State Threads". This is a really good paper, and it will give you a much better intuition for the type of runST in particular and for higher-rank types in general. The explanation take several pages, it's very well done, and I'm not going to try to condense it here. Consider foo :: (forall a. a -> a) -> (Char,Bool) bar :: forall a. ((a -> a) -> (Char, Bool)) If I call bar, I can simply pick any type a that I like, and I can pass it a function from type a to type a. For example, I can pass the function (+1) or the function reverse. You can think of the forall as saying "I get to pick the type now". (The technical word for picking the type is instantiating.) The restrictions on calling foo are much more stringent: the argument to foo must be a polymorphic function. With that type, the only functions I can pass to foo are id or a function that always diverges or errors, like undefined. The reason is that with foo, the forall is to the left of the arrow, so as the caller of foo I don't get to pick what a is—rather it's the implementation of foo that gets to pick what a is. Because forall is to the left of the arrow, rather than above the arrow as in bar, the instantiation takes place in the body of the function rather than at the call site.

摘要:forall关键字的完整解释需要数学，并且只有研究过数学的人才能理解。如果没有数学，即使是部分的解释也很难理解。但也许我的片面的、非数学的解释有一点帮助。去runST上看Launchbury和Peyton Jones吧!

---

补充:行话“在上面”，“在下面”，“在左边”。这些与编写类型的文本方式无关，而是与抽象语法树有关。在抽象语法中，forall接受类型变量的名称，然后在forall“下面”有一个完整类型。箭头有两种类型(参数和结果类型)，并形成一个新类型(函数类型)。参数类型是“箭头左边”;它是抽象语法树中箭头的左子元素。

例子:

In all总之;[a] -> [a]， forall在箭头上方;箭头左边的是[a]。 在 对于所有n f x。(forall e x。n e x -> f ->事实x f) -> Block n e x -> f ->事实x f 括号中的类型被称为“箭头左边的a forall”。(我在我正在工作的优化器中使用这样的类型。)

让我们从一个代码示例开始:

foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
    postProcess val
    where
        val :: b
        val = maybe onNothin onJust mval

这段代码不能在普通Haskell 98中编译(语法错误)。它需要一个扩展来支持forall关键字。

基本上，forall关键字有3种不同的常用用法(至少看起来是这样)，每一种都有自己的Haskell扩展:ScopedTypeVariables, RankNTypes/Rank2Types, ExistentialQuantification。

上面的代码在启用这两种情况下都不会出现语法错误，而只在启用ScopedTypeVariables时进行类型检查。

作用域类型变量:

限定作用域的类型变量有助于在where子句中为代码指定类型。它使得val:: b中的b与foob:: forall中的b相同。(b -> b) -> b -> (a -> b) ->也许是a -> b。

令人困惑的一点是:当你从一个类型中省略forall时，它实际上仍然隐式存在。(来自Norman的回答:“通常这些语言会从多态类型中省略forall”)。这个声明是正确的，但它指的是forall的其他用法，而不是ScopedTypeVariables的用法。

Rank-N-Types:

让我们从mayb:: b -> (a -> b) ->也许a -> b等价于mayb:: forall ab b -> (a -> b) ->也许a -> b，除非ScopedTypeVariables被启用。

这意味着它对所有a和b都成立。

假设你想做这样的事情。

ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])

这个电梯一定是什么类型的?它是liftTup::(forall x.x -> f x) -> (a, b) -> (f a, f b)。为了看看为什么，让我们试着编码它:

ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
    No instance for (Num [Char])
    ...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)

“嗯. .为什么GHC推断元组必须包含两个相同类型的元组?让我们告诉它，它们不需要

-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

ghci> :l test.hs
    Couldnt match expected type 'x' against inferred type 'b'
    ...

嗯。所以这里GHC不让我们在v上应用liftFunc，因为v:: b和liftFunc想要一个x。我们真的希望我们的函数得到一个接受任何可能的x的函数!

{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

所以不是liftTup对所有x都有效，而是它得到的函数起作用。

存在量化:

让我们举个例子:

-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x

ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2

这和Rank-N-Types有什么不同?

ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
    Couldnt match expected type 'a' against inferred type '[Char]'
    ...

对于Rank-N-Types, forall a意味着你的表达式必须适合所有可能的。例如:

ghci> length ([] :: forall a. [a])
0

空列表可以作为任何类型的列表。

因此，对于存在量化，数据定义中的foralls意味着，所包含的值可以是任何合适的类型，而不是必须是所有合适的类型。