Restringir una variable derivada de una clase de tipo o una instancia

Question

Escribo una clase de tipo para mi biblioteca pipes para definir una interfaz abstracta a tipos similares a Proxy. El tipo de clase se ve algo como:

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 

También estoy escribiendo extensiones para el tipo Proxy que son de la forma:

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

... y me gustaría que estas instancias de poder para imponer una restricción adicional que si m es un Monad entonces p a' a b' b m es un Monad para todos a', a, b' y b.

Sin embargo, no tengo ni idea de cómo codificar limpiamente eso como una restricción ya sea para la clase ProxyC o para las instancias. La única solución actualmente que conozco es hacer algo como lo codifica en las firmas de los métodos de la clase:

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

... pero esperaba que habría una solución más simple y más elegante.

Editar: Y ni siquiera esa última solución funciona, ya que el compilador no deduce que (Monad (SomeExtension p a' a b' b m)) implica (Monad (p a' a b' b m)) para una elección específica de las variables, incluso cuando se administra el siguiente ejemplo:

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

Edición # 2: la siguiente solución que estoy considerando es sólo la duplicación de los métodos para la clase Monad dentro de la clase ProxyC:

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

... y luego instanciarlos con cada instancia ProxyC. Esto parece estar bien para mis propósitos, ya que los métodos Monad solo necesitan ser usados ​​internamente para la escritura de extensiones y el tipo original todavía tiene una instancia apropiada Monad para el usuario intermedio. Todo lo que hace es simplemente exponer los métodos Monad al escritor de instancias.

Answer 1

una manera bastante trivial para hacer esto es utilizar un GADT para mover la prueba al nivel de valor

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

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

tendrá que abrir explícitamente el diccionario siempre que se necesite que

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

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

la La táctica de usar GADT para pasar pruebas de proposiciones es realmente muy general.Si estás bien usando tipo de restricción, y no sólo GADTs, en su lugar puede utilizar el paquete de Edward Kmett Data.Constraint

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

que le permite definido

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

y luego utiliza un operador infijo de lujo para indicar al compilador dónde buscar la instancia mónada

... \\ getProxyMonad' 

de hecho, el tipo de vinculación :- forma una categoría (donde los objetos son estafa straints), y esta categoría tiene lotes de buena estructura, lo que quiere decir que es muy agradable hacer pruebas con.

p.s. ninguno de estos fragmentos son probados.

edición: también se podría combinar las pruebas de nivel de valor con un envoltorio newtype y no necesita abrir GADTs por todo el lugar

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 
    ... 

sospecho, pero obviamente no lo han probado, que esta realización también ser relativamente eficiente.