Elevación de una función de orden superior en Haskell

Question

Estoy tratando de construir una función de tipo:

liftSumthing :: ((a -> m b) -> m b) -> (a -> t m b) -> t m b 

donde t es un transformador mónada. En concreto, estoy interesado en hacer esto:

liftSumthingIO :: MonadIO m => ((a -> IO b) -> IO b) -> (a -> m b) -> m b 

Jugueteé con algunas librerías hechicería y Haskell, pero en vano. ¿Cómo lo consigo a la derecha, o tal vez hay una solución lista en alguna parte que no encontré?

Answer 1

Esto no se puede hacer genéricamente en todas las instancias MonadIO porque el tipo IO está en una posición negativa. Hay algunas bibliotecas en hackage que hacen esto para instancias específicas (monad-control,), pero ha habido cierto debate sobre si son semánticamente correctas, especialmente con respecto a cómo manejan excepciones y cosas similares.

Editar: Algunas personas parecen interesadas en la distinción de posición positiva/negativa. En realidad, no hay mucho para decir (y probablemente ya lo haya escuchado, pero con un nombre diferente). La terminología proviene del mundo de la subtipificación.

La intuición detrás de subtipos es que "a es un subtipo de b (que voy a escribir a <= b) cuando un a se puede utilizar en cualquier lugar de una b se esperaba en su lugar". Decidir la subtipificación es sencillo en muchos casos; para los productos, (a1, a2) <= (b1, b2) cada vez que a1 <= b1 y a2 <= b2, por ejemplo, que es una regla muy sencilla. Pero hay algunos casos difíciles; por ejemplo, ¿cuándo deberíamos decidir a1 -> a2 <= b1 -> b2?

Bueno, tenemos una función f :: a1 -> a2 y un contexto que espera una función del tipo b1 -> b2. Entonces, el contexto va a usar el valor de retorno f como si fuera un b2, por lo tanto, debemos requerir que a2 <= b2. Lo más complicado es que el contexto va a suministrar f con b1, aunque f lo va a usar como si fuera a1. Por lo tanto, debemos exigir que b1 <= a1 - que mira hacia atrás desde lo que pueda adivinar! Decimos que a2 y b2 son "covariantes", u ocurren en una "posición positiva", y a1 y b1 son "contravariantes", u ocurren en una "posición negativa".

(Quick lado: ¿por qué? "Positivo" y "negativo" Está motivado por la multiplicación Considere estos dos tipos:.

f1 :: ((a1 -> b1) -> c1) -> (d1 -> e1) 
f2 :: ((a2 -> b2) -> c2) -> (d2 -> e2) 

Cuando debería f1 'tipo s ser un subtipo de f2' tipo s que? declarar estos hechos (ejercicio: comprobar esto usando la regla anterior):

• debemos tener e1 <= e2
• que deberíamos haber d2 <= d1
..
• Deberíamos tener c2 <= c1.
• Deberíamos tener b1 <= b2.
• Deberíamos tener a2 <= a1.

e1 está en una posición positiva en d1 -> e1, que es a su vez en una posición positiva en el tipo de f1; además, e1 está en una posición positiva en el tipo de f1 en general (ya que es covariante, por el hecho anterior). Su posición en todo el término es el producto de su posición en cada uno de los subterm: positivo * positivo = positivo. Del mismo modo, d1 está en una posición negativa en d1 -> e1, que está en una posición positiva en todo el tipo. negativo * positivo = negativo, y las variables d son de hecho contravariantes. b1 está en una posición positiva en el tipo a1 -> b1, que está en una posición negativa en (a1 -> b1) -> c1, que está en una posición negativa en todo el tipo. positivo * negativo * negativo = positivo, y es covariante. Se entiende la idea)

Ahora, vamos a echar un vistazo a la clase MonadIO:.

class Monad m => MonadIO m where 
    liftIO :: IO a -> m a 

Podemos ver esto como una declaración explícita de los subtipos: Estamos dando una manera de hacer IO a ser un subtipo de m a para un poco de concreto m. De inmediato sabemos que podemos tomar cualquier valor con IO constructores en posiciones positivas y convertirlos en m s. Pero eso es todo: no tenemos forma de convertir constructores negativos de IO en m s; necesitamos una clase más interesante para eso.