foralls in newtypes

[Andrew J Bromage]

G'day all.

On Wed, Oct 16, 2002 at 07:54:17AM -0700, Hal Daume III wrote:

> I was reading the HFL libs, namely Control.Monad.Logic, and there's a
> definition in there:
> 
> newtype Logic a = Logic { mkLogic :: (forall b. (a -> b -> b) -> b -> b) }
> 
> I'm curious why this is legal, but
> 
> newtype Logic2 a = forall b . Logic2 ((a -> b -> b) -> b -> b)
> 
> is not...

Firstly, it's not the same type, but you probably worked that much
out by yourself.  You don't want an existentially quantified
constructor at all, what you want is a constructor with a single
argument which has an existentially quantified function type.

Secondly, I've changed the definition of Logic since you looked at
it, so this is no longer valid.  We'll look at a simpler example
anyway, using data instead of newtype:

	data CPS a = forall b. CPS ((a -> b) -> b)

What should the type of this function be?

	mkCPS (CPS x) = x

Cheers,
Andrew Bromage