Оба Agda и Idris эффективно запрещают сопоставление образцов по значениям типа Type. Кажется, что Агда всегда соответствует первому случаю, а Идрис просто бросает ошибку.
Итак, почему typecase плохой? Это нарушает согласованность? Мне не удалось найти много информации о теме.
Очень странно, что люди считают, что совпадение моделей по типам плохое. Мы получаем много пробега из соответствия шаблонов на данных, которые кодируют типы, всякий раз, когда мы строим вселенную. Если вы примете подход, в котором мы с Торстен Альтенкирх (и с которыми мои товарищи и я начали заниматься инженерами), типы образуют замкнутую вселенную, поэтому вам даже не нужно решать (откровенно стоящую) проблему вычисления с помощью открытые типы данных для обработки типов данных. Если бы мы могли напрямую сопоставлять соответствие типам, нам не нужна функция декодирования для сопоставления кодов типов с их значениями, что в худшем случае уменьшает беспорядок и в лучшем случае уменьшает необходимость доказывания и принуждения эквациональными законами о поведении декодирования функция. У меня есть все основания строить теорию закрытого типа без посредников. Конечно, вам нужны, чтобы типы уровня 0 занимали тип данных уровня 1. Это происходит, конечно, при построении индуктивно-рекурсивной иерархии юниверсов.
Но как насчет параметричности, я слышу, что вы спрашиваете?
Во-первых, мне не нужна параметричность, когда я пытаюсь написать типовой код. Не навязывайте мне параметричность.
Во-вторых, почему типы должны быть единственными параметрами, в которые мы входим? Почему мы не должны иногда быть параметрическими в других вещах, например, совершенно обычные индексы типа, которые обитают в типах данных, но которые мы бы предпочли не использовать во время выполнения? Это настоящая неприятность в том, что величины, которые играют роль только в спецификации, просто из-за их типа вынуждены присутствовать.
Тип домена не имеет ничего общего с тем, должна ли квантификация над ним быть параметрической.
Пусть (например, предложенный Бернарди и друзьями) дисциплина, в которой как параметрическая/стираемая, так и непараметрическая/сопоставимая количественная оценка различны и доступны. Тогда типы могут быть данными, и мы все еще можем сказать, что мы имеем в виду.
Многие люди считают, что сопоставление по типам не так плохо, потому что это ломает параметричность для типов.
На языке с параметризацией для типов, когда вы видите переменную
f : forall a . a -> a
вы сразу же знаете много о возможных значениях f. Интуитивно: поскольку функция f является функцией, ее можно записать:
f x = body
Тело должно быть типа a, но a неизвестно, поэтому единственным доступным значением типа a является x. Если язык допускает итерацию, f может также зацикливаться. Но может ли он сделать выбор между циклом или возвратом x на основе значения x? Нет, потому a неизвестно, f не знает, какие функции вызывать на x, чтобы принять решение. Таким образом, существует только два варианта: fx = x и fx = fx. Это мощная теорема о поведении f которую мы получаем, просто глядя на тип f. Подобное рассуждение работает для всех типов с универсальными квантованными переменными типа.
Теперь, если f может совпадать с типом a, возможны многие другие реализации f. Таким образом, мы потеряем мощную теорему.
В Agda вы не можете сопоставить образ на Set, потому что это не индуктивный тип.