在Haskell中，monad transformer是否唯一？

Question

在Haskell中，monad transformer是否唯一？

haskellmonadsmonad-transformers

4

有一些问题（例如这个问题和这个问题）询问是否在Haskell中每个单子（除了IO外）都有一个对应的单子变换器。现在，我想问一个补充问题。每个单子是否仅有一个变换器（或者像IO一样没有变换器），还是可以有多个变换器？

反例是两个单子变换器，它们产生相同行为的单子，当应用于恒等单子时，但在应用于其他单子时会产生不同行为的单子。如果答案是单子可以有多个变换器，我希望能提供尽可能简单的Haskell示例。这些变换器不必实际有用（虽然那会很有趣）。

在链接的问题中，一些答案似乎暗示一个单子可能有多个变换器。然而，我并不了解范畴论，只知道基本定义，因此不确定它们是否回答了这个问题。

- QuantumWiz

1

在某个时候，我发现自己需要一个简单的转换器，我称之为OuterMaybeT，它与一般的MaybeT不同，但确实给出了OuterMaybeT Identity ≌ Maybe。但仅适用于应用，我认为它不能用作单子变换器，而且我实际上从未检查过它是否符合法律。 - leftaroundabout

@leftaroundabout OuterMaybe f 只是 Compose Maybe f，对吧？所以据我所见它应该是合法的。 - amalloy

1

我的意思是，我们可以很容易地定义一种类型T，使得T Identity ~= Maybe和T [] ~= []，对吧？所以……不，它们并不是唯一的。这有点像退化的例子，但我真的想不出一个清晰的属性来形式化我的直觉，即我认为哪些是退化的，哪些不是。也许有一些参数性的类型级别类似物之类的东西……？ - Daniel Wagner

@DanielWagner 您的意思是为 T Identity 和 T [] 分别提供两个独立的 instance 声明吗？当然，如果是这样的话，每个声明可以按照自己的方式定义。但是，这感觉更像是两个单独的转换器而不是一个转换器（作为 MaybeT 的替代方案）。我认为对于“非退化”情况来说，转换器只需要有一个形式为 instance (Monad m) => Monad (T m) where 的声明就足够了。不确定这是否要求过高。到目前为止，我只是粗略地浏览了答案，但我想在仔细阅读它们后会更明智。 - QuantumWiz

@QuantumWiz，使用我正在考虑的技术（GADTs），只需编写一个实例即可。 - Daniel Wagner

3个回答

1

身份单子至少有两个单子变换器：身份单子变换器和密度单子变换器。

newtype IdentityT m a = IdentityT (m a)
newtype Codensity m a = Codensity (forall r. (a -> m r) -> m r)

事实上，考虑到Codensity Identity，对于所有的r，(a -> r) -> r与a是同构的。

这些单子变换器非常不同。一个例子是，“bracket”可以在Codensity中被定义为单子动作：

bracket :: Monad m => m () -> m () -> Codensity m ()
bracket before after = Codensity (\k -> before *> k () *> after)

然而，将该签名转换为IdentityT并没有太多意义。

bracket :: Monad m => m () -> m () -> IdentityT m ()  -- cannot implement the same functionality

类似的例子也可以从延续/余续单子的变体中找到，但我还没有看到一个通用的方案。

状态单子对应于状态单子转换器以及余续单子和ReaderT的组合：

newtype StateT s m a = StateT (s -> m (s, a))
newtype CStateT s m a = CStateT (Codensity (ReaderT s m) a)

列表单子至少对应三个单子变换器，不包括错误的一个：

newtype ListT m a = ListT (m (Maybe (a, ListT m a)))  -- list-t
newtype LogicT m a = LogicT (forall r. (a -> m r -> m r) -> m r -> m r)  -- logict
newtype MContT m a = MContT (forall r. Monoid r => (a -> m r) -> m r))

前两个可以分别在包list-t中找到（也在pipes的等效形式中找到），以及logict。

- Li-yao Xia

我理解得对吗？Codensity既是一个Monad Transformer，同时又是一个Monad，它不需要被应用到另一个Monad上就可以成为Monad的一个实例？ - QuantumWiz

不，它只是一个单子变换器。 - Li-yao Xia

