Vincolo di una variabile derivata di una classe di tipo o di un'istanza

Question

Sto scrivendo una classe di tipo per la mia libreria pipes per definire un'interfaccia astratta per tipi-Proxy -like. La classe di tipo simile a:

class ProxyC p where 
    idT :: (Monad m) => b' -> p a' a b' b m r 
    (<-<) :: (Monad m) 
      => (c' -> p b' b c' c m r) 
      -> (b' -> p a' a b' b m r) 
      -> (c' -> p a' a c' c m r) 
    ... -- other methods 

Sto anche scrivendo le estensioni per il tipo Proxy che sono di forma:

instance (ProxyC p) => ProxyC (SomeExtension p) where .... 

... e vorrei questi casi per essere in grado imporre un ulteriore vincolo che se m è p a' a b' b m per tutti a', a, b' e b.

Tuttavia, non ho idea di come codificarlo in modo pulito come un vincolo per la classe ProxyC o per le istanze. L'unica soluzione che attualmente conosco è quello di fare qualcosa di simile la codifica nelle firme dei metodi della classe:

(<-<) :: (Monad m, Monad (p b' b c' c m), Monad (p a' a b' b m)) 
      => (c' -> p b' b c' c m r) 
      -> (b' -> p a' a b' b m r) 
      -> (c' -> p a' a c' c m r) 

... ma speravo ci sarebbe una soluzione più semplice e più elegante.

Edit: E neppure che l'ultima soluzione funziona, dal momento che il compilatore non dedurre che (Monad (SomeExtension p a' a b' b m)) implica (Monad (p a' a b' b m)) per una precisa scelta di variabili, anche se dato il seguente esempio:

instance (Monad (p a b m)) => Monad (SomeExtension p a b m) where ... 

Modifica # 2: la soluzione successiva sto considerando è solo duplicare i metodi per la classe Monad all'interno della classe ProxyC:

class ProxyC p where 
    return' :: (Monad m) => r -> p a' a b' b m r 
    (!>=) :: (Monad m) => ... 

... e quindi istanzialo con ciascuna istanza ProxyC. Ciò sembra a posto per i miei scopi poiché i metodi Monad devono essere utilizzati solo internamente per la scrittura di estensioni e il tipo originale ha ancora un'istanza corretta Monad per l'utente downstream. Tutto ciò non fa altro che esporre i metodi Monad al writer di istanze.

Answer 1

un modo piuttosto banale per farlo è utilizzare un GADT per spostare la prova al livello di valore di

data IsMonad m where 
    IsMonad :: Monad m => IsMonad m 

class ProxyC p where 
    getProxyMonad :: Monad m => IsMonad (p a' a b' b m) 

è necessario aprire esplicitamente il dizionario ovunque ne abbiate bisogno

--help avoid type signatures 
monadOf :: IsMonad m -> m a -> IsMonad m 
monadOf = const 

--later on 
case getProxyMonad `monadOf` ... of 
    IsMonad -> ... 

la la tattica dell'uso di GADT per superare le dimostrazioni di proposizioni è davvero molto generale.Se si sta bene con i tipi di vincolo, e non solo GADTs, si può invece usare il pacchetto di Edward Kmett Data.Constraint

class ProxyC p where 
    getProxyMonad :: Monad m => Dict (Monad (p a' a b' b m)) 

che consente definito

getProxyMonad' :: ProxyC p => (Monad m) :- (Monad (p a' a b' b m)) 
getProxyMonad' = Sub getProxyMonad 

e quindi utilizzare un operatore infisso di fantasia per dire al compilatore dove cercare l'istanza monade

... \\ getProxyMonad' 

infatti, il tipo di implicazione :- forma una categoria (in cui gli oggetti sono con straints), e questa categoria ha lotti di bella struttura, che è dire che è piuttosto bello fare prove con.

p.s. nessuno di questi frammenti viene testato.

edit: si potrebbe anche combinare le prove di livello valore con un wrapper Newtype e non è necessario aprire GADTs tutto il luogo

newtype WrapP p a' a b' b m r = WrapP {unWrapP :: p a' a b' b m r} 

instance ProxyC p => Monad (WrapP p) where 
    return = case getProxyMonad of 
       Dict -> WrapP . return 
    (>>=) = case getProxyMonad of 
       Dict -> \m f -> WrapP $ (unWrapP m) >>= (unWrapP . f) 

instance ProxyC p => ProxyC (WrapP p) where 
    ... 

ho il sospetto, ma ovviamente non hanno testato, che questa implementazione sarà anche essere relativamente efficiente.