haskell - ¿Hay una generalización de estas construcciones de estilo libre?

category-theory free-monad

Question

Estaba jugando con ideas libres, y encontré esto:

{-# LANGUAGE RankNTypes #-}

data Monoid m = Monoid { mempty :: m, mappend :: m -> m -> m }
data Generator a m = Generator { monoid :: Monoid m, singleton :: a -> m }

newtype Free f = Free { getFree :: forall s. f s -> s }

mkMonoid :: (forall s. f s -> Monoid s) -> Monoid (Free f)
mkMonoid f = Monoid {
    mempty = Free (mempty . f),
    mappend = /a b -> Free $ /s -> mappend (f s) (getFree a s) (getFree b s)
}

freeMonoid :: Monoid (Free Monoid)
freeMonoid = mkMonoid id

mkGenerator :: (forall s. f s -> Generator a s) -> Generator a (Free f)
mkGenerator f = Generator {
    monoid = mkMonoid (monoid . f),
    singleton = /x -> Free $ /s -> singleton (f s) x
}

freeGenerator :: Generator a (Free (Generator a))
freeGenerator = mkGenerator id

Me gustaría encontrar las condiciones bajo las cuales podría escribir una función:

mkFree :: (??? f) => f (Free f)

pero no he podido encontrar una estructura significativa para f (que no sea la trivial en la que mkFree es un método de ??? ) que permita escribir esta función. En particular, mi sentido estético preferiría si esta estructura no mencionara el tipo Free .

¿Alguien ha visto algo como esto antes? ¿Es esta generalización posible? ¿Existe una generalización conocida en una dirección en la que no haya pensado todavía?

Answer 1

El enlace con el álgebra universal fue un buen punto de partida, y después de leerlo un poco, todo encajó. Lo que estamos buscando es un álgebra F:

type Alg f x = f x -> x

para cualquier (endo) functor f . Por ejemplo, para un álgebra monoide el functor es:

data MonoidF m = MEmpty | MAppend m m deriving Functor

Para cualquier instancia de Monoid está el álgebra de monoides evidente:

monoidAlg :: Monoid m => Alg MonoidF m
monoidAlg MEmpty = mempty
monoidAlg (MAppend a b) = mappend a b

Ahora podemos tomar la definición de functor libre del paquete free-functors y reemplazar la restricción de clase con el álgebra f:

newtype Free f a = Free { runFree :: forall b. Alg f b -> (a -> b) -> b }

El funtor libre es, en cierto sentido, la mejor manera de convertir cualquier conjunto en un álgebra. Así es como:

unit :: a -> Free f a
unit a = Free $ /_ k -> k a

Es la mejor manera porque, para cualquier otra forma de convertir a en un álgebra b , podemos asignar una función del álgebra libre a b :

rightAdjunct :: Functor f => Alg f b -> (a -> b) -> Free f a -> b
rightAdjunct alg k (Free f) = f alg k

Lo que queda es mostrar que el functor libre crea un f-algebra (y esto es lo que pediste):

freeAlg :: Functor f => Alg f (Free f a)
freeAlg ff = Free $ /alg k -> alg (fmap (rightAdjunct alg k) ff)

Para explicar un poco: ff es de tipo f (Free fa) y necesitamos construir un Free fa . Podemos hacer eso si podemos construir una b , dado alg :: fb -> b y k :: a -> b . Entonces podemos aplicar alg a ff si podemos mapear cada Free fa que contiene a una b , pero eso es exactamente lo que hace rightAdjunct con alg y k .

Como habrás adivinado, esta Free f es la mónada gratuita en el functor f (la versión de la iglesia codificada es precisa).

instance Functor f => Monad (Free f) where
  return = unit
  m >>= f = rightAdjunct freeAlg f m