История изменений
Исправление quasimoto, (текущая версия) :
nothing_t это такой тип, что nothing_t x; нельзя инициализировать и вообще у x нет «нормального» смыла и такая переменная не должна появляться и должна быть запрещена в compile-time, то есть это универсальный подтип — оно подтип и bool и int и вообще чего угодно, поэтому нельзя сказать что существуют какие-то нормальные элементы у типа nothing_t, так как тогда они должны принадлежать _всем_ типам (а вот у T array[0] есть один хороший элемент и его можно инициализировать пустым списком инициализации, как и создать переменную такого типа — не nothing_t), у него могут быть «ненормальные» элементы если у _всех_ других типов они есть (функции возвращающие int, bool и т.п. могут падать и зависать, например, — это ненормальные значения, в отличии от хороших false, true, 0, ...) и нужен он для того чтобы быть критерием такой «ненормальности». Например, если есть завершающаяся функция nothing_t foo(some_t), то some_t такой же ненормальный как и nothing_t (аналогично — отображение из множества A в пустое множество существует тогда и только тогда, когда A само пусто), или — для нормального array<nothing_t, 0> xs; xs[j] имеет тип nothing_t то есть ненормален и недопустим прямо в compile-time, или так — функция из нормальных типов в ненормальный вида nothing_t! loop(ok_t, ...) будет вменяемой только если она никогда не вернёт управление — так можно типизировать функции для которых нужно в compile-time запретить завершаемость и получение результата (где ! это оговорка про необходимость ввести effect types коиндукцию/корекурсию для таких вещей).
Теория типов: нормальный ~ населённый тип, ненормальный — ненаселённый.
Логика: нормальный тип ~ истинное утверждение, ненормальный — ложное, nothing_t — ⊥ (arbitrary contradiction), foo — отрицание (¬ φ = φ → ⊥).
В C++ есть велосипед для универсального супертипа в виде boost::any, в динамических языках в нём вообще вся соль, но универсальный подтип bottom явно никому не нужен :)
Но вот в скалу он уже попал — http://www.scala-lang.org/node/128.
Исправление quasimoto, :
nothing_t это такой тип, что nothing_t x; нельзя инициализировать и вообще у x нет «нормального» смыла и такая переменная не должна появляться и должна быть запрещена в compile-time, то есть это универсальный подтип — оно подтип и bool и int и вообще чего угодно, поэтому нельзя сказать что существуют какие-то нормальные элементы у типа nothing_t, так как тогда они должны принадлежать _всем_ типам (а вот у T array[0] есть один хороший элемент и его можно инициализировать пустым списком инициализации, как и создать переменную такого типа — не nothing_t), у него могут быть «ненормальные» элементы если у _всех_ других типов они есть (функции возвращающие int, bool и т.п. могут падать и зависать, например, — это ненормальные значения, в отличии от хороших false, true, 0, ...) и нужен он для того чтобы быть критерием такой «ненормальности». Например, если есть завершающаяся функция nothing_t foo(some_t), то some_t такой же ненормальный как и nothing_t (аналогично — отображение из множества A в пустое множество существует тогда и только тогда, когда A само пусто), или — для нормального array<nothing_t, 0> xs; xs[j] имеет тип nothing_t то есть ненормален и недопустим прямо в compile-time, или так — функция из нормальных типов в ненормальный вида nothing_t! loop(ok_t, ...) будет вменяемой только если она никогда не вернёт управление — так можно типизировать функции для которых нужно в compile-time запретить завершаемость и получение результата (где ! это оговорка про необходимость ввести effect types для таких вещей).
Теория типов: нормальный ~ населённый тип, ненормальный — ненаселённый.
Логика: нормальный тип ~ истинное утверждение, ненормальный — ложное, nothing_t — ⊥ (arbitrary contradiction), foo — отрицание (¬ φ = φ → ⊥).
В C++ есть велосипед для универсального супертипа в виде boost::any, в динамических языках в нём вообще вся соль, но универсальный подтип bottom явно никому не нужен :)
Но вот в скалу он уже попал — http://www.scala-lang.org/node/128.
Исходная версия quasimoto, :
nothing_t это такой тип, что nothing_t x; нельзя инициализировать и вообще у x нет «нормального» смыла и такая переменная не должна появляться и должна быть запрещена в compile-time, то есть это универсальный подтип — оно подтип и bool и int и вообще чего угодно, поэтому нельзя сказать что существуют какие-то нормальные элементы у типа nothing_t, так как тогда они должны принадлежать _всем_ типам (а вот у T array[0] есть один хороший элемент и его можно инициализировать пустым списком инициализации, как и создать переменную такого типа — не nothing_t), у него могут быть «ненормальные» элементы если у _всех_ других типов они есть (функции возвращающие int, bool и т.п. могут падать и зависать, например, — это ненормальные значения, в отличии от хороших false, true, 0, ...) и нужен он для того чтобы быть критерием такой «ненормальности». Например, если есть завершающаяся функция nothing_t foo(some_t), то some_t такой же ненормальный как и nothing_t (аналогично — отображение из множества A в пустое множество существует тогда и только тогда, когда A само пусто), или — для нормального array<nothing_t, 0> xs; xs[j] имеет тип nothing_t то есть ненормален и недопустим прямо в compile-time, или так — функция из нормальных типов в ненормальный вида nothing_t loop(ok_t, ...) будет вменяемой только если она никогда не вернёт управление — так можно типизировать функции для которых нужно в compile-time запретить завершаемость и получение результата.
Теория типов: нормальный ~ населённый тип, ненормальный — ненаселённый.
Логика: нормальный тип ~ истинное утверждение, ненормальный — ложное, nothing_t — ⊥ (arbitrary contradiction), foo — отрицание (¬ φ = φ → ⊥).
В C++ есть велосипед для универсального супертипа в виде boost::any, в динамических языках в нём вообще вся соль, но универсальный подтип bottom явно никому не нужен :)
Но вот в скалу он уже попал — http://www.scala-lang.org/node/128.