Haskell中GHC.Prim中"let x = x in x"和"data Float#"的含义是什么

Question

我查看了GHC.Prim的模块,发现似乎GHC.Prim中的所有数据都被定义为data Float#没有类似的东西=A|B,并且GHC.Prim中的所有函数都被定义为gtFloat# = let x = x in x.

我的问题是这些定义是否有意义以及它们的含义.

我检查了GHC.Prim的标题,如下所示

{-
This is a generated file (generated by genprimopcode).
It is not code to actually be used. Its only purpose is to be
consumed by haddock.
-}

我想它可能与问题有一些关系,谁可以向我解释.

Answer 1

这是魔法 :)

这些是"原始的运营商和运营".它们被硬编码到编译器中,因此没有用于基元的数据构造器,并且所有函数都是底层的,因为它们在纯haskell中不一定是不可表达的.

(底部表示haskell程序中的"洞",无限循环或undefined底部示例)

换一种方式

这些数据声明/函数用于提供对原始编译器内部的访问.GHC.Prim存在用于导出这些原语,它实际上并不实现它们或任何东西(例如它的代码实际上并不实用).所有这些都是在编译器中完成的.

它适用于需要极其优化的代码.如果您认为可能需要它,那么可以阅读一些有关GHC中原语的有用信息

Answer 2

jozefg答案的简短扩展......

Primops正是由运行时提供的那些操作,因为它们不能在语言中定义(或者出于效率的原因,不应该被定义).真正的目的GHC.Prim不是要定义任何东西,而只是导出一些操作,以便Haddock可以记录它们的存在.

这个构造let x = x in x在GHC的代码库中就此使用了,因为该值undefined还没有被定义.(等到Prelude.等等.)但请注意,圆形let结构就像undefined语法正确一样,可以有任何类型.也就是说,它是一个带有⊥语义的无限循环,就像它一样undefined.

......而且放在一边

另请注意,通常Haskell表达式let x = z in y意味着"将变量更改x为表达式中出现的z任何位置x的表达式y".如果您熟悉lambda演算,则应将此视为将lambda抽象\x -> y应用于该术语的缩减规则z.那么Haskell表达式let x = x in x只不过是纯lambda演算之上的一些语法吗？让我们来看看.

首先,我们需要考虑Haskell的let表达式的递归性.该演算不承认递归定义,但由于原始的定点操作fix,¹我们可以明确地编码递归.例如,Haskell表达式let x = x in x具有相同的含义(fix \r x -> r x) z.²(我已经重命名了x应用程序的右侧,z以强调它x与lambda内部没有隐含的关系).

应用定点运算符的通常定义fix f = f (fix f),我们的翻译let x = x in x减少(或者不是)这样:

(fix \r x -> r x) z                 ==>
(\s y -> s y) (fix \r x -> r x) z   ==>
(\y -> (fix \r x -> r x) y) z       ==>
(fix \r x -> r x) z                 ==>   ...

因此,在语言开发的这一点上,我们使用内置的定点运算符从(类型化的)lambda演算的基础引入了se的语义.可爱!

1. 我们需要一个原始的定点操作(也就是说,内置于语言中),因为在简单类型的lambda演算及其近亲中定义一个定点组合器是不可能的.(fixHaskell的Prelude中的定义与此不矛盾 - 它是递归定义的,但是我们需要一个定点运算符来实现递归.)

2. 如果您之前没有看过这个,那么您应该阅读lambda演算中的定点递归.关于lambda演算的文本是最好的(有一些免费的在线),但一些谷歌搜索应该让你去.基本思想是我们可以通过抽象递归调用将递归定义转换为非递归定义,然后使用定点组合器将我们的函数(lambda抽象)传递给自身.定义良好的递归定义的基本情况对应于函数的固定点,因此函数执行,一遍又一遍地调用自身,直到它到达一个固定点,此时函数返回其结果.该死的很整洁,对吧？