Значения, типы, виды,... как бесконечную последовательность?

Я только начинаю знакомство с концепцией видов, так что несите меня, если я плохо формулирую свои вопросы...

Значения имеют типы:

3 :: Int
[1,2,3] :: [Int]
('c',True) :: (Char,Bool)

Типы имеют вид:

the type 'Int' has kind *
the type '[Int]' also has kind *
   but the type constructor [] has kind * -> *
similarly, the type (Char,Bool) has kind  *
   but the type constructor (,) has kind * -> * -> *

Что делают виды?

Есть ли у них виды ilk, или жанры, или породы, или разновидности?

Как далеко проходит эта последовательность абстракций? Мы останавливаемся, потому что у нас заканчиваются слова, или мы останавливаемся, потому что дальше дальше нет никакой ценности? Или, может быть, потому, что мы быстро достигаем пределов человеческого познания и просто не можем обернуть головы вокруг более высокоразвитых видов?

Связанный вопрос: языки дают нам конструкторы значений (например, оператор cons) для создания значений. Языки также дают нам типы-конструкторы типа (,) или [] для создания типов. Существуют ли какие-либо языки, которые предоставляют типы-конструкторы для создания видов?

Другой краевой случай, который мне интересен: у нас, по-видимому, есть тип, который не имеет значения, обозначается как ⊥, называемый "нижним типом". Есть ли вид, который не имеет типа: нижний вид?

Ответ 1

Терминология type и kind недостаточно масштабируется. Теоретики типа, так как Бертран Рассел использовал иерархию "типов". Одна из версий имеет то, что Integer : Type 0, Type 0 : Type 1, Type 1 : Type 2, ..., Type n : Type (n+1), .... В зависимых типизированных языках, таких как Coq и Agda, часто нужны эти "высшие сорта".

Уровни, подобные этому, полезны для избежания парадокса Рассела. Использование Type : Type имеет тенденцию вызывать противоречие (см. Quine для альтернативных проектов).

Это использование чисел - стандартная нотация, когда нам это нужно. Некоторые теории типов имеют понятие "кумулятивные виды", "кумулятивные уровни" или "кумулятивные виды", в которых говорится "if t : Type n then also t : Type (n+1)".

Кумулятивные уровни + "полиморфизм уровня" дают теорию почти такой же гибкой, как Type : Type, но избегают парадоксов. Coq делает уровни неявными в основном, хотя типы Set и Prop набраны как type, Type {1} : Type {2}. То есть вы обычно не видите числа, и большую часть времени он просто работает.

У Agda есть языковая прагма, которая обеспечивает уровень полиморфизма и делает вещи очень гибкими, но может быть немного бюрократичным (Agda, однако, обычно менее "бюрократична", чем Coq в других областях).

Другим хорошим словом является "вселенная".

Ответ 2

Вам, вероятно, следует прочитать статью Тима Шира о Омеге, диалекте Хаскелла с бесконечной башней типов/видов/сортов, но без полномасштабных зависимых типов. Это объясняет, почему вы хотите этого, и упоминает, что уровни выше "сортировки" на практике (по крайней мере до сих пор) не используются напрямую.