[Haskell-cafe] handling rank 2 types

[Ralf Lammel]

In a type system like MLF, your original code may type check.

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. It is rather about functions with classic
rank-1 types. To see this, insert $ for the application of Empty:

fooBar :: [v] -> Empty
fooBar l = Empty $ (map no l)
 where
  no :: a -> a'
  no x = error "element found"

You get the same type error as for the original monadic code. What you
could do is define a suitably typed application operator (likewise, a
suitably typed liftM). (With MLF the various types would be admitted by
a more general type.) 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

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'"? Parametric polymorphism seems to suggest that we can't do much.
You can observe the length of the list. That's it, more or less. Why not
store the length directly rather than having this superficially
polymorphic list? I am a little bit lost.

You wonder how you can generally solve this sort of problem?
- You seem to spot the wrapping approach: wrap foralls and unpack at
application time. This makes particularly sense for polymorphic
*functions*.
- The other approach is to use consistently rank-2 combinators.

I probably don't get what you try to do.

Ralf

> -----Original Message-----
> From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe- 
> bounces at haskell.org] On Behalf Of Andrew Pimlott
> Sent: Thursday, November 03, 2005 8:35 PM
> To: haskell-cafe at haskell.org
> Subject: [Haskell-cafe] handling rank 2 types
> 
> I am trying to use a rank 2 type to enforce a condition on a data 
> structure.  For the purpose of this message, I am trying to ensure 
> that a list is empty (ignoring the possibility of bottom elements):
> 
> > {-# OPTIONS -fglasgow-exts #-}
> > import Control.Monad
> > newtype Empty = Empty (forall a. [a])
> 
> I want a function
> 
> > listToEmpty :: [v] -> IO Empty
> > listToEmpty l = liftM Empty (mapM no l) where
> >   no :: a -> IO a'
> >   no x = fail "element found"
> 
> But this gives a "less polymorphic" error.  I think the problem is 
> that ghc will not instantiate the "a'" in "IO a'" as a higher-rank 
> type because it occurs within a type contructor.  I believe this is 
> the restriction referred to at the end of 7.4.9[1].  If I instead 
> write
> 
> > uncheckedListToEmpty :: [v] -> Empty uncheckedListToEmpty l = Empty 
> > (map no l) where
> >   no :: a -> a'
> >   no x = error "element found"
> 
> it compiles, because "v'" can be instantiated as "forall v. Rule v", 
> and even pass through map with the higher-rank type.
> 
> Is there any way to make ghc accept the first definition?  I found 
> this
> workaround:
> 
> > newtype Any = Any { unAny :: forall a. a } listToEmptyAny :: [v] -> 
> > IO Empty listToEmptyAny l = liftM (\l -> Empty (map unAny l)) (mapM 
> > no l) where
> >   no :: a -> IO Any
> >   no x = fail "element found"
> 
> But needing a newtype wrapper Empty was bad enough; do I really need 
> one for every intermediate result (that is inside another type 
> constructor) as well?  I could probably define a generic family of 
> wrappers
> 
> > newtype Forall = Forall (forall a. a) newtype Forall1 c1 = Forall1 
> > (forall a. c1 a) newtype Forall2 c1 c2 = Forall2 (forall a. c1 c2 a)
> ...
> 
> But I would still have to use them everywhere.  Any other tricks?
> 
> Andrew
> 
> [1] http://haskell.org/ghc/docs/latest/html/users_guide/type-
> extensions.html#universal-quantification
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe