LINUX.ORG.RU

История изменений

Исправление wandrien, (текущая версия) :

Почему не назвать это Nullptr, и буквально засунуть его внутрь типа NullablePointer = Pointer | Nullptr?

Потому что фактически это так и есть, но в языке с системой типов уровня Паскаля нет возможности выразить эту мысль.

Поэтому я иду снизу, от реализации: сначала в ЯП будут введены аналоги NullablePointer<a> и Pointer<a> в качестве типов из коробки, а уже потом - средства выражать идентичные концепции на языке типов.

Тут, кстати, есть забавное следствие несоответствия императивной и функциональной семантики.

В функциональной семантике выражение, типом которого является nulltype, является таким же законным выражением, как и любое другое. А поскольку nulltype заведомо не требует никакого вычисления, тело выражения может быть сразу свёрнуто до null.

А в императивной семантике функция, возвращающая результат типа nulltype, может иметь побочные эффекты.

Разрешение этого несоответствия требует введения понятия чистоты функции в ЯП.

В случае боттомов всё всегда сложнее. В ленивых языках боттом - это значение, да ещё (взмахивая руками) «любого типа». В энергичных это зачастую честный Never, без значений. И там и там произносятся похожие слова про невозвращаемость, но я не понимаю до конца, как обо всём этом думать. В теории типов, с которой я знаком, этот вопрос обходится стороной, по крайней мере при первом знакомстве. Дальше там как будто можно нагородить конструкции из refl’ов, но поля слишком узки.

Это на слишком сложном, пожалуй. Тут я пасс. Трактовка недостижимого значения как значения «любого типа» по смыслу заставляет вспомнить импликацию. Если посылка ложна, то суждение истинно при любом следствии.

Но в качестве общих рассуждений не по теме замечу, что программа на ленивом языке применительно к императивной семантике и сайд эффектам — это формула, результатом вычисления которой является инструкция для исполнения.

При чем понятия «формула» и «вычисление» тут первичны, а исполнение сугубо вторично.

В языках наподобие C++ и C# при кажущейся похожести пассов руками первичным понятием является именно «исполнение», а не «вычисление». А «вычисление» возникает вследствие утилитарной попытки (порой тщетной) объяснить компилятору предметную область задачи. (В ЯП наподобие Python/Ruby/SmallTalk — вообще не возникает.)

Исходная версия wandrien, :

Почему не назвать это Nullptr, и буквально засунуть его внутрь типа NullablePointer = Pointer | Nullptr?

Потому что фактически это так и есть, но в языке с системой типов уровня Паскаля нет возможности выразить эту мысль.

Поэтому я иду снизу, от реализации: сначала в ЯП будут введены аналоги NullablePointer<a> и Pointer<a> в качестве типов из коробки, а уже потом - средства выражать идентичные концепции на языке типов.

Тут, кстати, есть забавное следствие несоответствия императивной и функциональной семантики.

В функциональной семантике выражение, типом которого является nulltype, является таким же законным выражением, как и любое другое. А поскольку nulltype заведомо не требует никакого вычисления, тело выражения может быть сразу свёрнуто до null.

А в императивной семантике функция, возвращающая результат типа nulltype, может иметь побочные эффекты.

Разрешение этого несоответствия требует введения понятия чистоты функции в ЯП.

В случае боттомов всё всегда сложнее. В ленивых языках боттом - это значение, да ещё (взмахивая руками) «любого типа». В энергичных это зачастую честный Never, без значений. И там и там произносятся похожие слова про невозвращаемость, но я не понимаю до конца, как обо всём этом думать. В теории типов, с которой я знаком, этот вопрос обходится стороной, по крайней мере при первом знакомстве. Дальше там как будто можно нагородить конструкции из refl’ов, но поля слишком узки.

Это на слишком сложном, пожалуй. Тут я пасс. Трактовка недостижимого значения как значения «любого типа» по смыслу заставляет вспомнить импликацию. Если посылка ложна, то суждение истинно независимо от следствия.

Но в качестве общих рассуждений не по теме замечу, что программа на ленивом языке применительно к императивной семантике и сайд эффектам — это формула, результатом вычисления которой является инструкция для исполнения.

При чем понятия «формула» и «вычисление» тут первичны, а исполнение сугубо вторично.

В языках наподобие C++ и C# при кажущейся похожести пассов руками первичным понятием является именно «исполнение», а не «вычисление». А «вычисление» возникает вследствие утилитарной попытки (порой тщетной) объяснить компилятору предметную область задачи. (В ЯП наподобие Python/Ruby/SmallTalk — вообще не возникает.)