Пример «Типа 1», который не является ни «Типом», ни обитателем «Типа».

Каков пример жителя Type 1, который не является ни Type, ни жителем Type? Я не мог ничего придумать, исследуя Idris REPL.

Чтобы быть более точным, я ищу некоторые x, отличные от Type, которые дают следующее:

Idris> :t x
x : Type 1

dependent-type idris
person Snowball    schedule 12.11.2014    source источник

Ответы (2)


arrow_upward
7
arrow_downward

Я не специалист по теории типов, но вот мое понимание. В руководстве по Idris есть раздел 12.8 Кумулятивность< /сильный>. В нем говорится, что существует внутренняя иерархия вселенных типов:

Type : Type 1 : Type 2 : Type 3 : ...

И для любого x : Type n подразумевается x : Type m для любого m > n. Также есть пример, демонстрирующий, как это предотвращает возможные циклы в выводе типа.

Но я думаю, что эта иерархия только для внутреннего пользования и нет возможности создать значение Type (n+1) которого нет в Type n.

См. также статьи в nLab об юниверсах в теории типов и о тип типов.

Возможно, эта ошибка в репозитории idris-dev тоже может оказаться полезной. Эдвин Брейди ссылается на документ по проектированию и реализации (см. раздел 3.2.2). ).

person laughedelic    schedule 12.11.2014

arrow_upward
5
arrow_downward

Я не эксперт по Идрису, но я ожидаю, что

Type -> Type

также находится в Type 1.

я бы тоже ожидал

Nat -> Type

и если очень повезет (в этом не уверен)

List Type

быть таким большим.

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

person pigworker    schedule 12.11.2014
comment
Я не уверен, что Идрис раскрывает программисту слишком много информации об Type уровнях. Type : Type 1, вероятно, только потому, что Type : Type является противоречием. - person Ramon Snir; 12.11.2014
comment
Type -> Type действительно находится в Type 1, но также и в Type (как заметил Рамон). То же самое верно для Nat -> Type и List Type. - person Snowball; 12.11.2014
comment
Я бы проверил сам, но клика install idris угрожает сломать пакеты, которые мне нужны для критически важного программного обеспечения. Я думаю, что есть два отдельных вопроса: к какому уровню относится тип? и сколько информации об уровне отображает Идрис? - person pigworker; 13.11.2014
comment
Все, что делает Идрис, — это строит граф ограничений и проверяет отсутствие циклов. Тип : Тип 1 - это взлом дисплея, потому что люди продолжали сообщать, что это было несоответствие, и мне надоело объяснять это... - person Edwin Brady; 13.11.2014
comment
@Edwin: Это ответ, который я искал. Спасибо! - person Snowball; 13.11.2014