История изменений
Исправление 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 — вообще не возникает.)