Существует ли обобщение этих свободных конструкций? - программирование
Подтвердить что ты не робот

Существует ли обобщение этих свободных конструкций?

Я играл со свободными идеями и нашел это:

{-# 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

Я хотел бы найти условия, при которых я мог бы написать funcion:

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

но мне не удалось найти значимую структуру для f (кроме тривиальной, в которой mkFree - метод ???), который позволил бы записать эту функцию. В частности, мой эстетический смысл предпочел бы, чтобы эта структура не упоминала тип Free.

Кто-нибудь видел что-то подобное раньше? Возможно ли это обобщение? Есть ли известное обобщение в том направлении, о котором я еще не думал?

4b9b3361

Ответ 1

Ссылка на универсальную алгебру была хорошей отправной точкой, и после прочтения ее немного все встало на свои места. Мы ищем F-алгебру:

type Alg f x = f x -> x

для любого (endo) -функтора f. Например, для моноидной алгебры функтор имеет вид:

data MonoidF m = MEmpty | MAppend m m deriving Functor

Для любого экземпляра Monoid существует очевидная моноидная алгебра:

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

Теперь мы можем взять определение свободного функтора из пакета free-functors и заменить ограничение класса на f-алгебру:

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

Свободный функтор в некотором смысле является лучшим способом превратить любое множество a в алгебру. Вот как это делается:

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

Это лучший способ, поскольку для любого другого способа превратить a в алгебру b, мы можем дать функцию от свободной алгебры до b:

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

Осталось фактически показать, что свободный функтор создает f-алгебру (и это то, о чем вы просили):

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

Объяснить немного: ff имеет тип f (Free f a), и нам нужно построить Free f a. Мы можем сделать это, если мы сможем построить a b, учитывая alg :: f b -> b и k :: a -> b. Поэтому мы можем применить alg к ff, если мы можем отобразить каждый Free f a, который он содержит в b, но то, что делает rightAdjunct с alg и k.

Как вы могли догадаться, эта Free f - это свободная монада на функторе f (закодированная в церкви версия, чтобы быть точным.)

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