haskell - 定义应用实例的问题

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'是输出之一。所以，输入 Foo就像 indexed state 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 的实例允许改变环境类型？我搜索了 indexed functors ，但乍一看，他们似乎并没有解决我的问题。有人可以提出一些建议来实现这一目标吗？

Answer 1

您的 Foo type 是 Atkey 最初称为 parameterised monad 的示例。 ，而其他所有人(可以说是错误的)现在都称为索引单子(monad)。

带索引的 monad 是类似 monad 的东西，有两个索引，它们描述了通过类型的有向图的路径。排序索引一元计算要求两个计算的索引像多米诺骨牌一样排列。

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

如果您有一个索引 monad，它描述了来自 x 的路径至 y ，以及从 y 获取的方法至 z , 索引绑定(bind) >>>=会给你一个更大的计算，从 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具有多米诺骨牌式的排序，对于转换类型级环境的计算来说是一个很好的抽象:您希望第一个计算使环境处于对第二个可口的状态。让我们写一个 IMonad 的实例对于 Foo .

我将首先指出您的 Woo s a类型与 (a, Maybe s) 同构，这是 Writer 的一个示例单子(monad)。我提到这一点是因为我们需要 Monad (Woo s) 的实例后来我懒得自己写了。

type Woo s a = Writer (First s) a

我选择了 First 作为我喜欢的 Maybe 的口味monoid 但我不知道你打算如何使用 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 上的函数里面的单子(monad)。

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 .意外惊喜，我们最终委托(delegate)给 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'')

附录 : 这张照片中缺少的东西是变形金刚。本能告诉我你应该能够表达 Foo作为一个单子(monad)变压器堆栈:

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

但是索引 monad 没有关于变形金刚的引人入胜的故事。 >>>=的类型将要求堆栈中的所有索引 monad 以相同的方式操作它们的索引，这可能不是您想要的。索引单子(monad)也不能与常规单子(monad)很好地组合。

所有这一切都是说索引 monad 转换器使用 McBride-style indexing scheme 表现得更好一些。 .麦克布莱德的 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