JUS*_*ION 295 syntax haskell types ghc forall
我开始理解forall关键字如何在所谓的"存在类型"中使用,如下所示:
data ShowBox = forall s. Show s => SB s
然而,这仅仅是如何forall使用的一个子集,我根本无法将其用于这样的事情:
runST :: forall a. (forall s. ST s a) -> a
或解释为什么这些是不同的:
foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))
或整个RankNTypes东西......
我倾向于选择清晰,无术语的英语而不是学术环境中常见的语言.我尝试阅读的大部分解释(我可以通过搜索引擎找到的解释)存在以下问题:
runST,foo和bar以上).所以...
关于实际问题.任何人都可以完全解释的forall清晰,简单的英语关键字(或者,如果它存在于某个地方,点到我已经错过了这样一个明确的解释),不承担我在行话悠久的数学家？
编辑添加:
下面有高质量的答案有两个突出的答案,但不幸的是我只能选择一个最好的答案. 诺曼的回答很详细的和有用的,解释的方式,表现出一定的理论基础的东西forall,并在同一时间向我展示了一些它的实际影响. yairchu的回答覆盖了其他人没有提到的范围(范围类型变量),并用代码和GHCi会话说明了所有概念.我愿意选择两者是最好的.不幸的是,我不能和上,俯瞰着两个答案后密切,我已经决定,yairchu的稍微挤掉了诺曼,因为说明性代码和附加的说明.这是一个有点不公平,但是,因为我真的需要这两个答案,了解这一点是一点forall没给我留下了恐惧的隐隐感觉,当我看到它在类型签名.
yai*_*chu 253
让我们从代码示例开始:
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关键字.
基本上,关键字有3 种不同的常见用法forall(或者至少看起来如此),并且每种用途都有自己的Haskell扩展名:ScopedTypeVariables,RankNTypes/ Rank2Types, ExistentialQuantification.
上面的代码没有启用任何一个语法错误,但只有启用的类型检查ScopedTypeVariables.
范围类型变量:
Scoped类型变量有助于为where子句中的代码指定类型.这使得b在val :: b同样的一个作为b的foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b.
令人困惑的一点:你可能会听到,当你forall从一个类型中省略它时,它实际上仍然隐含在那里.(来自Norman的回答:"通常这些语言省略了多态类型的概念").这种说法是正确的,但它指的是其他用途forall,而不是ScopedTypeVariables用途.
排名-N-类型:
让我们先从这mayb :: b -> (a -> b) -> Maybe a -> b相当于mayb :: forall a b. b -> (a -> b) -> Maybe a -> b,除了因为当ScopedTypeVariables被启用.
这意味着,它适用于所有的a和b.
假设您想要做这样的事情.
ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])
这个类型必须是什么liftTup？是的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没有让我们应用liftFunc上v,因为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意味着您的表达式必须适合所有可能的as.例如:
ghci> length ([] :: forall a. [a])
0
空列表可以作为任何类型的列表.
因此,对于存在量化,定义中的foralls data意味着所包含的值可以是任何合适的类型,而不是它必须是所有合适的类型.
Nor*_*sey 115
任何人都可以用清晰,简单的英语完整地解释forall关键字吗？
没有.(好吧,也许Don Stewart可以.)
以下是一个简单明了的解释或forall:
这是一个量词.你必须至少有一点逻辑(谓词演算)才能看到一个普遍的或存在的量词.如果你从未见过谓词演算或对量词不满意(我在博士资格考试中看到学生不舒服),那么对你来说,没有简单的解释forall.
这是一种类型量词.如果你还没有看过System F并且已经开始编写多态类型的练习,那么你会发现forall令人困惑.使用Haskell或ML的经验是不够的,因为通常这些语言省略了forall多态类型.(在我看来,这是一个语言设计错误.)
特别forall是在Haskell中,使用方式让我感到困惑.(我不是一个类型理论家,但是我的工作让我接触了很多类型理论,而且我对它很满意.)对我来说,混淆的主要原因forall是用于编码一种类型的我本人更愿意写作exists.这是一个涉及量词和箭头的类型同构类型的合理证明,每当我想要理解它时,我必须自己查找并解决同构现象.
如果你对类型同构的想法不满意,或者如果你没有任何关于类型同构的思考,那么这种使用forall会阻碍你.
虽然一般概念forall总是相同的(绑定引入类型变量),但不同用途的细节可能会有很大差异.非正式英语不是解释变化的非常好的工具.要真正了解正在发生的事情,你需要一些数学知识.在这种情况下,相关的数学可以在Benjamin Pierce的介绍性文本" 类型和编程语言"中找到,这是一本非常好的书.
至于你的具体例子,
runST 应该让你的头受伤.在野外很少发现较高级别的类型(箭头左侧的forall).我鼓励你阅读引入的文章runST:"懒惰的功能状态线程".这是一篇非常好的论文,它将为您提供更好的直觉runST,特别是对于更高级别的类型.这个解释需要几页,它做得很好,我不打算在这里压缩它.
考虑
foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))
如果我打电话bar,我可以简单地选择a我喜欢的任何类型,并且我可以从类型a到类型传递函数a.例如,我可以传递函数(+1)或函数reverse.你可以想到forall"我现在就选择这种类型".(选择类型的技术词是实例化.)
对调用的限制foo要严格得多:参数foo 必须是多态函数.对于那种类型,我可以传递给的唯一函数foo是id一个总是发散或错误的函数,比如undefined.其原因是,与foo,则forall是箭头的左侧,这样的调用foo我不明白选择什么样a的,而它的实现的foo是得到选择什么样a的.因为forall在箭头的左侧,而不是在箭头的上方bar,实例化发生在函数的主体中而不是在调用站点.
摘要:一个完整的解释forall关键字需要数学,只能由人谁研究数学来理解.没有数学,即使是部分解释也很难理解.但也许我的部分非数学解释有点帮助.去阅读Launchbury和Peyton Jones runST吧!
附录:术语"上方","下方","左侧".这些与编写类型的文本方式无关,而与抽象语法树有关.在抽象语法中,a forall采用类型变量的名称,然后在forall下面有一个完整类型.箭头采用两种类型(参数和结果类型)并形成一种新类型(函数类型).参数类型是"箭头左侧"; 它是抽象语法树中箭头的左子项.
例子:
在forall a . [a] -> [a],箭头在箭头上方; 箭头左边的是什么[a].
在
forall n f e x . (forall e x . n e x -> f -> Fact x f)
-> Block n e x -> f -> Fact x f
括号中的类型将被称为"箭头左侧的一个字母".(我在我正在使用的优化器中使用这样的类型.)
Don*_*art 50
我的原始答案:
任何人都可以用清晰,简单的英语完整地解释forall关键字
正如诺曼所指出的那样,很难从类型理论中对技术术语进行清晰,简单的英语解释.我们都在尝试.
关于'forall'只有一件事需要记住:它将类型绑定到某个范围.一旦你理解了,一切都相当容易.它相当于类型级别的'lambda'(或'let'形式) - Norman Ramsey使用"left"/"above"的概念在他出色的答案中传达了相同的范围概念.
'forall'的大多数用法非常简单,你可以在GHC用户手册S7.8中找到它们,特别是在 'forall'的嵌套形式上的优秀S7.8.5.
在Haskell中,当类型被普遍定量化时,我们通常会忽略类型的绑定器,如下所示:
length :: forall a. [a] -> Int
相当于:
length :: [a] -> Int
而已.
由于您现在可以将类型变量绑定到某个范围,因此您可以使用除顶级以外的范围(" 通用量化 "),就像您的第一个示例一样,其中类型变量仅在数据结构中可见.这允许隐藏类型(" 存在类型 ").或者我们可以任意嵌套绑定("排名N类型").
要深入理解类型系统,您需要学习一些术语.这就是计算机科学的本质.但是,如上所述,简单的用法应该能够通过类似于价值水平的'let'来直观地理解.Launchbury和Peyton Jones是一个很好的介绍.
C. *_*ann 30
他们密集地充满了假设,我已经阅读了最新的离散数学分类,类别理论或抽象代数本周流行.(如果我再也没有读过"请参阅论文的任何细节",那就太早了.)
呃,简单的一阶逻辑呢？forall非常清楚地提到了通用量化,在这种情况下,存在性这个术语也更有意义,尽管如果有exists关键词则不那么尴尬.量化是有效的通用还是存在取决于量词相对于函数箭头哪一侧使用变量的位置,这有点令人困惑.
因此,如果这没有帮助,或者如果您不喜欢符号逻辑,那么从更具功能性的编程角度来看,您可以将类型变量视为函数的(隐式)类型参数.在这种意义上采用类型参数的函数传统上是出于任何原因使用大写lambda编写的,我将在此处写为/\.
所以,考虑一下这个id功能:
id :: forall a. a -> a
id x = x
我们可以将它重写为lambda,将"类型参数"移出类型签名并添加内联类型注释:
id = /\a -> (\x -> x) :: a -> a
这是做同样的事情const:
const = /\a b -> (\x y -> x) :: a -> b -> a
所以你的bar功能可能是这样的:
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在类型签名中看到a 时,只需将其视为类型签名的lambda表达式.就像常规lambdas一样,范围forall尽可能向右扩展,直到括号括起来,就像绑定在常规lambda中的变量一样,由a绑定的类型变量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的实际语法......
"模式匹配"其类型参数并返回任意现有类型的函数是类型族或函数依赖项 - 在前一种情况下,它甚至已经看起来像函数定义一样.
Apo*_*isp 26
这是一个简单明了的快速而肮脏的解释,你可能已经熟悉了.
该forall关键字实际上只在Haskell中以一种方式使用.当你看到它时,它总是意味着同样的事情.
通用量化
甲普遍量化类型是一种形式的forall a. f a.该类型的值可以被认为是一个函数采用一个类型 a作为其参数,并返回值类型的f a.除了在Haskell中,这些类型参数由类型系统隐式传递.无论它接收哪种类型,这个"函数"都必须给你相同的值,因此值是多态的.
例如,考虑类型forall a. [a].该类型的值采用另一种类型a,并返回相同类型的元素列表a.当然,只有一种可能的实施方式.它必须给你空列表,因为a它绝对是任何类型.空列表是元素类型中唯一的多态的列表值(因为它没有元素).
或类型forall a. a -> a.这种函数的调用者提供类型a和类型的值a.然后,实现必须返回相同类型的值a.只有一种可能的实施方式.它必须返回与给定值相同的值.
存在量化
一个存在性量化类型将有形式exists a. f a,如果哈斯克尔支持该符号.该类型的值可以被认为是由类型和类型值组成的对(或"产品").af a
例如,如果您具有type类型的值,则您具有exists a. [a]某种类型的元素列表.它可以是任何类型,但即使你不知道它是什么,你可以做很多这样的清单.您可以反转它,或者您可以计算元素的数量,或执行不依赖于元素类型的任何其他列表操作.
好的,等一下.为什么Haskell forall用来表示如下所示的"存在主义"类型？
data ShowBox = forall s. Show s => SB s
它可能令人困惑,但它确实描述了数据构造函数 的类型SB:
SB :: forall s. Show s => s -> ShowBox
构造完成后,您可以将类型值ShowBox视为由两件事组成.它是一种类型s和类型的值s.换句话说,它是存在量化类型的值.如果Haskell支持这种表示法,那ShowBox真的可以写成exists s. Show s => s.
runST 和朋友
鉴于此,这些有何不同？
foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))
我们先来看看bar.它采用类型a和函数类型a -> a,并生成类型的值(Char, Bool).我们可以选择Int作为a类型的函数,Int -> Int例如.但是foo不同.它要求实现foo能够将它想要的任何类型传递给我们给它的函数.所以我们可以合理地给它的唯一功能是id.
我们现在应该能够解决以下类型的含义runST:
runST :: forall a. (forall s. ST s a) -> a
所以runST必须能够产生类型的值a,无论我们给出什么类型a.要做到这一点,它需要一个类型的参数,forall s. ST s a它只是类型的函数a.然后,该函数必须能够生成类型的值,而a不管实现runST决定给出的类型s.
好的,那又怎样？好处是,这会对调用者施加约束runST,因为类型a根本不涉及类型s.例如,您不能将类型的值传递给它ST s [s].这在实践中意味着实现runST可以使用类型的值自由地执行变异s.类型系统保证这种突变是本地实现的runST.
类型runST是rank-2多态类型的示例,因为其参数的类型包含forall量词.foo上面的类型也是第2级.普通的多态类型,如同bar,是秩-1,但如果参数的类型需要具有多态性,并且具有自己的forall量词,则它变为rank-2 .如果一个函数采用rank-2参数,那么它的类型是rank-3,依此类推.通常,采用排名的多态参数的类型n具有排名n + 1.
任何人都可以用清晰,简单的英语完全解释forall关键字(或者,如果它存在于某个地方,指向我错过的这样一个明确的解释),并不认为我是一个沉浸在行话中的数学家？
我将尝试forall在Haskell及其类型系统的上下文中解释其含义和可能的应用.
但是在你明白我想引导你去Runar Bjarnason的一个非常容易接受和好听的演讲题为" 限制解放,自由约束 ".这个演讲充满了来自现实世界用例的例子以及Scala中支持这一陈述的例子,尽管它没有提及forall.我将尝试解释forall下面的观点.
CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN
非常重要的是消化并相信这个陈述继续下面的解释,所以我恳请你观看谈话(至少部分内容).
现在一个非常常见的例子,显示Haskell类型系统的表现力是这种类型的签名:
foo :: a -> a
据说,给定这种类型的签名,只有一种功能可以满足这种类型,即identity功能或更普遍的功能id.
在我学习Haskell的初级阶段,我总是想知道以下功能:
foo 5 = 6
foo True = False
他们都满足上面的类型签名,那么为什么Haskell人声称它是id单独的满足类型签名？
那是因为forall类型签名中隐含了隐藏.实际类型是:
id :: forall a. a -> a
那么,现在让我们回到声明:限制解放,自由约束
将其转换为类型系统,此语句变为:
和
让我们试着证明第一个陈述:
类型级别的约束..
因此对我们的类型签名施加约束
foo :: (Num a) => a -> a
在术语层面成为自由 使我们有自由或灵活性来编写所有这些
foo 5 = 6
foo 4 = 2
foo 7 = 9
...
通过约束a任何其他类型类等可以观察到相同的情况
那么现在这种类型签名:foo :: (Num a) => a -> a转换为:
?a , st a -> a, ?a ? Num
这被称为存在量化,它转化为存在一些实例,a当某个类型的函数输入时,a返回某些相同类型的函数,并且这些实例都属于数字集.
因此,我们可以看到添加约束(a应该属于Numbers集),释放术语级别以具有多个可能的实现.
现在进入第二个陈述,实际上有一个解释forall:
类型层面的自由成为术语层面的约束
所以现在让我们解释类型级别的函数:
foo :: forall a. a -> a
现在这转换为:
?a , a -> a
这意味着此类型签名的实现应该a -> a适用于所有情况.
所以现在这开始限制我们的学期水平.我们再也写不出来了
foo 5 = 7
因为如果我们把它a作为一个,这个实现就不会满足Bool.a可以是a Char或a [Char]或自定义数据类型.在任何情况下它都应该返回类似的东西.这种类型级别的自由是所谓的通用量化,唯一可以满足这一要求的功能就是
foo a = a
这通常被称为identity功能
因此forall是liberty类型级别的,其实际目的是针对constrain特定实现的术语级别.