定义应用实例的问题

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

什么是完全合理的。我的观点是，可以为 Foo 定义一个 Applicative 实例，允许更改环境类型吗？我用谷歌搜索 indexed functors，但乍一看，它们似乎无法解决我的问题。有人可以提出一些建议来实现这一目标吗？

Answer 1

本质上，您缺少对 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')

Answer 2

您的 Foo 类型是 Atkey 最初称为 parameterised monad 的示例，其他人（可以说是错误的）现在称为 indexed monad。

Indexed monads 是类似 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 的方法，索引绑定 >>>= 会给你一个更大的计算，使你从 x 到 z.

另请注意 ipure returns 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 具有多米诺骨牌式排序，是转换类型级环境的计算的良好抽象：您希望第一个计算使环境处于第二个可以接受的状态。让我们为 Foo.

写一个 IMonad 的实例

我首先要注意您的 Woo s a 类型与 (a, Maybe s) 同构，这是 Writer monad 的一个示例。我提到这个是因为我们稍后需要 Monad (Woo s) 的实例，而我懒得自己写。

type Woo s a = Writer (First s) a

我选择了First as my preferred flavour of Maybe monoid but I don't know exactly how you intend to use Woo. You may prefer 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。令人惊讶的是，我们最终委托给 Writer s 的 Monad 实例。还要注意巧妙地使用 traverseW 将 writer 内部的中间体 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 下表现得更好一些。 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

定义应用实例的问题

Problems in defining an applicative instance

haskell

dependent-type

type-level-computation