证明即程序、结论公式即程序类型

Haskell_百度百科 https://baike.baidu.com/item/Haskell

Haskell(发音为 /ˈhæskəl/) [1]  是一种标准化的,通用纯函数式编程语言,有非限定性语义和强静态类型。它的命名源自美国逻辑学家Haskell Brooks Curry,他在数学逻辑方面的工作使得函数式编程语言有了广泛的基础。在Haskell中,“函数是一等公民”。 [2]  作为函数式编程语言,主要控制结构是函数。Haskell语言是1990年在编程语言Miranda的基础上标准化的,并且以λ演算(Lambda-Calculus)为基础发展而来。具有“证明即程序、结论公式即程序类型” [3-6]  的特征。这也是Haskell语言以希腊字母「λ」(Lambda)作为自己标志的原因。Haskell语言的最重要的两个应用是GHC(Glasgow Haskell Compiler)和Hugs(一个Haskell语言的解释器)。

原文地址:https://www.cnblogs.com/rsapaper/p/9632736.html