haskell - preestablecida - monadologia leibniz pdf
¿Se puede ejecutar una mónada tipo `ST` puramente(sin la biblioteca` ST`)? (3)
Esta publicación es Haskell alfabetizada. Simplemente coloque un archivo como "pad.lhs" y ghci podrá ejecutarlo.
> {-# LANGUAGE GADTs, Rank2Types #-}
> import Control.Monad
> import Control.Monad.ST
> import Data.STRef
Bien, entonces pude imaginar cómo representar la mónada ST en código puro. Primero comenzamos con nuestro tipo de referencia. Su valor específico no es realmente importante. Lo más importante es que PT sa no debe ser isomorfo a ningún otro tipo para todos. (En particular, debe ser isomorfo para ni () ni Void ).
> newtype PTRef s a = Ref {unref :: s a} -- This is defined liked this to make `toST''` work. It may be given a different definition.
El tipo de s es *->* , pero eso no es realmente importante en este momento. Podría ser polykind , por todo lo que nos importa.
> data PT s a where
> MkRef :: a -> PT s (PTRef s a)
> GetRef :: PTRef s a -> PT s a
> PutRef :: a -> PTRef s a -> PT s ()
> AndThen :: PT s a -> (a -> PT s b) -> PT s b
Muy claro. AndThen nos permite usar esto como una Monad . Usted se estará preguntando cómo se implementa el return . Aquí está su instancia de mónada (solo respeta las leyes de mónada con respecto a runPF , que se definirá más adelante):
> instance Monad (PT s) where
> (>>=) = AndThen
> return a = AndThen (MkRef a) GetRef --Sorry. I like minimalism.
> instance Functor (PT s) where
> fmap = liftM
> instance Applicative (PT s) where
> pure = return
> (<*>) = ap
Ahora podemos definir fib como un caso de prueba.
> fib :: Int -> PT s Integer
> fib n = do
> rold <- MkRef 0
> rnew <- MkRef 1
> replicateM_ n $ do
> old <- GetRef rold
> new <- GetRef rnew
> PutRef new rold
> PutRef (old+new) rnew
> GetRef rold
Y escribe cheques. ¡Viva! Ahora, pude convertir esto a ST (ahora vemos por qué s tenía que ser * -> * )
> toST :: PT (STRef s) a -> ST s a
> toST (MkRef a ) = fmap Ref $ newSTRef a
> toST (GetRef (Ref r)) = readSTRef r
> toST (PutRef a (Ref r)) = writeSTRef r a
> toST (pa `AndThen` apb) = (toST pa) >>= (toST . apb)
Ahora podemos definir una función para ejecutar PT sin hacer referencia alguna a ST :
> runPF :: (forall s. PT s a) -> a
> runPF p = runST $ toST p
runPF $ fib 7 da 13 , que es correcto.
Mi pregunta es si podemos definir runPF sin referencia utilizando ST en absoluto?
¿Hay una forma pura de definir runPF ? La definición de PTRef completo de importancia; es solo un tipo de marcador de posición de todos modos. Se puede redefinir a lo que sea que lo haga funcionar.
Si no puede definir runPF puramente, dé una prueba de que no puede.
El rendimiento no es una preocupación (si lo fuera, no habría hecho que cada return tuviera su propia referencia).
Estoy pensando que los tipos existenciales pueden ser útiles.
Nota: Es trivial si suponemos que es dinámicamente o algo así. Estoy buscando una respuesta que funcione con todos a .
Nota: De hecho, una respuesta ni siquiera necesariamente tiene mucho que ver con PT . Solo necesita ser tan poderoso como ST sin usar magia. (La conversión de (forall s. PT s) es una especie de prueba de si una respuesta es válida o no).
Una solución simple es envolver una mónada de State y presentar la misma API que ST . En este caso, no es necesario almacenar información del tipo de tiempo de ejecución, ya que se puede determinar a partir del tipo de STRef -s, y el truco de cuantificación habitual de ST s nos permite evitar que los usuarios dañen el contenedor que almacena las referencias.
Mantenemos ref-s en un IntMap e incrementamos un contador cada vez que IntMap una nueva referencia. La lectura y la escritura solo modifican el IntMap con un poco de unsafeCoerce salpicado encima.
{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes, RoleAnnotations #-}
module PureST (ST, STRef, newSTRef, readSTRef, modifySTRef, runST) where
import Data.IntMap (IntMap, (!))
import qualified Data.IntMap as M
import Control.Monad
import Control.Applicative
import Control.Monad.Trans.State
import GHC.Prim (Any)
import Unsafe.Coerce (unsafeCoerce)
type role ST nominal representational
type role STRef nominal representational
newtype ST s a = ST (State (IntMap Any, Int) a) deriving (Functor, Applicative, Monad)
newtype STRef s a = STRef Int deriving Show
newSTRef :: a -> ST s (STRef s a)
newSTRef a = ST $ do
(m, i) <- get
put (M.insert i (unsafeCoerce a) m, i + 1)
pure (STRef i)
readSTRef :: STRef s a -> ST s a
readSTRef (STRef i) = ST $ do
(m, _) <- get
pure (unsafeCoerce (m ! i))
writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef (STRef i) a = ST $
modify $ /(m, i'') -> (M.insert i (unsafeCoerce a) m, i'')
modifySTRef :: STRef s a -> (a -> a) -> ST s ()
modifySTRef (STRef i) f = ST $
modify $ /(m, i'') -> (M.adjust (unsafeCoerce f) i m, i'')
runST :: (forall s. ST s a) -> a
runST (ST s) = evalState s (M.empty, 0)
foo :: Num a => ST s (a, Bool)
foo = do
a <- newSTRef 0
modifySTRef a (+100)
b <- newSTRef False
modifySTRef b not
(,) <$> readSTRef a <*> readSTRef b
Ahora podemos hacer:
> runST foo
(100, True)
Pero lo siguiente falla con el error de tipo ST habitual:
> runST (newSTRef True)
Por supuesto, el esquema anterior nunca basura recopila referencias, sino que libera todo en cada llamada runST . Creo que un sistema más complejo podría implementar múltiples regiones distintas, cada una etiquetada por un parámetro de tipo, y asignar / liberar recursos de una manera más refinada.
Además, el uso de unsafeCoerce significa aquí que el uso de elementos internos directamente es tan peligroso como usar las GHC.ST internas de GHC.ST y el State# directamente, por lo que deberíamos asegurarnos de presentar una API segura y también probar nuestras piezas internas a fondo (de lo contrario, podemos obtener segfaults en Haskell, un gran pecado).
Desde que publiqué mi respuesta anterior , indicó que no le importa hacer cambios en su definición de PT . Me complace informar: relajar esa restricción cambia la respuesta a su pregunta de no a ¡ sí ! Ya he argumentado que necesita indexar su mónada por el conjunto de tipos en su medio de almacenamiento, así que aquí hay un código de trabajo que muestra cómo hacerlo. (Originalmente tuve esto como una edición de mi respuesta anterior, pero pasó demasiado tiempo, así que aquí estamos).
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeOperators #-}
import Prelude
Vamos a necesitar una clase de Monad más inteligente que la del Preludio: la de las cosas indexadas tipo mónada que describen las rutas a través de un gráfico dirigido. Por razones que deberían ser evidentes, voy a definir funtores indexados también.
class FunctorIx f where
imap :: (a -> b) -> f i j a -> f i j b
class FunctorIx m => MonadIx m where
ireturn :: a -> m i i a
(>>>=) :: m i j a -> (a -> m j k b) -> m i k b
(>>>) :: MonadIx m => m i j a -> m j k b -> m i k b
ma >>> mb = ma >>>= /_ -> mb
replicateM_ :: MonadIx m => Int -> m i i a -> m i i ()
replicateM_ 0 _ = ireturn ()
replicateM_ n m = m >>> replicateM_ (n - 1) m
Una mónada indexada usa el sistema de tipo para rastrear el progreso de un cálculo con estado. mija es un cálculo monádico que requiere un estado de entrada de i , cambia el estado a j y produce un valor de tipo a . La secuenciación de mónadas indexadas con >>>= es como jugar al dominó. Puede alimentar un cálculo que toma el estado de i a j en un cálculo que va de j a k , y obtener un mayor cálculo de i a k . (Hay una versión más rica de esta mónada indexada descrita en Kleisli Arrows of Outrageous Fortune ( y en otros lugares ), pero esta es suficiente para nuestros propósitos).
Una posibilidad con MonadIx es una mónada de File que rastrea el estado de un identificador de archivo, asegurando que no se olvide de liberar recursos. fOpen :: File Closed Open () comienza con un archivo cerrado y lo abre, fRead :: File Open Open String devuelve el contenido de un archivo abierto, y fClose :: File Open Closed () toma un archivo de abierto a cerrado. La operación de run requiere un cálculo del tipo File Closed Closed a , que asegura que los manejadores de sus archivos siempre se limpien.
Pero estoy divagando: aquí no nos preocupamos por un identificador de archivo sino por un conjunto de "ubicaciones de memoria" tipadas; los tipos de cosas en el banco de memoria de la máquina virtual son lo que usaremos para los índices de la mónada. Me gusta obtener mónadas de "programa / intérprete" de forma gratuita porque expresa el hecho de que los resultados viven en las hojas de un cómputo, y promueve la capacidad de compilación y la reutilización de código, así que aquí está el funtor que producirá PT cuando lo FreeIx a FreeIx :
data PTF ref as bs r where
MkRef_ :: a -> (ref (a '': as) a -> r) -> PTF ref as (a '': as) r
GetRef_ :: ref as a -> (a -> r) -> PTF ref as as r
PutRef_ :: a -> ref as a -> r -> PTF ref as as r
instance FunctorIx (PTF ref) where
imap f (MkRef_ x next) = MkRef_ x (f . next)
imap f (GetRef_ ref next) = GetRef_ ref (f . next)
imap f (PutRef_ x ref next) = PutRef_ x ref (f next)
PTF está parametrizado por el tipo de referencia ref :: [*] -> * -> * - las referencias permiten saber qué tipos están en el sistema e indexados por la lista de tipos almacenados en la "memoria" del intérprete. El caso interesante es MkRef_ : hacer una nueva referencia agrega un valor de tipo a a la memoria, tomando as a '': as ; la continuación espera una ref en el entorno extendido. Las otras operaciones no cambian la lista de tipos en el sistema.
Cuando creo referencias secuencialmente ( x <- mkRef 1; y <- mkRef 2 ), tendrán diferentes tipos: la primera será una ref (a '': as) a y la segunda será una ref (b '': a '': as) b . Para alinear los tipos, necesito una forma de usar una referencia en un entorno más grande que aquel en el que se creó. En general, esta operación depende del tipo de referencia, así que la incluiré en una clase.
class Expand ref where
expand :: ref as a -> ref (b '': as) a
Una posible generalización de esta clase resumiría el patrón de aplicaciones repetidas de expand , con un tipo como inflate :: ref as a -> ref (bs :++: as) a .
Aquí hay otra parte de infraestructura reutilizable, la mónada libre indexada que mencioné anteriormente. FreeIx convierte un funtor indexado en una mónada indexada al proporcionar una operación de unión alineada con el tipo Free , que vincula el nudo recursivo en el parámetro del functor, y una operación de no hacer nada en Pure .
data FreeIx f i j a where
Pure :: a -> FreeIx f i i a
Free :: f i j (FreeIx f j k a) -> FreeIx f i k a
lift :: FunctorIx f => f i j a -> FreeIx f i j a
lift f = Free (imap Pure f)
instance FunctorIx f => MonadIx (FreeIx f) where
ireturn = Pure
Pure x >>>= f = f x
Free love {- , man -} >>>= f = Free $ imap (>>>= f) love
instance FunctorIx f => FunctorIx (FreeIx f) where
imap f x = x >>>= (ireturn . f)
Una desventaja de las mónadas libres es la plantilla que debe escribir para que trabajar con Free y Pure sea más fácil. Aquí hay algunos PTs de acción simple que forman la base de la API de la mónada, y algunos sinónimos de patrones para ocultar los constructores Free cuando desempaquetamos valores de PT .
type PT ref = FreeIx (PTF ref)
mkRef :: a -> PT ref as (a '': as) (ref (a '': as) a)
mkRef x = lift $ MkRef_ x id
getRef :: ref as a -> PT ref as as a
getRef ref = lift $ GetRef_ ref id
putRef :: a -> ref as a -> PT ref as as ()
putRef x ref = lift $ PutRef_ x ref ()
pattern MkRef x next = Free (MkRef_ x next)
pattern GetRef ref next = Free (GetRef_ ref next)
pattern PutRef x ref next = Free (PutRef_ x ref next)
Eso es todo lo que necesitamos para poder escribir cálculos PT . Aquí está tu ejemplo fib . Estoy usando RebindableSyntax y redefiniendo localmente los operadores de mónada (a sus equivalentes indexados) para poder usar la notación do en mi mónada indexada.
-- fib adds two Ints to an arbitrary environment
fib :: Expand ref => Int -> PT ref as (Int '': Int '': as) Int
fib n = do
rold'' <- mkRef 0
rnew <- mkRef 1
let rold = expand rold''
replicateM_ n $ do
old <- getRef rold
new <- getRef rnew
putRef new rold
putRef (old+new) rnew
getRef rold
where (>>=) = (>>>=)
(>>) = (>>>)
return :: MonadIx m => a -> m i i a
return = ireturn
fail :: MonadIx m => String -> m i j a
fail = error
Esta versión de fib ve exactamente como la que quería escribir en la pregunta original. La única diferencia (aparte de las vinculaciones locales de >>= y así sucesivamente) es la llamada a expand . Cada vez que creas una nueva referencia, tienes que expand todas las antiguas, lo cual es un poco tedioso.
Finalmente, podemos finalizar el trabajo que nos propusimos hacer y construir una máquina PT que utilice una Tuple como medio de almacenamiento y Elem como el tipo de referencia.
infixr 5 :>
data Tuple as where
E :: Tuple ''[]
(:>) :: a -> Tuple as -> Tuple (a '': as)
data Elem as a where
Here :: Elem (a '': as) a
There :: Elem as a -> Elem (b '': as) a
(!) :: Tuple as -> Elem as a -> a
(x :> xs) ! Here = x
(x :> xs) ! There ix = xs ! ix
updateT :: Elem as a -> a -> Tuple as -> Tuple as
updateT Here x (y :> ys) = x :> ys
updateT (There ix) x (y :> ys) = y :> updateT ix x ys
Para usar un Elem en una tupla más grande que la que construiste, solo necesitas hacer que se vea más abajo en la lista.
instance Expand Elem where
expand = There
Tenga en cuenta que esta implementación de Elem es más bien un índice de Bruijn: las variables de límite más reciente tienen índices más pequeños.
interp :: PT Elem as bs a -> Tuple as -> a
interp (MkRef x next) tup = let newTup = x :> tup
in interp (next $ Here) newTup
interp (GetRef ix next) tup = let x = tup ! ix
in interp (next x) tup
interp (PutRef x ix next) tup = let newTup = updateT ix x tup
in interp next newTup
interp (Pure x) tup = x
Cuando el intérprete encuentra una solicitud MkRef , aumenta el tamaño de su memoria al agregar x al frente. El comprobador de tipos le recordará que cualquier ref de antes de MkRef debe expand correctamente, por lo que las referencias existentes no se desvanecen cuando la tupla cambia de tamaño. Pagamos un intérprete sin yesos inseguros, pero tenemos integridad referencial para arrancar.
Ejecutar desde un inicio permanente requiere que el cómputo PT comience con un banco de memoria vacío, pero permitimos que termine en cualquier estado.
run :: (forall ref. Expand ref => PT ref ''[] bs a) -> a
run x = interp x E
Tipea, pero ¿funciona?
ghci> run (fib 5)
5
ghci> run (fib 3)
2
tl; dr: no es posible sin ajustes a la definición de PT . Este es el problema principal: ejecutará su cálculo con estado en el contexto de algún tipo de medio de almacenamiento, pero dicho medio de almacenamiento debe saber cómo almacenar tipos arbitrarios . Esto no es posible sin empaquetar algún tipo de evidencia en el constructor MkRef , ya sea un diccionario Typeable envuelto existencialmente como otros han sugerido, o una prueba de que el valor pertenece a uno de un conjunto finito conocido de tipos.
Para un primer intento, intentemos usar una lista como medio de almacenamiento y enteros para referirnos a los elementos de la lista.
newtype Ix a = MkIx Int -- the index of an element in a list
interp :: PT Ix a -> State [b] a
interp (MkRef x) = modify (++ [x]) >> gets (Ref . MkIx . length)
-- ...
Al almacenar un nuevo elemento en el entorno, nos aseguramos de agregarlo al final de la lista, de modo que los Ref que hemos distribuido permanezcan apuntando al elemento correcto.
Esto no es correcto Puedo hacer referencia a cualquier tipo a , pero el tipo de interp dice que el medio de almacenamiento es una lista homogénea de b s. GHC nos hace explotar cuando rechaza esta firma de tipo, quejándose de que no puede coincidir con el tipo de cosa dentro de MkRef .
Sin inmutarse, aprovechemos el uso de una lista heterogénea como entorno para la mónada de State en la que interpretaremos PT .
infixr 4 :>
data Tuple as where
E :: Tuple ''[]
(:>) :: a -> Tuple as -> Tuple (a '': as)
Este es uno de mis tipos de datos Haskell favoritos. Es una tupla extensible indexada por una lista de los tipos de cosas dentro de ella. Las tuplas son listas vinculadas heterogéneas con información de nivel de tipo sobre los tipos de cosas dentro de ella. (A menudo se llama HList siguiendo el papel de Kiselyov pero prefiero Tuple .) Cuando agrega algo al frente de una tupla, agrega su tipo al frente de la lista de tipos. En un estado de ánimo poético, una vez lo expresé de esta manera : "La tupla y su tipo crecen juntos, como una vid trepando por una planta de bambú".
Ejemplos de Tuple s:
ghci> :t ''x'' :> E
''x'' :> E :: Tuple ''[Char]
ghci> :t "hello" :> True :> E
"hello" :> True :> E :: Tuple ''[[Char], Bool]
¿Cómo son las referencias a los valores dentro de las tuplas? Tenemos que demostrarle a GHC que el tipo de cosa que estamos obteniendo de la tupla es del tipo que esperamos.
data Elem as a where -- order of indices arranged for convenient partial application
Here :: Elem (a '': as) a
There :: Elem as a -> Elem (b '': as) a
La definición de Elem es estructuralmente la de los números naturales (los valores de Elem como There (There Here) tienen un aspecto similar a los naturales como S (SZ) ) pero con tipos adicionales, en este caso, lo que demuestra que el tipo a está en el type- lista de niveles as . Menciono esto porque es sugerente: Nat ''s es un buen índice de listas, y asimismo Elem es útil para indexar en una tupla. En este sentido, será útil como reemplazo del Int dentro de nuestro tipo de referencia.
(!) :: Tuple as -> Elem as a -> a
(x :> xs) ! Here = x
(x :> xs) ! (There ix) = xs ! ix
Necesitamos un par de funciones para trabajar con tuplas e índices.
type family as :++: bs where
''[] :++: bs = bs
(a '': as) :++: bs = a '': (as :++: bs)
appendT :: a -> Tuple as -> (Tuple (as :++: ''[a]), Elem (as :++: ''[a]) a)
appendT x E = (x :> E, Here)
appendT x (y :> ys) = let (t, ix) = appendT x ys
in (y :> t, There ix)
Probemos y escribamos un intérprete para un PT en un entorno Tuple .
interp :: PT (Elem as) a -> State (Tuple as) a
interp (MkRef x) = do
t <- get
let (newT, el) = appendT x t
put newT
return el
-- ...
No se puede hacer, bromista. El problema es que el tipo de Tuple en el entorno cambia cuando obtenemos una nueva referencia. Como mencioné antes, agregar algo a una tupla agrega su tipo al tipo de tupla, un hecho desmentido por el tipo State (Tuple as) a . GHC no se dejó engañar por este intento de subterfugio: Could not deduce (as ~ (as :++: ''[a1])) .
Aquí es donde las ruedas se desprenden, por lo que puedo ver. Lo que realmente quieres hacer es mantener el tamaño de la tupla constante a lo largo de un cálculo PT . Esto requeriría que indexe PT por la lista de tipos a los que puede obtener referencias, lo que demuestra cada vez que lo hace y le permite (dando un valor de Elem ). El entorno se vería entonces como una tupla de listas, y una referencia consistiría en un Elem (para seleccionar la lista correcta) y un Int (para encontrar el elemento particular en la lista).
Este plan rompe las reglas, por supuesto (es necesario cambiar la definición de PT ), pero también tiene problemas de ingeniería. Cuando llamo a MkRef , me corresponde a mí dar un Elem por el valor al que hago referencia, que es bastante tedioso. (Dicho esto, por lo general, puedes convencer a GHC para que encuentre los valores de Elem mediante una búsqueda de prueba con una clase de tipo hacky).
Otra cosa: componer PT s se vuelve difícil. Todas las partes de su computación deben ser indexadas por la misma lista de tipos. Podría intentar introducir combinators o clases que le permitan hacer crecer el entorno de un PT , pero también debería actualizar todas las referencias cuando lo haga. Usar la mónada sería bastante difícil.
Una implementación posiblemente más limpia permitiría que la lista de tipos en un PT varíe a medida que recorre el tipo de datos: cada vez que se encuentra con un MkRef el tipo recibe uno más. Debido a que el tipo de computación cambia a medida que avanza, no puede usar una mónada regular; debe recurrir a IxMonad . Si quieres saber cómo es ese programa, mira mi otra respuesta .
En última instancia, el punto de fricción es que el tipo de tupla está determinado por el valor de la solicitud PT . El entorno es lo que una solicitud determinada decide almacenar en él. interp no puede elegir lo que está en la tupla, debe provenir de un índice en PT . Cualquier intento de infringir ese requisito va a colapsar y arder. Ahora, en un verdadero sistema de tipo dependiente, podríamos examinar el valor del PT que se nos dio y descubrir qué debería ser. Por desgracia, Haskell no es un sistema de tipo dependiente.