[Haskell-cafe] type questions again....
Luke Palmer
lrpalmer at gmail.com
Fri Jan 11 13:03:02 EST 2008
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
More information about the Haskell-Cafe
mailing list