但是实例声明只是 instance Monad (Codensity f) where（或在较新的 GHC 版本中为 instance Monad (Codensity (f :: k -> TYPE rep)) where）。似乎没有限制 f 必须是一个 monad。例如，MaybeT 的 monad 实例声明是 instance (Monad m) => Monad (MaybeT m) where，因此要求 m 是一个 monad。 - QuantumWiz

从那个意义上讲，是的，它比单子变换器更通用。我以为你指的是“Monad Codensity”，但它没有很好的类型化。 - Li-yao Xia

1

Codensity 对于单子来说，就像差异列表对于列表一样。另请参见计算作为幺半群的概念。 - Li-yao Xia

显示剩余3条评论

1

还有一个例子是具有两个不等价变换器的单子：选择单子。

 type Sel r a = (a -> r) -> a

Monad并不是很出名，但有一些论文提到它。这里有一个引用了一些论文的软件包：

https://hackage.haskell.org/package/transformers-0.6.0.4/docs/Control-Monad-Trans-Select.html

该软件包实现了一个转换器：

type SelT r m a = (a -> m r) -> m a

但是存在第二个变压器：

type Sel2T r m a = (m a -> r ) -> m a

证明这个变压器的定理更加困难，但我已经完成了。

第二个变压器的优点是它在 m 上是协变的，因此可以定义 hoist 函数：

 hoist :: (m a -> n a) -> Sel2T r m a -> Sel2T r n a

第二个变压器是“完全功能”，具有所有的提升和“起重机”。第一个变压器不是完全功能的；例如，您不能定义blift :: Sel r a -> SelT r m a。换句话说，您不能将来自Sel的单调计算嵌入到SelT中，就像您不能在Continuation monad和Codensity monad中这样做一样。

但是使用Sel2T变压器，所有提升都存在，并且您可以将Sel计算嵌入到Sel2T中。

这个例子展示了一个带有两个变压器的monad，而没有以任何方式使用Codensity构造。

- winitzki

选择单子是什么的简短直观解释存在吗？ - undefined

1

@QuantumWiz它返回一个类型为a的值，给定一个由类型a-> r的函数表示的"选择标准"。在最简单的非平凡情况下，取r = Boolean，所以类型为a -> r的函数只是一个断言，说明类型为a的给定值是"好"还是"坏"。类型为(a -> Boolean) -> a的选择函数将以某种方式返回满足这种断言的类型为a的值。 - undefined

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Daniel Wagner · Accepted Answer

这里有一个打破唯一性的反例想法。我们知道一般来说单子是不能组合的......但我们同时也知道，如果有适当的swap操作，你是可以把它们组合在一起的[1]！那么我们来为可以与自己交换的单子创建一个类。

-- | laws (from [1]):
-- swap . fmap (fmap f) = fmap (fmap f) . swap
-- swap . pure = fmap pure
-- swap . fmap pure = pure
-- fmap join . swap . fmap (join . fmap swap) = join . fmap swap . fmap join . swap
class Monad m => Swap m where
    swap :: m (m a) -> m (m a)

instance Swap Identity where swap = id
instance Swap Maybe where
    swap Nothing = Just Nothing
    swap (Just Nothing) = Nothing
    swap (Just (Just x)) = Just (Just x)

那么我们可以构建一个单子变换器，将一个单子与自身组合起来，如下所示：

newtype Twice m a = Twice (m (m a))

希望很明显“pure”和“(<$>)”是在做什么。我不会定义“(>>=)”，而是定义“join”，因为我认为这更容易理解；“(>>=)”可以从它派生。

instance Swap m => Monad (Twice m) where
    join = id
        . Twice                        -- rewrap newtype
        . fmap join . join . fmap swap -- from [1]
        . runTwice . fmap runTwice     -- unwrap newtype

instance MonadTrans Twice where lift = Twice . pure

我没有检查lift是否对所有Swap实例遵守MonadTrans法则，但我确实检查了Identity和Maybe的情况。

现在，我们有：

IdentityT Identity ~= Identity ~= Twice Identity
IdentityT Maybe    ~= Maybe   !~= Twice Maybe

这表明IdentityT不是产生Identity的唯一单子变换器。

[1] 由Mark P. Jones和Luc Duponcheel撰写的组合单子。