[Haskell-cafe] type questions again....

[Nicholls, Mark]

Is my problem here, simply that the forall extension in GHC is misleading.....that the "forall" in
 
"MkSwizzle :: (forall a. Ord a => [a] -> [a]) -> Swizzle"
 
is not the same beast as the "forall" in..
 
data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a)

really
 
data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)

would be much better syntax....
 
don't get me wrong....I still don't especially understand...but if it's a misleading label...I can mentally substitute "exists" whenever I see a "forall" without a "=>".

________________________________

From: Luke Palmer [mailto:lrpalmer at gmail.com]
Sent: Fri 11/01/2008 18:03
To: Nicholls, Mark
Cc: haskell-cafe at haskell.org
Subject: Re: [Haskell-cafe] type questions again....



On Jan 11, 2008 5:47 PM, Nicholls, Mark <Nicholls.Mark at mtvne.com> wrote:
> > If you wrap an existential type up in a constructor, not
> > much changes:
>
> If you wrap a what?....should this read existential or universal?

Whoops, right, universal.

> > > newtype ID = ID (forall a. a -> a)
> >
> > ID can hold any value of type forall a. a -> a; i.e. it can hold any
> > value which exhibits the property that it can give me a value of type
> > a -> a for any type a I choose.  In this case the only things ID can
> > hold are id and _|_, because id is the only function that has that
> > type.   Here's how I might use it:
>
> It's the only function you've defined the type of....
>
> Id2 :: forall a. a -> a
>
> Now it can hold id2?

Well, that's not what I meant, but yes it can hold id2.

What I meant was that, in this case, id2 = _|_ or id2 = id, there are no
other possibilities.


> > > id' :: forall a. Num a => a -> a
> > > id' = id  -- it doesn't have to use the constraint if it doesn't
> want to
>
> "it doesn't have to use the constraint if it doesn't want to" ?
>
> If id was of type..
>
> Id::forall a. Ord a => a -> a
>
> Then I assume it would complain?

Yes.

> > but you need to use constructors to use
> > them.  I'll write them using GADTs, because I think they're a lot
> > clearer that way:
> >
> > data NUM' where
> >     NUM' :: Num a => a -> NUM'
> >
> > Look at the type of the constructor NUM'.  It has a universal type,
> > meaning whatever type a you pick (as long as it is a Num), you can
> > create a NUM' value with it.
>
> yes
>
> and then it goes wrong...
>
> > So the type contained inside the NUM'
> > constructor
>
> ?
>
> > is called existential (note that NUM' itself is just a
> > regular ADT; NUM' is not existential).
> >
>
> Why existential....see below...I have a guess

Okay, I was being handwavy here.  Explaining this will allow me to
clear this up.

If you take the non-GADT usage of an existential type:

data Foo
    = forall a. Num a => Foo a

That is isomorphic to a type:

data Foo
    = Foo (exists a. Num a => a)

Except GHC doesn't support a keyword 'exists', and if it did, it would only be
able to be used inside constructors like this (in order for inference
to be decidable),
so why bother?  That's what I meant by "the type inside the constructor", Foo is
not existential, (exists a. Num a => a) is.

> > So when you have:
> >
> > > negNUM' :: NUM' -> NUM'
> > > negNUM' (NUM' n) = NUM' (negate n)

Here n has an existential type, specifically (exists a. Num a => a).

> > Here the argument could have been constructed using any numeric type
> > n, so we know very little about it.  The only thing we know is that it
> > is of some type a, and that type has a Num instance.
>
> I think one of the harrowing things about Haskell is the practice of
> overloading data constructors with type names....it confuses the hell
> out of me....

Yeah that took a little getting used to for me too.  But how am I supposed
to come up with enough names if I want to name them differently!?  That
would require too much creativity...  :-)

> OK so this declaration says that forall x constructed using "NUM'
> n"...there *exists* a type T s.t. T is a member of type class NUM"...

(you probably meant type class Num here)

> which in term implies that that there exists the function negate...
>
> yes?

Huh, I had never thought of it like that, but yes.

I just realized that I think of programming in a way quite different
than I think of logic.  Maybe I should try to have my brain unify them.

> > > doubleNUM' :: NUM' -> NUM'
> > > doubleNUM' (NUM' n) = NUleM' (n + n)
> >
> > We can add it to itself, but note:
> >
> > > addNUM' :: NUM' -> NUM' -> NUM'
> > > addNUM' (NUM' a) (NUM' b) = NUM (a + b)  -- Illegal!
> >
> > We can't add them to each other, because the first argument could have
> > been constructed with, say, a Double and the other with a Rational.
> >
> > But do you see why we're allowed to add it to itself?
>
> We can add it to itself because "+" is of type "a->a->a"...

Yep, so whatever type a n happens to have, it matches both arguments.

> > How about this:
> >
> > > data Variant where
> > >    Variant :: a -> Variant
> >
> > This is a type that can be constructed with any value whatsoever.
> > Looks pretty powerful... but it isn't.  Why not?
> >
>
> Eeek.....
>
> Because a could be of any type whatsover?...so how I actually do
> anything with it?

Right.

Luke


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080112/3cedce9f/attachment.htm