定义应用程序实例时出现问题

Question

假设我想要定义由两个类型级环境索引的数据类型.就像是:

data Woo s a = Woo a | Waa s a

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

这个想法是env输入环境,env'是输出环境.因此,type Foo类似于索引状态monad.到现在为止还挺好.我的问题是我怎么能表明这Foo是一个应用函子.显而易见的尝试是

instance Applicative (Foo s env env') where
    pure x = Foo (\s env -> (Woo x, env))
    -- definition of (<*>) omitted.

但GHC抱怨pure说它是错误类型的,因为它推断了类型

    pure :: a -> Foo s env env a

而不是预期的类型

    pure :: a -> Foo s env env' a

什么是完全合理的.我的观点是,可以定义一个允许更改环境类型的Applicative实例Foo吗？我用google搜索索引的仿函数,但乍一看,它们似乎没有解决我的问题.有人可以建议实现这个目标吗？

Answer 1

你的Foo类型是Atkey最初称为参数化monad的一个例子,其他人(可以说是错误的)现在称为索引monad.

索引monad是类似monad的东西,有两个索引,用于描述通过类型的有向图的路径.排序索引monadic计算要求两个计算的索引像dominos一样排列.

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.

您在问题中提到的索引monad的一个简单示例是索引状态monad 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通过其多米诺骨牌排序,对于转换类型级环境的计算是一个很好的抽象:您希望第一次计算使环境处于对第二种环境可口的状态.让我们写一个IMonadfor 的实例Foo.

我将首先注意到你的Woo s a类型是同构的(a, Maybe s),这是Writermonad的一个例子.我提到这个是因为我们Monad (Woo s)以后需要一个实例而且我懒得自己编写.

type Woo s a = Writer (First s) a

我选择First了我喜欢的Maybemonoid 味道,但我不知道你打算如何使用它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函数:我们进入有状态计算和内部monad 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.我们必须用它Writer s的Applicative例子来粉碎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.令人惊讶的是,我们最终委托了Writer s他们的Monad实例.还要注意将作者内部的traverseW中间体a用于Kleisli箭头的狡猾用法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'')

附录:这张照片中缺少的是变形金刚.Instinct告诉我你应该能够表达Foo为monad变换器堆栈:

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

但索引的monad没有一个令人信服的故事来讲述变形金刚.类型>>>=将要求堆栈中的所有索引monad以相同的方式操纵它们的索引,这可能不是你想要的.索引monad也不能很好地与常规monad组合.

所有这一切都说明索引的monad变换器在McBride风格的索引方案中表现得更好一些.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)

然后monad变形金刚看起来像这样:

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