Проблемы с определением аппликативного экземпляра

Ваш тип Foo является примером того, что Atkey изначально назвал параметризованной монадой. , а все остальные (возможно, неправильно) теперь вызывают индексированную монаду.

Индексированные монады — это монадоподобные вещи с двумя индексами, которые описывают путь через ориентированный граф типов. Упорядочивание индексированных монадических вычислений требует, чтобы индексы двух вычислений выстраивались в ряд, как костяшки домино.

class IFunctor f where
    imap :: (a -> b) -> f x y a -> f x y b

class IFunctor f => IApplicative f where
    ipure :: a -> f x x a
    (<**>) :: f x y (a -> b) -> f y z a -> f x z b

class IApplicative m => IMonad m where
    (>>>=) :: m x y a -> (a -> m y z b) -> m x z b

Если у вас есть индексированная монада, описывающая путь от x к y и способ перехода от y к z, то индексированная привязка >>>= даст вам больше вычислений, которые переведут вас от x к z.

Также обратите внимание, что ipure возвращает f x x a. Значение, возвращаемое ipure, не проходит через ориентированный граф типов. Как уровень типа id.

Простым примером индексированной монады, на которую вы ссылались в своем вопросе, является монада индексированного состояния newtype IState i o a = IState (i -> (o, a)), которая преобразует тип своего аргумента из i в o. Вы можете выполнять последовательность вычислений с отслеживанием состояния только в том случае, если тип вывода первого совпадает с типом ввода второго.

newtype IState i o a = IState { runIState :: i -> (o, a) }

instance IFunctor IState where
    imap f s = IState $ \i ->
        let (o, x) = runIState s i
        in (o, f x)

instance IApplicative IState where
    ipure x = IState $ \s -> (s, x)
    sf <**> sx = IState $ \i ->
        let (s, f) = runIState sf i
            (o, x) = runIState sx s
        in (o, f x)

instance IMonad IState where
    s >>>= f = IState $ \i ->
        let (t, x) = runIState s i
        in runIState (f x) t

Теперь к вашему актуальному вопросу. IMonad с его упорядочиванием в стиле домино является хорошей абстракцией для вычислений, преобразующих среду на уровне типов: вы ожидаете, что первое вычисление оставит среду в состоянии, приемлемом для второго. Давайте напишем экземпляр IMonad для Foo.

Начну с того, что ваш тип Woo s a изоморфен типу (a, Maybe s), который является примером Writer монада. Я упоминаю об этом, потому что позже нам понадобится экземпляр для Monad (Woo s), а мне лень писать свой собственный.

type Woo s a = Writer (First s) a

Я выбрал First как мой любимый вариант моноида Maybe, но я точно не знаю, как вы собираетесь использовать Woo. Вы можете предпочесть Last.

Я также скоро воспользуюсь тем фактом, что Writer является экземпляром Traversable. На самом деле, Writer еще более проходим, чем это: поскольку он содержит только один a, нам не нужно сталкивать какие-либо результаты вместе. Это означает, что нам нужно только ограничение Functor для эффективного f.

-- cf. traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
traverseW :: Functor f => (a -> f b) -> Writer w a -> f (Writer w b)
traverseW f m = let (x, w) = runWriter m
                in fmap (\x -> writer (x, w)) (f x)

Давайте приступим к делу.

Foo s это IFunctor. Экземпляр использует функторность Writer s: мы идем внутрь вычислений с сохранением состояния и fmap функции над монадой Writer внутри.

newtype Foo (s :: *) (env :: [(Symbol,*)]) (env' :: [(Symbol,*)]) (a :: *) =
    Foo { runFoo :: s -> Sing env -> (Woo s a, Sing env') }

instance IFunctor (Foo s) where
    imap f foo = Foo $ \s env ->
        let (woo, env') = runFoo foo s env
        in (fmap f woo, env')

Нам также нужно сделать Foo обычным Functor, чтобы использовать его с traverseW позже.

instance Functor (Foo s x y) where
    fmap = imap

Foo s это IApplicative. Мы должны использовать экземпляр Applicative Writer s, чтобы разбить Woo вместе. Вот откуда берется ограничение Monoid s.

instance IApplicative (Foo s) where
    ipure x = Foo $ \s env -> (pure x, env)
    foo <**> bar = Foo $ \s env ->
        let (woof, env') = runFoo foo s env
            (woox, env'') = runFoo bar s env'
        in (woof <*> woox, env'')

Foo s это IMonad. Сюрприз-сюрприз, мы заканчиваем делегирование экземпляру Monad Writer s. Обратите также внимание на хитрое использование traverseW для подачи промежуточного звена a внутри записывающего устройства к стрелке Клейсли f.

instance IMonad (Foo s) where
    foo >>>= f = Foo $ \s env ->
        let (woo, env') = runFoo foo s env
            (woowoo, env'') = runFoo (traverseW f woo) s env'
        in (join woowoo, env'')

Дополнение. На этой картинке не хватает трансформеров. Инстинкт подсказывает мне, что вы должны уметь выражать Foo как стек преобразования монад:

type Foo s env env' = ReaderT s (IStateT (Sing env) (Sing env') (WriterT (First s) Identity))

Но у индексированных монад нет интересной истории о преобразователях. Тип >>>= потребовал бы, чтобы все индексированные монады в стеке манипулировали своими индексами одинаковым образом, что, вероятно, не то, что вам нужно. Индексированные монады также плохо сочетаются с обычными монадами.

Все это говорит о том, что преобразование индексированных монад немного лучше работает с McBride. схема индексации стиля. IMonad Макбрайда выглядит так:

type f ~> g = forall x. f x -> g x

class IMonad m where
    ireturn :: a ~> m a
    (=<?) :: (a ~> m b) -> (m a ~> m b)

Тогда преобразователи монад будут выглядеть так:

class IMonadTrans t where
    ilift :: IMonad m => m a ~> t m a

По сути, вам не хватает ограничения на Sing env', а именно, что это должно быть Monoid, потому что:

• вам нужно иметь возможность генерировать значение типа Sing env' из ничего (например, mempty)
• вам нужно иметь возможность объединить два значения типа Sing env' в одно во время <*> (например, mappend).

Вам также понадобится возможность комбинировать значения s в <*>, поэтому, если вы не хотите откуда-то импортировать SemiGroup, вы, вероятно, захотите, чтобы это тоже было Monoid.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveFunctor #-}
module SO37860911 where
import GHC.TypeLits (Symbol)
import Data.Singletons (Sing)

data Woo s a = Woo a | Waa s a 
  deriving Functor

instance Monoid s => Applicative (Woo s) where
  pure = Woo 
  Woo f <*> Woo a = Woo $ f a 
  Waa s f <*> Woo a = Waa s $ f a 
  Woo f <*> Waa s a = Waa s $ f a 
  Waa s f <*> Waa s' a = Waa (mappend s s') $ f a 

data Foo (s :: *) (env :: [(Symbol,*)]) (env' :: [(Symbol,*)]) (a :: *) =
     Foo { runFoo :: s -> Sing env -> (Woo s a, Sing env') }
  deriving Functor

instance (Monoid s, Monoid (Sing env')) => Applicative (Foo s env env') where
  pure a = Foo $ \_s _env -> (pure a, mempty)
  Foo mf <*> Foo ma = Foo $ \s env -> case (mf s env, ma s env) of
    ((w,e), (w',e')) -> (w <*> w', e `mappend` e')