Facendo rango-n quantificazione in Idris

Question

posso fare solo i tipi di rango-n in Idris 0.9.12 in un modo piuttosto goffo:

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

ho bisogno di sottolineature dove c'è un tipo di applicazione, perché Idris getta analizzare errori quando provo a fare il (nested) tipo argomenti implicita:

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

Una questione probabilmente più grande è che non posso fare vincoli di classe nei tipi più alto rango a tutti. Non posso tradurre la seguente funzione Haskell Idris:

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

Questo mi impedisce anche di utilizzare le funzioni Idris come sinonimi tipo per tipi come Lens, che è Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t in Haskell.

Un modo per ovviare o aggirare i suddetti problemi?

Answer 1

Ho appena implementato questo in master, consentendo impliciti in ambiti arbitrari, e sarà nella prossima versione di hackage. Tuttavia non è ancora ben collaudato! Ho provato, almeno le seguenti semplici esempi, e pochi altri:

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

Il vincolo principale al minuto è che non si può dare valori per gli argomenti impliciti direttamente, se non a livello superiore. Alla fine ne farò qualcosa ...