用于泛化索引 monad 的类型级类幺半群操作？

Question

为了激发这个问题，让我们首先回顾一个沼泽标准的 Hoare-Dijkstra 风格的索引 monad，以及索引编写器 monad 的示例实例。

对于索引 monad，我们只需要 (i)binds:

上的类型对齐

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)

它确实是一个类似 writer 的 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仍然没有进行typecheck。就好像 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（又名。分级单子，参见 effect-monad）。

特别是，使用 IMonadTF（分级 monads）你可以绑定任何两个计算，它们的索引被附加在一起，而使用 IMonadHoare（索引 monads）你只能绑定具有匹配索引的计算.因此，您不能轻易地将任意 IMonadHoare（例如 IWriter）编码为 IMonadTF，因为当索引不匹配时 bind 没有任何意义。

这种 IMonadHoare 的 "partially defined composition" 让人想起类别，实际上我们可以用类别箭头索引的单子来概括 IMonadHoare 和 IMonadTF，而不是成对的指数或幺半群的元素。实际上，我们可以在 classes:

中看到类别示例

对(i, j)可以看作是一个类别的箭头，其中i和j是对象（所以i和[=之间只有一个箭头26=]，一对 (i, j)，虽然它是什么并不重要，只是正好有一个）；
幺半群是类别。

这是按类别 c :: k -> k -> Type 索引的 class 个单子；此 class 通过对应于您的 Empty 和 Append 的关联类型 Id 和 Cat 包含类别 c 的定义。它看起来实际上与 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 之间（在某些 set/type 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)

Answer 2

(没有理由把元组放入IWriter；我只是打算用这个

data IWriter (cat :: idx -> idx -> Type) (p :: (idx, idx)) (a :: Type) where
  IWriter :: a -> cat i j -> IWriter cat '(i, j) a

)

你写了

ireturn x = IWriter x id

对于所有版本 class。但是，IWriter x id :: forall i. IWriter cat (i, i) a，而您需要 IWriter cat m a（其中 cat、m 和 a 是 ireturn 的参数）。 (,) _ _ 不是 m，句号。你也不能写一个约束来证明这一点，因为 i 需要成为 ireturn 的参数，但它是一个类型 class 方法，所以这是不允许的。除此之外，正确的 IMonad 实际上是最后一个（IMonadConstraint，1 和 2，在一起）。

class IMonad (m :: idx -> Type -> Type) | m -> idx where
  type IsEmpty m (i :: idx) :: Constraint
  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

您需要断言一个公理：

data IsTup (p :: (i, j)) where IsTup :: IsTup '(x, y)
isTup :: forall p. IsTup p
isTup = unsafeCoerce IsTup

命题forall (p :: (i, j)). exists (x :: i) (y :: j). p ~ '(x, y)在Haskell中既不可证明也不可证伪，所以如果需要的话，我们可以像这样把它当作一个公理。看来"true"够了。

instance Category cat => IMonad (IWriter cat) where
  type IsEmpty (IWriter cat) '(i, j) = i ~ j
  type IsAppend (IWriter cat) '(_, i) '(j, _) = i ~ j
  type Append (IWriter cat) '(i, _) '(_, j) = '(i, j)
  ireturn :: forall i a. IsEmpty (IWriter cat) i => a -> IWriter cat i a
  ireturn x | IsTup <- isTup @i = IWriter x id
  ibind (IWriter x w) f | IWriter y w' <- f x = IWriter y (w >>> w')
  -- IWriter :: forall cat p a. forall i j. p ~ '(i, j) => a -> cat i j -> IWriter cat p a
  -- IsTup   :: forall     p  . forall x y. p ~ '(x, y) =>                 IsTup       p
  -- in ibind, the two matches on IWriter prove that the two type-level tuple
  -- arguments are actually tuples
  -- in ireturn, you need to split that behavior out into it's own type IsTup,
  -- make forall p. IsTup p an axiom, and use it to show that the argument i
  -- is also really a tuple

用于泛化索引 monad 的类型级类幺半群操作？

Type-level monoid-like operations for generalizing indexed monads?

haskell

monads

type-families

type-level-computation