是否有可能在同一个函数中以不同方式实例化多态代码？

Question

好吧,我不知道怎么做,但是知道Haskell是一种无限深度的语言,我决定在放弃之前问这个问题.

假设我们有一个多态的值,例如:

foo :: Monad m => m Int
foo = return Int

显然,根据上下文,m可以实例化为不同的类型.我想知道现在是否可以采用这段抽象代码并在同一函数内的几个不同的上下文中使用它(例如在覆盖代码时减少样板):

bar :: Monad m => m Int -> Property
bar m = conjoin
  [ checkIt (runIdentityT m)
  , checkIt (runReaderT m ())
  , …
  ]

哪里checkIt接受一些具体的monad.由于foo本质上是抽象的描述如何做某事,应该可以在几个上下文中使用它,但问题显然是如果我们承诺使用任何Monad m => m Int签名bar,那么我们就不能在不太抽象的层次上编写这个函数了它不可能适应Monad其实现中的每个可能的实例.

---

有没有办法通过foo进入bar这样就可以在里面几个类型的环境中使用？

Answer 1

你想要rank-2类型:

bar :: (forall m. Monad m => m Int) -> Property
bar m = conjoin
  [ checkIt (runIdentityT m)
  , checkIt (runReaderT m ())
  , …
  ]

现在,bar foo将打字检查.

具体地说,类型(forall m. Monad m => m Int)要求参数是多态的并且可用于所有 monad m.通过比较,原始类型

bar :: Monad m => m Int -> Property

只需要参数有型的形式m Int为一些单子m.在你的情况下,你显然想要"为所有人",而不是"为某些人".

您可以通过在文件顶部放置以下行来启用rank-2类型:

{-# LANGUAGE Rank2Types #-}

从理论上讲,我的胆量告诉我这种类型

(forall m. Monad m => m Int)

实际上是同构的

Int

与同构:

iso :: Int -> (forall m. Monad m => m Int)
iso x = return x

osi :: (forall m. Monad m => m Int) -> Int
osi m = runIdentity m

由于与之相关的自由定理,上述确实应该是一个同构forall m. Monad m => m Int.

如果我的直觉是正确的,我认为,这意味着该类型的每个值forall m. Monad m => m Int 都必须具有return x某个整数的形式x.

所以,最后的反问题是:你为什么不简单地传递一个Int,并删除不需要的rank-2机器？