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:[EMAIL PROTECTED] Sent: Fri 11/01/2008 18:03 To: Nicholls, Mark Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] type questions again.... On Jan 11, 2008 5:47 PM, Nicholls, Mark <[EMAIL PROTECTED]> 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
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe