为什么从Int到Int只有一个非严格的函数？

Question

根据这篇关于Haskell的指称语义的文章,从Int到Int只有一个非严格(非底部保留)函数.

报价:

碰巧只有一个类型为Integer - > Integer的非严格函数的原型:

一个x = 1

对于每个具体数字k,其变体是constk x = k.为什么这些是唯一可能的？请记住,一个n可没少比一个⊥定义.由于Integer是一个扁平域,因此两者必须相等.

基本上它表示该类型签名的唯一非严格函数只能是常量函数.我不遵循这个论点.我也不确定平面域是什么意思,文章的其余部分导致相信它只是意味着值的集合只有一个节点:bottom.

函数从A-> A或A-> B出现类似的情况？那是他们必须是不变的功能？

Answer 1

任何关于Integer那个函数的函数都不const k是k必须检查它的参数.你不能部分检查Integer,哪个可能是什么意思是它是一个"平坦的领域".这是IntegerHaskell规范中定义语义的结果,而不是核心语言的语义.

相比之下,[a] -> [a]每种类型都存在无限多种类型的非严格函数a,例如take1:

take1 (x:_) = [x]

要显示非严格性,请定义

ones = 1 : ones

在指称语义方面,[[ ones]] =⊥.但take1 ones计算结果为[1],所以take1是不严谨的.那么是take2 (x:y:_) = [x,y],take10等

如果你想在整数上使用非严格的非常量函数,你需要一个不同的整数表示Integer,例如:

data Bit = Zero | One
newtype BinaryInt = I [Bit]

如果我们将列表解释I为"little-endian"二进制整数,那么函数

mod2 (I [])       =  I []
mod2 (I (lsb:_))  =  I [lsb]

是非严格的.

Answer 2

直觉是懒惰的函数不能在不强制它的情况下检查它的参数(因此变得严格).如果你不检查你的论点,你必须const

单调性的真正答案.如果您将语义域视为其中排序关系是"已定义"之一的posets,则所有函数都是顺序保留.为什么？由于所有底部都是相同的,并且永远循环与底部相同,因此非单调函数将解决停止问题.

好吧,那为什么这意味着它const创造了唯一的懒惰功能呢？好了,说挑一个任意函数f,使得

f :: Integer -> Integer
f ? = y

因为? <= x对所有人来说x,一定是这样y <= f x.如果y是非底值,那么该不等式的唯一解决方案是f x = y

编辑:这个参数适用于类型的类型Integer,Bool但不适用于类型类型的原因[a]是最后一步:Integer在某种意义上,只有一个单独?的类型.也就是说,除了之外,所有整数都是同样定义的?.另一方面,? < (?:?)虽然(?:?) < (?:[])还有(?:?) < (?:(?:?)) < (?:(?:(?:?))) < ...更多,(?:?) < ('a':?).也就是说,语义域[a]是足够丰富,以至于y <= f x用y =/= ?并不意味着f x = y.