Is it possible to instantiate polymorphic piece of code differently in the same function?

Question

OK, I don't see how it can be done, but knowing that Haskell is a language of infinite depth, I decided to ask this here before giving up.

Suppose we have a value that is polymorphic, for example:

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

Obviously, depending on context, m can be instantiated to different types. I wonder if it's possible now to take this abstract piece of code and use it in several different contexts inside the same function (for example to reduce boilerplate when covering code):

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

Where checkIt accepts some concrete monad. Since foo is essentially abstract description how to do something, it should be possible to use it in several contexts, but the problem is obviously that if we promise to work with any Monad m => m Int in signature of bar, then we cannot write this function on less abstract level since then it's not possible to accommodate to every possible instance of Monad in its implementation.

---

Is there a way to pass foo into bar so it can be used in several type contexts inside it?

Answer 1

You want rank-2 types:

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

Now, bar foo will type check.

Concretely, the type (forall m. Monad m => m Int) requires the argument to be polymorphic and usable for all monads m. By comparison, the original type

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

only requires the argument to have a type of the form m Int for some monad m. In your case, you clearly want "for all", and not "for some".

You can enable rank-2 types by putting at the top of your file the following line:

{-# LANGUAGE Rank2Types #-}

---

On a more theoretical note, my guts are telling me that the type

(forall m. Monad m => m Int)

is actually isomorphic to

Int

with isomorphisms:

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

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

The above should indeed be an isomorphism thanks to the free theorem associated to forall m. Monad m => m Int.

If my intuition is correct, as I believe, this means that every value of the type forall m. Monad m => m Int has to have the form return x for some integer x.

So, the final counter-question is: why don't you simply pass an Int, and remove the unneeded rank-2 machinery?