您當前的位置:首頁 > 繪畫

柯里化的前生今世(十一):Pure and Lazy

作者:由 何幻 發表于 繪畫時間:2018-03-03

語言的作用

語言的作用是為了交流想法,描述概念,

當前使用了什麼語言,取決於我們有什麼樣的需要。

為了理解詞法作用域,閉包,和continuation,

前文中,我們藉助了Racket。

現在,為了理解代數資料型別(algebraic data type),多型(polymorphism),引數化型別(parameterized type),型別類(type class),我們要學習Haskell了。

程式設計也是如此,它是關於思想的,

程式語言只是描述這種思想的工具罷了。

柯里化的前生今世(十一):Pure and Lazy

非嚴格語義(non-strict semantics)

在Haskell規範中,並沒有要求使用惰性求值策略(evaluation strategy),

只是規定它是一種非嚴格的語言(non-strict language),

具體的求值策略取決於實現。

那麼,什麼才能叫做non-strict呢?

non-strict與lazy有什麼關係呢?

還要從數學上函式的嚴格性(strictness)說起。

程式中的function與數學函式之間的關係,

是指稱語義中的內容。(指稱語義是形式語義的一種,它將每一段程式碼,與一個數學物件相對應,用來研究程式的含義。

在數學上,如果一個函式對定義域中的某些引數,沒有定義值,

就稱為該函式為部分函式(partial function)。

柯里化的前生今世(十一):Pure and Lazy

程式中的function,對應著數學上的部分函式。

此外,程式中某一型別的全體值,也不能簡單的對應於數學上的集合,

例如,程式中的全體整數型別的值,並不對應於整數集,

因為返回整型值的function,取某些引數時,程式可能不會終止。

為了給這樣的function和返回值找到指稱,

我們給每個集合增加一個新的值:

,讀作bottom。

f(⊥) = ⊥

一個數學函式,如果引數是

,那麼結果就一定是

這樣的函式稱為嚴格函式(strict function)。

反之,如果引數包含

,但是結果不一定是

這樣的函式就稱為非嚴格函式(non-strict function)。

如果程式語言中function的指稱語義是非嚴格函式,

那麼這樣的語言,就稱為非嚴格的語言(non-strict language)。

注:

嚴格性是指稱語義中的概念,而求值是操作語義中的概念。

並且指稱語義對於操作語義具有可靠性(soundness),

即,如果一個表示式根據操作語義求值為另一個,那麼,它們必定具有相同的指稱。

因此,對於non-strict language,求值策略可能並不唯一,

對Haskell來說,GHC是最流行的編譯器,

它使用了惰性求值(lazy evaluation)。

在沒有歧義的情況下,人們常用lazy暗指non-strict,

lazy更直觀更有利於溝通。

引用透明性

An expression is said to be referentially transparent if it can be replaced with its corresponding value without changing the program‘s behavior。

即,引用透明性(referential transparency)指的是,

程式中的表示式總是可以用它的值來代替。

而程式中的純函式(pure function),指的是,

(1)這個函式對相同引數總是輸出相同結果

(2)這個函式沒有副作用(side effect)

因此,純函式具有引用透明性。

此外,語言採用了惰性求值,意味著表示式的求值方式是按需確定的,

所以,依靠副作用來得到計算結果就不可行了,

我們不知道計算在什麼時候發生。

因此,一旦語言擁抱了惰性求值,就不得不保證引用透明性,

反之則不一定,具有引用透明性的語言,可能不必是惰性求值的。

至於,純函式是不是解決問題的最佳方式,目前尚無定論,

但至少它是為了追求優雅性,對通常程式設計方式的一種挑戰。

歷史上的純函式式惰性語言

在20世紀70年代末,Gerry Sussman和Guy Steele發明了Scheme,它是Lisp的一個方言,與lambda演算很相似,並支援了詞法作用域。

幾乎同時,Robin Milner為了進行自動定理證明發明瞭ML,其中使用了多型型別系統。

但是Scheme和ML都是基於嚴格語義的語言(strict language)。

到了80年代,人們燃起了對非嚴格語義的(non-strict),或者說是按需求值的(call-by-need)函式式語言的研究熱情。

這方面的研究理所當然的吸引了很多人,首先,函式式語言簡單而優雅,其次,惰性(lazy)與引用透明性有關,並且還可以處理無窮長的資料結構(infinite data structure)。

在80年代中期,很多研究者都想設計實現一個純函式式的(pure)惰性語言,Miranda和Lazy ML是其中的兩個例子。

1987年波特蘭FPCA’87會議之後,與會者想發明一種尚未命名的新語言,

其實一開始,人們想從一門現有的語言開始,逐漸發展迭代,比如說,使用當時最成熟的Miranda。

Miranda是David Turner的公司Research Software Limited開發的一門語言,它是惰性求值的,包含代數資料型別,使用了Hindley-Milner型別系統,從1985年起用於商業中。Miranda有很好使用者介面,對實現的支援良好,還有大量的教材。

可是,與David Turner溝通後,他拒絕了這件事。

我們想要一門用於研究語言特性的語言,因此我們決定任何人都可以擴充套件和修改語言本身,重新實現或者發行。但是David Turner想維持一份語言規範,讓語言具有最好的可移植性,他不想讓Miranda出現各種不同的方言。

於是,Haskell的故事就這樣開始了。

柯里化的前生今世(十一):Pure and Lazy

參考

A History of Haskell

Non-strict semantics

Lazy Evaluation of Haskell

Foundations for Programming Languages

下一篇:柯里化的前生今世(十二):多型性

標簽: 函式  strict  求值  語言  語義