Почему имена образуют вид, а не только тип?

Question

Некоторое время назад в одном из расширений Haskell (не могу найти ссылку) и recently in Ur Я обнаружил, что имена (например, полей записи) образуют вид. Может ли кто-нибудь объяснить, почему абстракции типа для них недостаточно?

Answer 1

Ответ прост: они могут отображаться в типах. Следовательно, они должны жить на уровне типа (иначе вам понадобятся зависимые типы). И поскольку они живут на уровне типа, они классифицируются по типу.

Answer 2

Системы записи определяют правила для значений, типов и (возможно) видов. Какие правила используются, зависит от разрабатываемой системы типов и того, чего хочет достичь дизайнер.

E.g. в Haskell, звукозаписывающие является:

• значение (функции аксессоров)
• этих значений имеют типов (например Record -> Int)
• этих типов имеют виды (*)

Другие систем записи могут используйте систему типа или вида для разных целей.

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

Примером использования системы типов в Haskell является использование «unboxed types». Эти типы, которые имеют:

• разные представления во время выполнения для регулярных значений
• различные связывающие формы (например, не могут быть выделены в куче)

Для того, чтобы держать Unboxed типы смешивания в с регулярными типов, им присваивается другой вид , который позволяет компилятору отслеживать их разделение.

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