<HTML dir=ltr><HEAD><TITLE>Re: [Haskell-cafe] type questions again....</TITLE>
<META http-equiv=Content-Type content="text/html; charset=unicode">
<META content="MSHTML 6.00.6000.16587" name=GENERATOR></HEAD>
<BODY>
<DIV id=idOWAReplyText91147 dir=ltr>
<DIV dir=ltr><FONT face=Arial color=#000000 size=2>Is my problem here, simply that the forall extension in GHC is misleading.....that the "forall" in</FONT></DIV>
<DIV dir=ltr><FONT face=Arial size=2></FONT> </DIV>
<DIV dir=ltr>"MkSwizzle :: (forall a. Ord a => [a] -> [a]) -> Swizzle"</DIV>
<DIV dir=ltr> </DIV>
<DIV dir=ltr>is not the same beast as the "forall" in..</DIV>
<DIV dir=ltr> </DIV>
<DIV dir=ltr>data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a)<BR></DIV>
<DIV dir=ltr>really</DIV>
<DIV dir=ltr> </DIV>
<DIV dir=ltr>data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)<BR></DIV>
<DIV dir=ltr>would be much better syntax....</DIV>
<DIV dir=ltr> </DIV>
<DIV dir=ltr>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 "=>".<BR>
<HR tabIndex=-1>
<FONT face=Tahoma size=2><B>From:</B> Luke Palmer [mailto:lrpalmer@gmail.com]<BR><B>Sent:</B> Fri 11/01/2008 18:03<BR><B>To:</B> Nicholls, Mark<BR><B>Cc:</B> haskell-cafe@haskell.org<BR><B>Subject:</B> Re: [Haskell-cafe] type questions again....<BR></FONT><BR></DIV></DIV>
<DIV>
<P><FONT size=2>On Jan 11, 2008 5:47 PM, Nicholls, Mark <Nicholls.Mark@mtvne.com> wrote:<BR>> > If you wrap an existential type up in a constructor, not<BR>> > much changes:<BR>><BR>> If you wrap a what?....should this read existential or universal?<BR><BR>Whoops, right, universal.<BR><BR>> > > newtype ID = ID (forall a. a -> a)<BR>> ><BR>> > ID can hold any value of type forall a. a -> a; i.e. it can hold any<BR>> > value which exhibits the property that it can give me a value of type<BR>> > a -> a for any type a I choose. In this case the only things ID can<BR>> > hold are id and _|_, because id is the only function that has that<BR>> > type. Here's how I might use it:<BR>><BR>> It's the only function you've defined the type of....<BR>><BR>> Id2 :: forall a. a -> a<BR>><BR>> Now it can hold id2?<BR><BR>Well, that's not what I meant, but yes it can hold id2.<BR><BR>What I meant was that, in this case, id2 = _|_ or id2 = id, there are no<BR>other possibilities.<BR><BR><BR>> > > id' :: forall a. Num a => a -> a<BR>> > > id' = id -- it doesn't have to use the constraint if it doesn't<BR>> want to<BR>><BR>> "it doesn't have to use the constraint if it doesn't want to" ?<BR>><BR>> If id was of type..<BR>><BR>> Id::forall a. Ord a => a -> a<BR>><BR>> Then I assume it would complain?<BR><BR>Yes.<BR><BR>> > but you need to use constructors to use<BR>> > them. I'll write them using GADTs, because I think they're a lot<BR>> > clearer that way:<BR>> ><BR>> > data NUM' where<BR>> > NUM' :: Num a => a -> NUM'<BR>> ><BR>> > Look at the type of the constructor NUM'. It has a universal type,<BR>> > meaning whatever type a you pick (as long as it is a Num), you can<BR>> > create a NUM' value with it.<BR>><BR>> yes<BR>><BR>> and then it goes wrong...<BR>><BR>> > So the type contained inside the NUM'<BR>> > constructor<BR>><BR>> ?<BR>><BR>> > is called existential (note that NUM' itself is just a<BR>> > regular ADT; NUM' is not existential).<BR>> ><BR>><BR>> Why existential....see below...I have a guess<BR><BR>Okay, I was being handwavy here. Explaining this will allow me to<BR>clear this up.<BR><BR>If you take the non-GADT usage of an existential type:<BR><BR>data Foo<BR> = forall a. Num a => Foo a<BR><BR>That is isomorphic to a type:<BR><BR>data Foo<BR> = Foo (exists a. Num a => a)<BR><BR>Except GHC doesn't support a keyword 'exists', and if it did, it would only be<BR>able to be used inside constructors like this (in order for inference<BR>to be decidable),<BR>so why bother? That's what I meant by "the type inside the constructor", Foo is<BR>not existential, (exists a. Num a => a) is.<BR><BR>> > So when you have:<BR>> ><BR>> > > negNUM' :: NUM' -> NUM'<BR>> > > negNUM' (NUM' n) = NUM' (negate n)<BR><BR>Here n has an existential type, specifically (exists a. Num a => a).<BR><BR>> > Here the argument could have been constructed using any numeric type<BR>> > n, so we know very little about it. The only thing we know is that it<BR>> > is of some type a, and that type has a Num instance.<BR>><BR>> I think one of the harrowing things about Haskell is the practice of<BR>> overloading data constructors with type names....it confuses the hell<BR>> out of me....<BR><BR>Yeah that took a little getting used to for me too. But how am I supposed<BR>to come up with enough names if I want to name them differently!? That<BR>would require too much creativity... :-)<BR><BR>> OK so this declaration says that forall x constructed using "NUM'<BR>> n"...there *exists* a type T s.t. T is a member of type class NUM"...<BR><BR>(you probably meant type class Num here)<BR><BR>> which in term implies that that there exists the function negate...<BR>><BR>> yes?<BR><BR>Huh, I had never thought of it like that, but yes.<BR><BR>I just realized that I think of programming in a way quite different<BR>than I think of logic. Maybe I should try to have my brain unify them.<BR><BR>> > > doubleNUM' :: NUM' -> NUM'<BR>> > > doubleNUM' (NUM' n) = NUleM' (n + n)<BR>> ><BR>> > We can add it to itself, but note:<BR>> ><BR>> > > addNUM' :: NUM' -> NUM' -> NUM'<BR>> > > addNUM' (NUM' a) (NUM' b) = NUM (a + b) -- Illegal!<BR>> ><BR>> > We can't add them to each other, because the first argument could have<BR>> > been constructed with, say, a Double and the other with a Rational.<BR>> ><BR>> > But do you see why we're allowed to add it to itself?<BR>><BR>> We can add it to itself because "+" is of type "a->a->a"...<BR><BR>Yep, so whatever type a n happens to have, it matches both arguments.<BR><BR>> > How about this:<BR>> ><BR>> > > data Variant where<BR>> > > Variant :: a -> Variant<BR>> ><BR>> > This is a type that can be constructed with any value whatsoever.<BR>> > Looks pretty powerful... but it isn't. Why not?<BR>> ><BR>><BR>> Eeek.....<BR>><BR>> Because a could be of any type whatsover?...so how I actually do<BR>> anything with it?<BR><BR>Right.<BR><BR>Luke<BR></FONT></P></DIV></BODY></HTML>