Issues using id with natural transformations

[ecaustin]

Attempting to compile this code:

{-# LANGUAGE TypeOperators, RankNTypes #-}
module Test where

import Control.Natural

trans :: Maybe ~> []
trans Nothing = []
trans (Just x) = [x]

testFun :: (Maybe ~> []) -> (Maybe ~> [])
testFun = id

test fl = (if fl then testFun else id) trans

Gives this error:

[1 of 1] Compiling Test             ( Test.hs, interpreted )

Test.hs:14:36:
    Couldn't match type ‘forall x1. Maybe x1 -> [x1]’
                   with ‘Maybe x -> [x]’
    Expected type: Maybe ~> [] -> Maybe x -> [x]
      Actual type: Maybe ~> [] -> Maybe ~> []
    Relevant bindings include
      test :: Bool -> Maybe x -> [x] (bound at Test.hs:14:1)
    In the expression: id
    In the expression: if fl then testFun else id
Failed, modules loaded: none.

Note that the definition of testFun is id which GHC accepts, but the use of id in test is rejected.

This is with GHC 7.10.x.

[andygill]

Nice! I'm working on a idea to fix this. I want to try something before adding id.

[ecaustin]

Adding an explicit type annotation solves the issue:
test fl = (if fl then testFun else (id :: (Maybe ~> []) -> (Maybe ~> [])) trans

But using a polymorphic natural transformation doesn't:

idTrans :: a ~> a
idTrans = id

test fl = (if fl then testFun else idTrans) trans

All three should compile without error in my mind.

Is this one of facets of type-inference that RankNTypes breaks?

[andygill]

The test fails on

testFun :: (Maybe ~> []) -> (Maybe ~> [])
testFun = id

for me.

(Update: I had the wrong flag, sorry.)

[ecaustin]

What if you replace that with this?

testFun :: (Maybe ~> []) -> (Maybe ~> [])
testFun = undefined

[RyanGlScott]

Is this one of facets of type-inference that RankNTypes breaks?

I believe it is simply that. In the expression if fl then testFun else id, the term testFun has the type forall a. Maybe a -> [a], but the term id infers its type as Maybe b -> [b] without a forall (unless you give it a rank-n type ascription as you did above). Thus, we cannot unify a with b, since b is expected to be instantiated with a particular type, but a isn't allowed to do that.

That's why you can beta-reduce to if fl then testFun trans else id trans and have it typecheck, since GHC no longer needs to unify the type variables of testFun and id.

We could define a little combinator:

-- Please give me a better name
applyNT :: (f ~> g) -> f ~> g
applyNT = id -- or ($), if you like the application metaphor

Then this typechecks:

(if fl then testFun else applyNT) trans

[ecaustin]

Doh. You caught the blunder I made as I was rushing out the door at work.

My idTrans combinator is just reflexive, functional extensionality.

Really what we want, and what you showed with applyNT, is reflexivity of the transformation itself.

Good catch.

[andygill]

What do we call applyNT? I also want a better name, but can not think of one.

[ecaustin]

Well if functors are homomorphisms between categories and natural transformations are morphisms between functors then what we're talking about is an endomorphism between natural transformations, right?

So maybe endo would be a better name?

[andygill]

I see this all the time

type X (c :: Constraint) f g = (c m) => (f ~> m) -> (g ~> m)

... :: X Monad Example IO

which is also a natural transformation transformation. Wish I had a name for it as well.

[ecaustin]

I tried to write a version of your example that type-checked so I could better understand what you meant:

type X (c :: (* -> *) -> Constraint) f g m = (c m) => (f ~> m) -> (g ~> m)

That looks like it's expressing a homomorphism over natural transformations that changes the domain of the transformation?

I'm not sure why the constraint is involved, or if its even important, as the codomain of the transformation will stay fixed even without it.

[andygill]

The constraint is there because you can use forall m on the right hand side of the =.

[ecaustin]

Ah, gotcha. So the intended meaning was:

type X (c :: (* -> *) -> Constraint) f g =
  forall m. (c m) => (f ~> m) -> (g ~> m)

ex :: X MonadIO Maybe []

Is that right?

[andygill]

Yes. It appears again and again.

[ecaustin]

That's super interesting, I've never seen that before.
Is there anything that uses that pattern on Hackage that you know of?

It seems like without an accompanying transformation of type f ~> g that it wouldn't be particularly useful?

Edit: I got that backwards. We'd need g ~> f for the commutativity diagram to make sense, right?