Pregunta ¿Se puede ejecutar una mónada tipo `ST` puramente (sin la biblioteca` ST`)?


Esta publicación es Haskell alfabetizada. Simplemente coloque un archivo como "pad.lhs" y ghci será capaz de ejecutarlo.

> {-# LANGUAGE GADTs, Rank2Types #-}
> import Control.Monad
> import Control.Monad.ST
> import Data.STRef

De acuerdo, entonces pude descifrar cómo representar el ST Mónada 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 s a no debe ser isomorfo a ningún otro tipo forall s. (En particular, debe ser isomorfo para ninguno () 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 un Monad. Usted se estará preguntando cómo return está implementado. 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 ST en absoluto:

> runPF :: (forall s. PT s a) -> a
> runPF p = runST $ toST p

runPF $ fib 7 da 13, cual es correcta.


Mi pregunta es ¿podemos definir runPF sin referencia usando ST ¿en absoluto?

¿Hay una manera pura de definir runPF? PTRefLa definición de 's es completamente sin 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 tu no poder definir runPF puramente, da una prueba de que no puede.

El rendimiento no es una preocupación (si lo fuera, no habría hecho todas las return tener su propia referencia).

Estoy pensando que los tipos existenciales pueden ser útiles.

Nota: es trivial si suponemos que es a es dinamizable 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 (Conversión de (forall s. PT s) es una especie de prueba de si una respuesta es válida o no).


32
2017-11-28 19:04


origen


Respuestas:


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 arbitrario tipos. Esto no es posible sin empaquetar algún tipo de evidencia en el MkRef constructor - ya sea una envoltura existencial Typeable diccionario 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 artículo en el entorno, nos aseguramos de agregarlo al final de la lista, de modo que Refs que hemos distribuido anteriormente apuntando al elemento correcto.

Esto no es correcto Puedo hacer una referencia a alguna tipo a, pero el tipo de interp dice que el medio de almacenamiento es una lista homogénea de bs. GHC nos hace explotar cuando rechaza esta firma de tipo, quejándose de que no puede coincidir b con el tipo de cosa dentro MkRef.


Sin inmutarse, intentemos usar una heterogéneo lista como el entorno para el State mónada 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. Se trata de un tupla extensible indexado por una lista de los tipos de cosas dentro de él. 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 dije de esta manera: "La tupla y su tipo crecen juntos, como una vid trepando por una planta de bambú".

Ejemplos de Tuples:

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 el de los números naturales (Elem valores como There (There Here) se parecen a los números naturales como S (S Z)) pero con tipos adicionales, en este caso, demostrando que el tipo a está en la lista de nivel de tipo as. Menciono esto porque es sugerente: Nats hacer buenos índices de listas, y del mismo modo Elem es útil para indexar en una tupla. En este sentido, será útil como un reemplazo para el 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 PT en un Tuple ambiente.

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 la tupla, un hecho desmentido por el tipo State (Tuple as) a. GHC no se deja 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 PT cálculo. Esto requeriría que indices PT a sí mismo por la lista de tipos a los que puede obtener referencias, demostrando cada vez que lo hace que está autorizado (dando un Elem valor). El entorno se vería entonces como una tupla de listas, y una referencia consistiría en Elem (para seleccionar la lista correcta) y un Int (para encontrar el artículo particular en la lista).

Este plan rompe las reglas, por supuesto (debe cambiar la definición de PT), pero también tiene problemas de ingeniería. Cuando llamo MkRef, la responsabilidad recae en mí para dar un Elem por el valor al que hago referencia, que es bastante tedioso. (Dicho esto, generalmente puede convencer a GHC para que encuentre Elemvalores por búsqueda de prueba utilizando una clase de tipo hacky.)

Otra cosa: componer PTs se vuelve difícil. Todas las partes de su computación deben ser indexadas por mismo lista de tipos. Podría intentar introducir combinators o clases que le permitan hacer crecer el entorno de un PT, pero también tendrías que actualizar todas las referencias cuando lo hagas. Usar la mónada sería bastante difícil.

Una implementación posiblemente más limpia permitiría la lista de tipos en un PT para variar 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 la tupla está determinada por el valor de la PT solicitud. El entorno es lo que una solicitud dada decide almacenar en él. interp no puede elegir lo que está en la tupla, debe venir 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 PT valor que nos dieron y averiguar qué as debiera ser. Por desgracia, Haskell no es un sistema de tipo dependiente.


14
2017-11-28 23:54



Una solución simple es envolver un State Mónada y presente 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 lo usual ST s El truco de cuantificación nos permite evitar que los usuarios dañen el contenedor que almacena las referencias.

Mantenemos ref-s en una IntMap e incrementar un contador cada vez que asignamos una nueva referencia. Leer y escribir simplemente modifica el IntMap Con algo 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 el siguiente falla con el habitual ST error de tecleado:

> runST (newSTRef True)

Por supuesto, el esquema anterior nunca basura recoge referencias, sino que libera todo en cada runST llamada. 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 internos directamente es tan peligroso como usar GHC.ST internos y State# directamente, por lo que debemos asegurarnos de presentar una API segura, y también probar nuestros internos por completo (o de lo contrario podemos obtener segfaults en Haskell, un gran pecado).


11
2017-11-28 22:51



Desde que publiqué mi respuesta anterior, ha indicado que no le importa hacer cambios a su definición de PT. Me complace informar: relajar esa restricción cambia la respuesta a su pregunta de no a ! 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 un más inteligente Monad clase que la del Preludio: la de cosas indexadas como mónadas describiendo caminos 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. m i j a es un cálculo monádico que requiere un estado de entrada de i, cambia el estado a jy produce un valor de tipo a. Secuenciación de mónadas indexadas con >>>= es como jugar dominó Puede alimentar un cálculo que toma el estado de i a j en un cálculo que va desde 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 Flechas de Kleisli de la fortuna indignante (y en otra parte) pero este es suficiente para nuestros propósitos).

Una posibilidad con MonadIx es un File mónada que rastrea el estado de un manejador 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. los run la operación requiere un cálculo del tipo File Closed Closed a, lo que garantiza que sus manejadores de 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 mis mónadas de "programa / intérprete" gratis 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 del código, así que aquí está el factor que producirá PT cuando lo conectamos a FreeIx abajo:

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 pueden 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 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: el primero será un ref (a ': as) a y el segundo será un 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 cerrarí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 Mencioné antes. FreeIx convierte un functor indexado en una mónada indexada al proporcionar una operación de unión alineada con el tipo Free, que une el nudo recursivo en el parámetro del functor, y una operación de no hacer nada 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 el estándar que debe escribir para hacer Free y Pure más fácil trabajar con. Aquí hay algunas acciones individuales PTs que forman la base del API de la mónada, y algunos sinónimos de patrones para esconder el Free constructores cuando desempaquetamos PT valores.

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 PT cómputos. Aquí está tu fib ejemplo. Estoy usando RebindableSyntax y redefinir localmente los operadores de mónadas (a sus equivalentes indexados) para que pueda usar do notación 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 se ve exactamente como el que quería escribir en la pregunta original. La única diferencia (aparte de las consolidaciones locales de >>= y así sucesivamente) es la llamada a expand. Cada vez que creas una nueva referencia, tienes que expand todos los viejos, lo cual es un poco tedioso.

Finalmente podemos terminar el trabajo que nos propusimos hacer y construir un PT-machine que usa un Tuple como el 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 para la que la construiste, solo necesitas hacer que se vea más abajo en la lista.

instance Expand Elem where
    expand = There

Tenga en cuenta que este despliegue de Elem es más bien como un índice de Bruijn: las variables más limitadas recientemente 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 se encuentra con un MkRef solicitud, aumenta el tamaño de su memoria al agregar x al frente. El verificador de tipos te recordará que cualquier refs de antes de la MkRef debe estar correctamente expanded, por lo que las referencias existentes no se pierden cuando la tupla cambia de tamaño. Pagamos un intérprete sin yesos inseguros, pero tenemos integridad referencial para arrancar.

Ejecutar desde un principio permanente requiere que el PT el cómputo espera comenzar 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

9
2017-12-01 11:32