Doing Rang-n Quantifizierung in Idris

Question

Ich kann nur Rang-n-Typen in Idris 0.9.12 in einer ziemlich unbeholfen Weise tun:

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

ich die Unterstrichen müssen überall dort, wo eine Art Anwendung ist, weil Idris analysieren wirft Fehler, wenn ich versuche, die (verschachtelten) Typen Argumente implizit zu machen:

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

A wahrscheinlich größeres Problem ist, dass ich nicht Klasse Einschränkungen in höherrangigen Typen überhaupt tun kann. Ich kann die folgende Haskell Funktion Idris übersetzen:

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

Das bin ich auch mit Idris Funktionen als Typ Synonyme verhindert für Typen wie Lens, die Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t in Haskell ist.

Jede Möglichkeit, die oben genannten Probleme zu beheben oder zu umgehen?

Answer 1

Ich habe dies gerade in Master implementiert, so dass es in beliebige Bereiche impliziert, und es wird in der nächsten Hack-Release sein. Es ist aber noch nicht gut getestet! Ich habe zumindest die folgenden einfachen Beispiele versucht, und ein paar andere:

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() 

Das Haupthindernis in der Minute ist, dass Sie nicht Werte für implizite Argumente direkt, außer auf der obersten Ebene geben können. Ich werde etwas dagegen tun ...