dependent type - Haciendo la cuantificación de rango-n en Idris

dependent-type higher-rank-types

Question

Solo puedo hacer tipos de rango-n en Idris 0.9.12 de una manera bastante torpe:

tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f _ a, f _ b)

Necesito los guiones bajos donde quiera que haya una aplicación de tipo, porque Idris arroja errores de análisis cuando intento que los argumentos de tipo (anidados) sean implícitos:

tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn''t compile

Un problema probablemente mayor es que no puedo hacer restricciones de clase en tipos de rango más alto en absoluto. No puedo traducir la siguiente función de Haskell a Idris:

appShow :: Show a => (forall a. Show a => a -> String) -> a -> String
appShow show x = show x

Esto también me impide usar las funciones de Idris como sinónimos de tipo para tipos como Lens , que es Lens stab = forall f. Functor f => (a -> fb) -> s -> ft Lens stab = forall f. Functor f => (a -> fb) -> s -> ft en Haskell.

¿Alguna forma de remediar o eludir los problemas anteriores?

Answer 1

Acabo de implementar esto en master, permitiendo implicaciones en ámbitos arbitrarios, y estará en la próxima versión de hackage. ¡Aún no está bien probado! Al menos he probado los siguientes ejemplos simples, y algunos otros:

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
appShow s x = s x

AppendType : Type
AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

append : AppendType
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f a, f b)

Proxy  : Type -> Type -> Type -> Type -> (Type -> Type) -> Type -> Type

Producer'' : Type -> (Type -> Type) -> Type -> Type
Producer'' a m t = {x'', x : _} -> Proxy x'' x () a m t

yield : Monad m => a -> Producer'' a m ()

La principal restricción en este momento es que no puede dar valores para argumentos implícitos directamente, excepto en el nivel superior. Voy a hacer algo al respecto con el tiempo ...