agda - ¿Por qué Typecase es algo malo?
dependent-type idris (3)
Tanto Agda como Idris prohíben efectivamente la coincidencia de patrones en valores del tipo Type . Parece que Agda siempre coincide en el primer caso, mientras que Idris simplemente arroja un error.
Entonces, ¿por qué typecase es algo malo? ¿Rompe la consistencia? No he podido encontrar mucha información sobre el tema.
En Agda, no se puede emparejar patrones en Set porque no es un tipo inductivo.
Es realmente extraño que la gente piense que la coincidencia de patrones en tipos es mala. Obtenemos un gran kilometraje de la coincidencia de patrones en los datos que codifican tipos, cada vez que hacemos una construcción del universo. Si adoptas el enfoque que Thorsten Altenkirch y yo fuimos pioneros (y que mis camaradas y yo comenzamos a diseñar), los tipos forman un universo cerrado , por lo que ni siquiera necesitas resolver el problema (francamente vale la pena resolver) de la informática con abrir tipos de datos para tratar tipos como datos. Si pudiéramos hacer coincidir patrones en tipos directamente, no necesitaríamos una función decodificadora para asignar códigos de tipo a sus significados, lo que en el peor de los casos reduce el desorden y, en el mejor de los casos, reduce la necesidad de probar y obligar por leyes ecuacionales sobre el comportamiento de decodificación función. Tengo toda la intención de construir una teoría de tipos cerrada sin intermediarios de esta manera. Por supuesto, necesita que los tipos de nivel 0 habitan en un tipo de datos de nivel 1. Eso sucede como una cuestión de rutina cuando construyes una jerarquía recursiva inductiva del universo.
Pero ¿qué pasa con la parametricidad, oí que preguntas?
En primer lugar, no quiero la parametricidad cuando intento escribir un código genérico. No me fuerce la parametricidad.
En segundo lugar, ¿por qué deberían los tipos ser las únicas cosas en las que estamos paramétricos? ¿Por qué no deberíamos ser paramétricos en otras cosas, por ejemplo, índices de tipos perfectamente ordinarios que habitan en tipos de datos pero que preferiríamos no tener en tiempo de ejecución? Es una verdadera molestia que las cantidades que solo juegan un papel en la especificación se vean obligadas, por su tipo, a estar presentes.
El tipo de dominio no tiene nada que ver con si la cuantificación debería ser paramétrica.
Tengamos (por ejemplo, como lo propusieron Bernardy y sus amigos) una disciplina en la que la cuantificación paramétrica / borrable y no paramétrica / compatible sea distinta y ambas estén disponibles. Entonces los tipos pueden ser datos y aún podemos decir lo que queremos decir.
Muchas personas ven la coincidencia en los tipos como mala porque rompe la parametrización de los tipos.
En un lenguaje con parametricidad para tipos, cuando ve una variable
f : forall a . a -> a
inmediatamente sabes mucho sobre los posibles valores de f . Intuitivamente: como f es una función, se puede escribir:
f x = body
El cuerpo debe ser del tipo a , pero a es desconocido, por lo que el único valor disponible de tipo a es x . Si el lenguaje permite la no determinación, f también podría repetirse. ¿Pero puede hacer la elección entre bucle o devolver x función del valor de x ? No, porque a se desconoce, f no sabe a qué funciones llamar en x para tomar la decisión. Entonces, realmente solo hay dos opciones: fx = x y fx = fx . Este es un poderoso teorema sobre el comportamiento de f que obtenemos solo mirando el tipo de f . Un razonamiento similar funciona para todos los tipos con variables de tipo universalmente cuantificadas.
Ahora bien, si f puede coincidir en el tipo a , muchas más implementaciones de f son posibles. Entonces perderíamos el poderoso teorema.