22
Mi pregunta es probablemente más fácil de explicar en forma de un ejemplo:devueltos localizados en el nivel de tipo Nat en GHC 7,6
type family Take (n :: Nat) (xs :: [k]) :: [k]
type instance Take 0 xs = '[]
type instance Take (n+1) (x ': xs) = x ': Take n xs
El segundo ejemplo que aquí se rechaza, sin embargo, porque (+), siendo una familia tipo en sí, no se puede usar en los argumentos. Pero no parece haber ningún Succ ni nada que se use generalmente para hacer coincidir Nats.
Entonces, ¿se puede expresar esto? y si es así, ¿cómo?
Actualización. Observé que las funciones isZero y isEven en GHC.TypeLits se encuentran bajo el encabezado "Destrucción de tipos". ¿Están destinados a ser utilizados en el nivel de tipo de alguna manera? Sospecho que no ... pero sobre todo porque no puedo ver cómo hacerlo. :)
Derecha. Acabo de instalar GHC 7.6 para poder verificar este código, y GHC señala los dos problemas que menciona en sus comentarios a continuación. Disculpas (Presioné el botón 'eliminar' en mi respuesta, así que ahora no puedo comentarlo directamente). – macron
Parece que codifica las condiciones de finalización ya que los argumentos pueden funcionar (ver https://gist.github.com/a39ce17ca47798b0f0ef) pero solo parece tener éxito cuando n == 1. Intenté esto en la rama type-nats, no en 7.6, entonces ymmv. –
Las funciones 'isZero' y' isEven' construyen las GADTs de nombre similar, que dan acceso al predicado de nivel de tipo en el nivel de término. En otras palabras, es una forma de hacer la coincidencia que desea en una función de nivel de término regular, en lugar de una función de tipo. : [ –