LINUX.ORG.RU

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

Исправление 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.