[Haskell-cafe] handling rank 2 types

[Andrew Pimlott]

On Thu, Nov 03, 2005 at 11:57:49PM -0800, Ralf Lammel wrote:
> Let's do an experiment.
> We replace the IO monad by the Id(entity) monad.
> We actually replace the Id newtype also to become true type-level
> identity.
> So we get:
> 
> --
> -- This is like your 2nd say unchecked... sample
> --
> 
> fooBar :: [v] -> Empty
> fooBar l = Empty (map no l)
>  where
>   no :: a -> a'
>   no x = error "element found"
> 
> But the problem is not about "a higher-rank type occurring with a type
> constructor", as you guess.

I thought my explanation sounded fishy.  Someone else explained this to
me off-list as well.

> It is rather about functions with classic rank-1 types.
...
> What you could do is define a suitably typed application operator
> (likewise, a suitably typed liftM).
...
> In the non-monadic example, we need:
> 
> -- Use app instead of ($)
> app :: ((forall a. [a]) -> c) -> (forall b. [b]) -> c
> app f x = f x

Ok, but this would have to be rewritten for different kinds:

    app1 :: ((forall a. c1 a) -> c) -> (forall b. c1 b) -> c
    app1 f x = f x
    app2 :: ((forall a. c1 c2 a) -> c) -> (forall b. c1 c2 b) -> c
    app2 f x = f x
    ...

Furthermore, I don't believe it works for me.  I would need something
like

    liftM' :: Monad m => (forall a. [a] -> c) -> m (forall b. [b]) -> m c
    liftM' f x = ???

First, the type is illegal: "you cannot make a forall-type the argument
of a type constructor".  Second, even if it were, I would need versions
of the monad operators with custom types to implement it, eg

    bind :: Monad m => m (forall a. [a]) -> ((forall b. [b]) -> m c) -> m c

Or am I wrong?  An alternate (and legal) signature for liftM' is

    liftM' :: Monad m => (forall a. [a] -> c) -> (forall b. m [b]) -> m c

but to implement this, I think I would need

    bind :: Monad m => (forall a. m [a]) -> ((forall b. [b]) -> m c) -> m c

I tried implementing this just for Maybe:

    bindMaybe :: (forall a. Maybe [a]) -> ((forall b. [b]) -> Maybe c) ->
                    Maybe c
    bindMaybe x f = case x of
      Just x' -> f x'
      Nothing -> Nothing

But as expected, it doesn't typecheck, and AFAICT it shouldn't.

So my conclusion is that writing my own higher-ranked library wouldn't
work; I would still need newtype wrappers.

> BTW, what operations are we supposed to perform on the content of Empty;
> what's the real purpose for introducing this independent type variable
> "a'"?

Suppose instead

    newtype NoRight = NoRight (forall a. [Either Int a])

An alternative might be

    data No
    type NoRight = [Either Int No]

But the first version I can use directly (after unwrapping NoRight) as
an [Either Int Int], [Either Int String], etc.

My real purpose is to enforce that a logical statement has no variables.

Andrew