Ответ 1
Очень странно, что люди считают, что совпадение моделей по типам плохое. Мы получаем много пробега из соответствия шаблонов на данных, которые кодируют типы, всякий раз, когда мы строим вселенную. Если вы примете подход, в котором мы с Торстен Альтенкирх (и с которыми мои товарищи и я начали заниматься инженерами), типы образуют замкнутую вселенную, поэтому вам даже не нужно решать (откровенно стоящую) проблему вычисления с помощью открытые типы данных для обработки типов данных. Если бы мы могли напрямую сопоставлять соответствие типам, нам не нужна функция декодирования для сопоставления кодов типов с их значениями, что в худшем случае уменьшает беспорядок и в лучшем случае уменьшает необходимость доказывания и принуждения эквациональными законами о поведении декодирования функция. У меня есть все основания строить теорию закрытого типа без посредников. Конечно, вам нужны, чтобы типы уровня 0 занимали тип данных уровня 1. Это происходит, конечно, при построении индуктивно-рекурсивной иерархии юниверсов.
Но как насчет параметричности, я слышу, что вы спрашиваете?
Во-первых, мне не нужна параметричность, когда я пытаюсь написать типовой код. Не навязывайте мне параметричность.
Во-вторых, почему типы должны быть единственными параметрами, в которые мы входим? Почему мы не должны иногда быть параметрическими в других вещах, например, совершенно обычные индексы типа, которые обитают в типах данных, но которые мы бы предпочли не использовать во время выполнения? Это настоящая неприятность в том, что величины, которые играют роль только в спецификации, просто из-за их типа вынуждены присутствовать.
Тип домена не имеет ничего общего с тем, должна ли квантификация над ним быть параметрической.
Пусть (например, предложенный Бернарди и друзьями) дисциплина, в которой как параметрическая/стираемая, так и непараметрическая/сопоставимая количественная оценка различны и доступны. Тогда типы могут быть данными, и мы все еще можем сказать, что мы имеем в виду.