我应该首先提一下,我对Haskell很新.有没有特别的理由let在Haskell中保留表达式？
我知道Haskell摆脱了rec对应于let语句的Y-combinator部分的关键字,表明它是递归的.为什么他们没有let完全摆脱声明呢？
如果他们这样做,陈述在某种程度上似乎会更加迭代.例如,类似于:
let y = 1+2
z = 4+6
in y+z
只会是:
y = 1+2
z = 4+6
y+z
对于熟悉函数式编程的人来说,哪个更易读,更容易阅读.我能想到保持它的唯一原因是这样的:
aaa = let y = 1+2
z = 4+6
in y+z
如果没有这个let,我认为最终会出现模棱两可的语法:
aaa =
y = 1+2
z = 4+6
y+z
但是如果Haskell没有忽略空格,并且代码块/范围与Python类似,它是否能够删除let？
是否有更强的理由留下来let？
对不起,如果这个问题看起来很愚蠢,我只是想了解更多关于它为什么存在的问题.
从语法上讲,你可以很容易地想象出一种语言let.where如果我们想要的话,我们可以立即依靠Haskell来生成这个.除此之外还有许多可能的语法.
在语义上,你可能会认为让我们可以转化为类似的东西
let x = e in g ==> (\x -> g) e
实际上,在运行时这两个表达式是相同的(模递归绑定,但可以用它来实现fix).但是,传统上,它let具有特殊的类型语义(以及where顶级名称定义......所有这些都是有效的语法糖let).
特别是在形成Haskell基础的Hindley-Milner型系统中,存在一种let概括性的概念.直观地说,它将我们将函数升级到最多态的形式.特别是,如果我们有一个函数出现在某个类似的类型的表达式中
a -> b -> c
这些变量,a,b,和c,可能会或可能不会已经在表达的意思.特别是,他们被认为是固定的未知类型.将其与类型进行比较
forall a b c. a -> b -> c
其中包括的概念多态性通过陈述,立即,即使有碰巧是类型变量a,b以及c可在envionment,这些引用是新鲜的.
这是HM推理算法中非常重要的一步,因为它是如何生成多态,允许HM达到其更一般的类型.不幸的是,只要我们愿意,就不可能做到这一步 - 它必须在受控点完成.
这就是let-generalization的作用:它表示当类型绑定let到特定名称时,应该将类型推广到多态类型.当它们仅作为参数传递给函数时,不会发生这种泛化.
因此,最终,您需要一种"let"形式才能运行HM推理算法.此外,它不仅仅是功能应用的语法糖,尽管它们具有相同的运行时特性.
从语法上讲,这个"let"概念可以被调用let,where或者通过顶级名称绑定的约定来调用(这三个都在Haskell中可用).只要它存在并且是生成人们期望多态性的绑定名称的主要方法,那么它将具有正确的行为.
为什么Haskell和其他功能语言使用有重要原因let.我会尝试逐步描述它们:
Haskell和其他函数语言中使用的Damas-Hindley-Milner类型系统允许多态类型,但类型量词仅允许在给定类型表达式的前面.例如,如果我们写
const :: a -> b -> a
const x y = x
然后const是多态的类型,它被隐含地普遍量化为
?a.?b. a -> b -> a
并且const可以专门到我们通过替换两个式表达式获得任何类型a和b.
但是,类型系统不允许在类型表达式中使用量词,例如
(?a. a -> a) -> (?b. b -> b)
在系统F中允许这样的类型,但是类型检查和类型推断是不可判定的,这意味着编译器将无法为我们推断类型,并且我们必须使用类型显式地注释表达式.
(长期以来,系统F中类型检查的可判定性问题一直存在,并且它有时被称为"一个令人尴尬的开放性问题",因为许多其他系统已经证明了不可判定性,但是这个系统已被证实,直到Joe Wells于1994年.)
(GHC允许您使用RankNTypes扩展来启用此类显式内部量词,但如上所述,无法自动推断类型.)
考虑表达式?x.M,或者在Haskell表示法中\x -> M,M某些术语包含在哪里x.如果xis a的类型和类型M是b,那么整个表达式的类型将是?x.M : a ? b.由于上述限制,a一定不能包含∀,因此类型x不能包含类型量词,它不能是多态的(换句话说它必须是单态的).
考虑一下这个简单的Haskell程序:
i :: a -> a
i x = x
foo :: a -> a
foo = i i
让我们现在忽视它foo不是很有用.重点是id在定义foo中用两种不同的类型进行实例化.第一个
i :: (a -> a) -> (a -> a)
第二个
i :: a -> a
现在,如果我们尝试将此程序转换为纯粹的lambda演算语法let,我们最终会得到
(?i.i i)(?x.x)
第一部分是定义,foo第二部分是定义i.但这个术语不会打字.问题是i必须具有单形类型(如上所述),但我们需要它是多态的,以便我们可以实例化i到两种不同的类型.
实际上,如果你试图i -> i i在Haskell中进行类型检查,那么它将失败.没有我们可以指定的单态类型,i以便进行类型检查i i.
let 解决了这个问题如果我们写let i x = x in i i,情况就不同了.与前一段不同,这里没有lambda,没有像这样的自包含表达式?i.i i,我们需要一个抽象变量的多态类型i.因此let可以允许i有一个polymorhpic类型,在这种情况下?a.a ? a,因此i itypechecks.
如果没有let,如果我们编译了一个Haskell程序并将其转换为单个lambda术语,则必须为每个函数分配一个单态类型!这将是无用的.
因此let,基于Damas-Hindley-Milner类型系统的语言中的多态性是一种必不可少的结构.
Haskell的历史讲述了Haskell早已接受复杂的表面语法这一事实.
我们在这里花了一些时间来确定风格选择,但是一旦我们这样做了,我们就哪种风格"更好"进行了激烈的争论.一个潜在的假设是,如果可能的话应该只有一种方式做一些事情,"所以,例如,让let和where会多余和混乱.
最后,我们放弃了潜在的假设,并为这两种风格提供了完整的语法支持.这似乎是一个典型的委员会决定,但是现在的作者认为这是一个很好的选择,我们现在认为这是一种语言的力量.不同的结构具有不同的细微差别,真正的程序员在实践中同时使用let和where,guards和conditionals,模式匹配定义和case表达式 - 不仅在同一个程序中,有时在同一个函数定义中.毫无疑问,额外的句法糖使语言看起来更精细,但它是一种肤浅的复杂性,很容易通过纯粹的句法转换来解释.
这不是一个愚蠢的问题。这是完全合理的。
首先，let/in 绑定在语法上是明确的，并且可以以简单的机械方式重写为 lambda。
其次，正因为如此，let ... in ...它是一个表达式：也就是说，它可以写在任何允许表达式的地方。相反，您建议的语法更类似于where，它绑定到周围的语法构造，例如函数定义的模式匹配行。
人们也可能会争论说你建议的语法在风格上过于命令式，但这当然是主观的。
您可能更喜欢使用whereto let。许多 Haskell 开发人员都这样做。这是一个合理的选择。