haskell - 用于泛化索引单子(monad)的类型级类幺半群操作？

Question

为了提出这个问题，我们首先回顾一下沼泽标准 Hoare-Dijkstra 风格的索引 monad，以及索引 writer monad 的示例实例。

对于索引 monad，我们只需要 (i)bind 上的类型对齐:

class IMonadHoare m where
    ireturn :: a -> m i i a
    ibind :: m i j a -> (a -> m j k b) -> m i k b

然后为了证明这是可用的，让我们实现一个索引编写器 monad:

import Prelude hiding (id, (.))
import Control.Category

newtype IWriter cat i j a = IWriter{ runIWriter :: (a, cat i j) }

instance (Category cat) => IMonadHoare (IWriter cat) where
    ireturn x = IWriter (x, id)

    ibind (IWriter (x, f)) k = IWriter $
        let (y, g) = runIWriter (k x)
        in (y, g . f)

它确实是一个类似编写器的 monad，因为我们可以实现常用的方法:

itell :: (Category cat) => cat i j -> IWriter cat i j ()
itell f = IWriter ((), f)

ilisten :: (Category cat) => IWriter cat i j a -> IWriter cat i j (a, cat i j)
ilisten w = IWriter $
    let (x, f) = runIWriter w
    in ((x, f), f)

ipass :: (Category cat) => IWriter cat i j (a, cat i j -> cat i j) -> IWriter cat i j a
ipass w = IWriter $
    let ((x, censor), f) = runIWriter w
    in (x, censor f)

好的，到目前为止一切顺利。但现在我想将其推广到其他类型(呵呵)的指数。我认为只需为类型级幺半群操作添加关联的类型族就可以了，如下所示:

{-# LANGUAGE TypeFamilies, PolyKinds, MultiParamTypeClasses, FunctionalDependencies #-}

import Data.Kind

class IMonadTF idx (m :: idx -> Type -> Type) | m -> idx where
    type Empty m :: idx
    type Append m (i :: idx) (j :: idx) :: idx

    ireturn :: a -> m (Empty m) a
    ibind :: m i a -> (a -> m j b) -> m (Append m i j) b

那么，这有效吗？好吧，您可以使用它来定义 Empty/Append 未索引的内容，如下所示:

{-# LANGUAGE DataKinds, TypeOperators #-}

import GHC.TypeLists

newtype Counter (n :: Nat) a = Counter{ runCounter :: a }

instance IMonadTF Nat Counter where
    type Empty Counter = 0
    type Append Counter n m = n + m

    ireturn = Counter
    ibind (Counter x) k = Counter . runCounter $ k x

tick :: Counter 1 ()
tick = Counter ()

但是现在我们可以重新创建我们的 IWriter 示例吗？不幸的是，我无法做到。

首先，我们甚至不能声明Empty:

data IWriter cat (ij :: (Type, Type)) a where
    IWriter :: { runIWriter :: (a, cat i j) } -> IWriter cat '(i, j) a

instance (Category cat) => IMonadTF (Type, Type) (IWriter cat) where
    type Empty (IWriter cat) = '(i, i)

这当然会失败，因为类型变量 i 不在范围内。

让我们将 Empty 更改为 Constraint，然后重新创建 Counter 实例来验证它:

class IMonadConstraint idx (m :: idx -> Type -> Type) | m -> idx where
    type IsEmpty m (i :: idx) :: Constraint
    type Append m (i :: idx) (j :: idx) :: idx

    ireturn :: (IsEmpty m i) => a -> m i a
    ibind :: m i a -> (a -> m j b) -> m (Append m i j) b

newtype Counter (n :: Nat) a = Counter{ runCounter :: a }

instance IMonadConstraint Nat Counter where
    type IsEmpty Counter n = n ~ 0
    type Append Counter n m = n + m

    ireturn = Counter
    ibind (Counter x) k = Counter . runCounter $ k x

tick :: Counter 1 ()
tick = Counter ()

现在我们至少可以写出IsEmpty (Writer cat)的定义了，但是在下面的代码中，ireturn仍然没有进行类型检查。就好像 IsEmpty 的定义不用于解决约束:

instance (Category cat) => IMonadConstraint (Type, Type) (IWriter cat) where
    type IsEmpty (IWriter cat) '(i, j) = i ~ j

    ireturn x = IWriter (x, id)

Could not deduce i ~ '(j0, j0) from the context IsEmpty (IWriter cat) i

类似地，我们可以尝试通过添加附加约束来强制中间对齐:

class IMonadConstraint2 idx (m :: idx -> Type -> Type) | m -> idx where
    type IsAppend m (i :: idx) (j :: idx) :: Constraint
    type Append m (i :: idx) (j :: idx) :: idx

    ireturn :: (IsEmpty m i) => a -> m i a    ibind :: (IsAppend m i j) => m i a -> (a -> m j b) -> m (Append m i j) b

但是 IWriter 也会以类似的方式失败:

instance (Category cat) => IMonadConstraint2 (Type, Type) (IWriter cat) where
    type IsAppend (IWriter cat) '(i, j) '(j', k) = j ~ j'
    type Append (IWriter cat) '(i, j) '(j', k) = '(i, k)

    ibind (IWriter (x, w)) k = IWriter $
        let (y, w') = runIWriter (k x)
        in (y, w' . w)

Could not deduce j ~ '(j1, j0) from the context IsAppend (IWriter cat) i j

是因为IsEmpty和IsAppend定义了“pointwise”吗？

Answer 1

tl;dr:看起来您正在寻找按类别索引的 monad。

可编译要点:https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971

<小时/>

IMonadHoare不等于IMonadTF (又名分级单子(monad)，请参阅 effect-monad )。

特别是 IMonadTF (分级单子(monad))你可以绑定(bind)任意两个计算，它们的索引被附加在一起，而 IMonadHoare (索引单子(monad))您只能将计算与匹配的索引绑定(bind)。因此，您无法轻松地对任意 IMonadHoare 进行编码，如IWriter ，作为IMonadTF因为 bind 没有任何意义当索引不匹配时。

IMonadHoare的这种“部分定义的组合”让人想起类别，实际上我们可以概括两者 IMonadHoare和IMonadTF使用由类别箭头索引的单子(monad)，而不是单群的索引对或元素。事实上，我们可以看到这两个类中的类别示例:

1. 对 (i, j)可以看作是类别的箭头，其中 i和j是对象(因此 i 和 j 之间恰好有一个箭头，一对 (i, j) ，尽管它是什么并不重要，只是恰好有一个)；
2. 幺半群是类别。

这是按类别 c :: k -> k -> Type 索引的 monad 类;此类包括类别 c 的定义，通过关联类型 Id和Cat对应于您的Empty和Append 。它看起来实际上与 IMonadTF 几乎相同，除了您有一个类别 c :: k -> k -> Type而不是幺半群idx :: Type .

{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}

import Control.Category as C
import Data.Kind

class CatMonad (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) where
  type Id m :: c x x
  type Cat m (f :: c x y) (g :: c y z) :: c x z

  xpure :: a -> m (Id m) a

  xbind :: m f a -> (a -> m g b) -> m (Cat m f g) b

这是我之前提到的配对类别。每个对象之间i和j (在某些集合/类型 k 中)，有一个箭头 E (名称并不重要，重要的是只有一个)。它也可以被可视化为带有 k 中的顶点的完整图。 .

data Edge (i :: k) (j :: k) = E

我们现在可以定义IWriter作为CatMonad 。这有点挑剔，你必须输入 i和j明确地否则它们会在 CatMonad 的错误位置被量化。实例头。不然也不会有太大的麻烦。没有什么真正取决于 E ,它只是其类型的占位符，其中包含重要的索引 i和j .

newtype IWriter cat i j (q :: Edge i j) a = IWriter { runIWriter :: (a, cat i j) }

instance Category cat => CatMonad (IWriter cat) where
  type Id (IWriter cat) = E
  type Cat (IWriter cat) _ _ = E

  xpure a = IWriter (a, C.id)
  xbind (IWriter (a, f)) k =
    let IWriter (b, g) = k a in
    IWriter (b, f C.>>> g)