RE: [Haskell-cafe] type questions again....
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 wrongI 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 existentialsee 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 namesit 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&#
RE: [Haskell-cafe] type questions again....
> -Original Message- > From: Luke Palmer [mailto:[EMAIL PROTECTED] > Sent: 11 January 2008 17:11 > To: Nicholls, Mark > Cc: haskell-cafe@haskell.org > Subject: Re: [Haskell-cafe] type questions again > > 2008/1/11 Nicholls, Mark <[EMAIL PROTECTED]>: > > Can someone explain (in simple terms) what is meant by existential and > > universal types. > > > > Preferably illustrating it in terms of logic rather than lambda > calculus. > > Well, I don't know about logic. While they are certainly related to > existential and universal types in logic, I don't really see a way to > explain them in terms of that. > > Universal types are easy, you use them every day in Haskell. Take for > example id: > > > id :: a -> a > > Or better illustrated (using ghc extension): > > > id :: forall a. a -> a > > That means that for any type a I pick, I can get a value of type a -> > a from id. Yepit's universal because forall types a. > If you wrap an existential type up in a constructor, not > much changes: If you wrap a what?should this read existential or 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? > > > applyID :: ID -> (Int,String) -> (Int,String) > > applyID (ID f) (i,s) = (f i, f s) > > Note how I can use f, which is a universal type, on both an Int and a > String in the same place. Yep. > > You can also put typeclass constraints on universals. Take the > universal type forall a. Num a => a -> a. Among functions that have > this type are: > > > add1 :: forall a. Num a => a -> a > > add1 x = x + 1 > > > 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? > > Wrapping this up in a constructor: > > > newtype NUM = NUM (forall a. Num a => a -> a) > > We can create values: > > > NUM add1 :: NUM > > NUM id :: NUM > > And use them: > > > applyNUM :: NUM -> (Int, Double) -> (Int, Double) > > applyNUM (NUM f) (i,d) = (f i, f d) > Yep. > > > Existential types are dual, Dual? (like a dual basis rather than double?) > 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 existentialsee below...I have a guess > So when you have: > > > negNUM' :: NUM' -> NUM' > > negNUM' (NUM' n) = NUM' (negate n) > > 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 namesit confuses the hell out of me 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"... which in term implies that that there exists the function negate... yes? It's existential...because the word "exists" occurred in the above translation. > So we can > perform operations to it which work for any Num type, such as negate, > but not things that only work for particular Num types, such as div. Because the existence of the value implies the existence of a type in the typeclass? > > > doubleNUM' :: NUM' -> NUM' > > doubleNUM' (NUM' n) = NUleM' (n + n) > > We can add it to itself, but note
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 existentialsee 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 namesit 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
Re: [Haskell-cafe] type questions again....
2008/1/11 Nicholls, Mark <[EMAIL PROTECTED]>: > Can someone explain (in simple terms) what is meant by existential and > universal types. > > Preferably illustrating it in terms of logic rather than lambda calculus. Well, I don't know about logic. While they are certainly related to existential and universal types in logic, I don't really see a way to explain them in terms of that. Universal types are easy, you use them every day in Haskell. Take for example id: > id :: a -> a Or better illustrated (using ghc extension): > id :: forall a. a -> a That means that for any type a I pick, I can get a value of type a -> a from id. If you wrap an existential type up in a constructor, not much changes: > 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: > applyID :: ID -> (Int,String) -> (Int,String) > applyID (ID f) (i,s) = (f i, f s) Note how I can use f, which is a universal type, on both an Int and a String in the same place. You can also put typeclass constraints on universals. Take the universal type forall a. Num a => a -> a. Among functions that have this type are: > add1 :: forall a. Num a => a -> a > add1 x = x + 1 > id' :: forall a. Num a => a -> a > id' = id -- it doesn't have to use the constraint if it doesn't want to Wrapping this up in a constructor: > newtype NUM = NUM (forall a. Num a => a -> a) We can create values: > NUM add1 :: NUM > NUM id :: NUM And use them: > applyNUM :: NUM -> (Int, Double) -> (Int, Double) > applyNUM (NUM f) (i,d) = (f i, f d) Existential types are dual, 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. So the type contained inside the NUM' constructor is called existential (note that NUM' itself is just a regular ADT; NUM' is not existential). So when you have: > negNUM' :: NUM' -> NUM' > negNUM' (NUM' n) = NUM' (negate n) 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. So we can perform operations to it which work for any Num type, such as negate, but not things that only work for particular Num types, such as div. > 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? 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? Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type questions again....
On 11/01/2008, Nicholls, Mark <[EMAIL PROTECTED]> wrote: > Preferably illustrating it in terms of logic rather than lambda calculus. > > > There's plenty of stuff out there on it….but most of it seems double dutch > (no offense to the dutch intended). > I think the preferred idiom, considering the notation, is that "it's all Greek to me" ;-) D -- Dougal Stanton [EMAIL PROTECTED] // http://www.dougalstanton.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
