gwi*_*man 16 haskell pattern-matching
我试图理解Haskell 2010报告第3.17.2节 "模式匹配的非正式语义".大多数情况,与模式匹配成功或失败有关,似乎很简单,但是我很难理解被描述为模式匹配"发散"的情况.
我被半说服意味着匹配算法没有"收敛"到答案(因此匹配函数永远不会返回).但是,如果不返回,那么,它如何返回一个值,如括号"ie return ?"所示？?无论如何"返回" 意味着什么？一个人如何处理这个结果？
第5项具有特别令人困惑的(对我而言)"如果值为?,则匹配发散".这只是说一个值?产生匹配结果?？(撇开我不知道那个结果意味着什么!)
任何照明,可能有一个例子,将不胜感激!
经过几个冗长的回答后补遗:感谢Tikhon和所有人的努力.
似乎我的困惑来自于存在两个不同的解释领域:Haskell特征和行为的领域,以及数学/语义领域,而在Haskell文献中,这两者混合在一起,试图用后者来解释前者. ,没有足够的路标(对我来说)属于哪个元素.
显然,"底部" ?位于语义域中,并且不作为Haskell中的值存在(即:您无法输入,您永远不会得到打印为" ?"的结果).
因此,在解释说函数"返回 ?"的地方,这指的是执行任何许多不方便的事情的函数,例如不终止,抛出异常或返回"未定义".是对的吗？
此外,那些评论说?实际上是一个可以传递的价值的人, 实际上是在考虑绑定到尚未被实际评估的普通函数(可以说是"未爆炸的炸弹")并且可能永远不会,由于懒惰,对吧？
Tik*_*vis 16
值为⊥,通常发音为"bottom".它是在语义意义上的价值-这是不是一个正常的Haskell的价值本身.它表示不产生正常Haskell值的计算:例如,异常和无限循环.
语义学是关于定义程序的"含义".在Haskell中,我们通常谈论指称语义,其中值是某种数学对象.最简单的例子是表达式10(以及表达式9 + 1)具有数字 10的表示(而不是Haskell值 10).我们通常写出这?9 + 1? = 10意味着Haskell表达式的表示9 + 1是数字10.
但是,我们用表达式做什么let x = x in x呢？此表达式没有Haskell值.如果你试图评估它,它将永远不会完成.而且,这对应于什么数学对象并不明显.但是,为了推理程序,我们需要给它一些表示.所以,基本上,我们只是为所有这些计算组成一个值,我们称之为值bottom(底部).
所以⊥只是一种定义不返回"计算"的计算的方法.
我们还定义了其他类似的计算undefined和error "some message"作为?,因为他们还没有明显的正常值.因此抛出异常对应于?.这正是失败的模式匹配所发生的情况.
通常的思考方式是每个Haskell类型都被"提升" - 它包含?.也就是说,Bool对应{?, True, False}而不仅仅是{True, False}.这表示Haskell程序不能保证终止并且可以有例外.定义自己的类型时也是如此 - 类型包含您为其定义的每个值?.
有趣的是,由于Haskell是非严格的,?可以存在于普通代码中.所以你可以拥有一个像这样的价值Just ?,如果你从来没有评价它,一切都会好起来的.一个很好的例子是const:const 1 ?评估为1.这适用于失败的模式匹配:
const 1 (let Just x = Nothing in x) -- 1
您应该阅读Haskell WikiBook中关于指称语义的部分.这是一个非常平易近人的介绍,我个人觉得非常有趣.
J. *_*son 11
因此,简单的指称语义,即?生命,是从Haskell值到其他一些值空间的映射.你这样做是为了以更正式的方式赋予程序意义,而不仅仅是讨论程序应该做什么 - 你说它们必须尊重它们的指称语义.
因此,对于Haskell,您经常考虑Haskell表达式如何表示数学值.您经常会看到Strachey括号?·?表示从Haskell到Math的"语义映射".最后,我们希望我们的语义括号与语义操作兼容.例如
?x + y? = ?x? + ?y?
左侧+是Haskell函数(+) :: Num a => a -> a -> a,右侧是交换组中的二元运算.虽然很酷,但因为我们知道我们可以使用语义映射中的属性来了解我们的Haskell函数应该如何工作.也就是说,让我们在"数学"中写下交换属性
?x? + ?y? == ?y? + ?x?
= ?x + y? == ?y + x?
= ?x + y == y + x?
其中第三步也表明Haskell (==) :: Eq a => a -> a -> a应该具有数学等价关系的属性.
无论如何,这一切都很好,直到我们记住计算机是有限的东西而数学并不太关心(除非你使用直觉逻辑,然后你得到Coq).所以,我们必须注意我们的语义不遵循Math的地方.这是三个例子
?undefined? = ??
?error "undefined"? = ??
?let x = x in x? = ??
这是?发挥作用的地方.我们只是断言,就Haskell的指称语义而言,每个例子都可能意味着(新引入的数学/语义概念)?.什么是数学属性?？好吧,这就是我们开始真正深入了解语义域并开始讨论函数和CPO等的单调性的地方.但基本上,这?是一个数学对象,与非终止游戏大致相同.从语义模型的角度来看,?它是有毒的,它以其毒性 - 非确定性来感染表达.
但它不是Haskell语言的概念,只是一种语言域的Haskell语言.在Haskell中,我们有undefined,error和无限循环.这个很重要.
因此,?undefined? = ?error "undefined"? = ?let x = x in x? = ?一旦我们理解了数学的意义,语义?就很清楚,但同样清楚的是,每个语义都具有"现实"中的不同效果.这有点像C的"未定义行为"......就语义域而言,它的行为是未定义的.你可能会在语义上称它为不可观察的.
?呢？那么"语义上"回归是什么意思?呢？嗯,?是一个完全有效的语义值,它具有模拟非确定性(或异步错误抛出)的感染属性.从语义的角度来看,它是一个完全有效的值,可以按原样返回.
从实现的角度来看,您有许多选择,每个选择都映射到相同的语义值.undefined是不是正确,也没有进入无限循环,所以如果你要选择一个语义上未定义的行为,你也可以选择一个有用的并抛出错误
*** Exception: <interactive>:2:5-14: Non-exhaustive patterns in function cheers