Pet*_*lák 6 haskell ghc compiler-optimization strictness
我始终认为,更换的表达x :: ()与() :: ()将编译Haskell程序中最基本的优化之一.由于()有一个居民,无论是什么x,它的结果是().在我看来,这种优化是参考透明度的重要结果.我们可以为只有一个居民的任何类型做这样的优化.
(更新:我在这个问题上的推理来自于自然演绎规则.单位类型对应于真值(⊤),我们有一个扩展规则"如果x : ?那么() : ?".例如见本文第20页.我认为它是安全的用扩展或契约替换表达式.)
这种优化的一个结果是undefined :: ()将被替换为() :: (),但我不认为这是一个问题 - 它只会让程序变得更加懒惰(并且依赖于undefined :: ()当然是一种糟糕的编程习惯).
但是今天我意识到这样的优化会Control.Seq彻底打破.Strategy被定义为
type Strategy a = a -> ()
我们有
-- | 'rseq' evaluates its argument to weak head normal form.
rseq :: Strategy a
rseq x = x `seq` ()
但是rseq x :: (),优化只会丢弃x对WHNF 的必要评估.
那问题出在哪里？
rseq和seq破坏引用透明度(即使我们只考虑终止表达式)？Strategy我们可以设计一种更好的方法来强制表达式与WHNF兼容吗？小智 11
引用透明性是关于相等语句和变量引用.当你说X = Y,你的语言是引用透明,那么你就可以替换的每一次出现X由Ÿ(模数范围).
如果没有指定x = (),那么你就不能更换x的()安全,比如你的情况.这是因为你对居民的错误(),因为在Haskell中有两个:一个是唯一的构造函数(),即().另一个是从未计算过的值.您可以将其称为底部或未定义:
x :: ()
x = x
你当然不能代替任何发生x由()这里,因为这将有机会语义.语言语义中底层的存在允许一些尴尬的边缘情况,特别是当你有一个seq组合器时,你甚至可以证明每个monad错误.这就是为什么在许多正式讨论中我们忽视了底层的存在.
但是,参考透明度不会受此影响.Haskell仍然是引用透明的,因此是一种纯函数式语言.
您对引用透明度的定义不正确.参考透明度并不意味着您可以替换x :: (),() :: ()并且一切都保持不变; 这意味着你可以用它的定义替换所有出现的变量,并且一切都保持不变.seq而rseq不是与引用透明的冲突,如果你使用这个定义.