[Haskell-cafe] type questions again....
Nicholls, Mark
Nicholls.Mark at mtvne.com
Sat Jan 12 06:20:00 EST 2008
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
More information about the Haskell-Cafe
mailing list