В чем смысл "let x = x in x" и "Data Float #" в GHC.Prim в Haskell - программирование
Подтвердить что ты не робот

В чем смысл "let x = x in x" и "Data Float #" в GHC.Prim в Haskell

Я посмотрел на модуль 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.
-}

Я думаю, это может иметь некоторые отношения с вопросами, и кто мог бы объяснить это мне.

4b9b3361

ОТВЕТЫ

Ответ 1

Это магия:)

Это "примитивные операторы и операции". Они жестко подключены к компилятору, поэтому нет конструкторов данных для примитивов, и все функции являются нижними, так как они обязательно не выражаются в чистом haskell.

(Bottom представляет собой "отверстие" в программе haskell, бесконечный цикл или undefined являются примерами дна)

Иными словами,

Эти декларации/функции данных предназначены для обеспечения доступа к внутренним внутренним компиляторам. GHC.Prim существует для экспорта этих примитивов, он фактически не реализует их или что-либо (например, его код фактически не полезен). Все это делается в компиляторе.

Это означает, что код должен быть чрезвычайно оптимизирован. Если вы считаете, что вам это может понадобиться, некоторые полезные чтение о примитивах в GHC

Ответ 2

Краткое расширение ответа jozefg...

Примпы - это именно те операции, которые предоставляются средой выполнения, потому что они не могут быть определены внутри языка (или не должны быть, по соображениям эффективности, сказать). Истинная цель GHC.Prim заключается не в том, чтобы определять что-либо, а просто для экспорта некоторых операций, чтобы Haddock мог документировать их существование.

Конструкция let x = x in x используется в этой точке в кодовой базе GHC, потому что значение undefined еще не было, um, "определено". (Это ждет до прелюдии.) Но обратите внимание, что круговая конструкция let, как и undefined, является синтаксически правильной и может иметь любой тип. То есть, это бесконечный цикл с семантикой ⊥, как и undefined.

... и в стороне

Также обратите внимание, что в общем случае выражение Haskell let x = z in y означает "изменить переменную x на выражение z везде, где x встречается в выражении y". Если вы знакомы с исчислением лямбда, вы должны признать это как правило сокращения для применения лямбда-абстракции \x -> y к термину z. Так выражение Haskell let x = x in x не что иное, как некоторый синтаксис на вершине чистого лямбда-исчисления? Давайте посмотрим.

Во-первых, нам нужно учитывать рекурсивность выражений Haskell let. Исчисление лямбда не допускает рекурсивных определений, но при условии примитивного оператора с фиксированной точкой fix, 1 мы можем явно кодировать рекурсию. Например, выражение Haskell let x = x in x имеет то же значение, что и (fix \r x -> r x) z. 2 (я переименовал x в правой части приложения в z, чтобы подчеркнуть, что это не имеет никакого неявного отношения к x внутри лямбда).

Применяя обычное определение оператора фиксированной точки, 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                 ==>   ...

Итак, на этом этапе развития языка мы ввели семантику ⊥ из основания (типизированного) лямбда-исчисления со встроенным оператором фиксированной точки. Прекрасный!

  • Нам нужна примитивная операция с фиксированной точкой (т.е. встроенная в язык), потому что невозможно определить комбинатор с фиксированной точкой в ​​просто типизированном лямбда-исчислении и его близких родственниках. (Определение fix в Haskell Prelude не противоречит этому - оно определено рекурсивно, но нам нужен оператор с фиксированной точкой для реализации рекурсии.)

  • Если вы еще этого не видели, вам следует прочитать рекурсию с фиксированной точкой в ​​исчислении лямбда. Текст по лямбда-исчислению лучше (есть некоторые бесплатные онлайн), но некоторые Googling должны вас поймать. Основная идея заключается в том, что мы можем преобразовать рекурсивное определение в нерекурсивный путем абстрагирования по рекурсивному вызову, а затем использовать комбинатор с фиксированной запятой, чтобы передать нашу функцию (абстракцию лямбда) для себя. Базовый регистр четко определенного рекурсивного определения соответствует фиксированной точке нашей функции, поэтому функция выполняется, вызывая себя снова и снова, пока не достигнет фиксированной точки, после чего функция возвращает результат. Довольно чертовски аккуратно, да?