On Monday 09 July 2007, Andrew Coppin wrote: > Stefan O'Rear wrote: > > All users should worry about is Quantifiers. > > > > A quantifier is an operator on types which defines a variable in some > > way. > > OK... > > > id has type :: ∀α. α → α > > > > toUpper (can) have type :: ∃α. α → α > > So... you're saying that id:: x -> x works for *every* possible choice > of x, but toUpper :: x -> x works for *one* possible choice of x?
Remember the quantifiers! id :: forall x. x -> x works for every choice of x, but toUpper :: exists x. x -> x works for only one choice of x. > (BTW... How in the hell do you get symbols like that in plain ASCII??) > > > If you're at all familiar with mathematics logic, don't hesistate to > > apply your intuitions about forall and exists - type systems and logics > > really are the same things. > > I have wide interests in diverse areas of science, mathematics and > computing, covering everything from cryptology to group theory to data > compression - but formal logic is something I've never been able to bend > my mind around. :-( > > > If you have a value of existential type, you can only do things with it > > that you can do with any type, because you don't know the actual type. > > Existential types hide information from the users. > > > > If you have a value of universal type, you can do things with it as if > > it had any matching type of your choice, because it doesn't know and > > can't care about the actual use type. Universal types hide information > > from the implementors. > > I stand in awe of people who actually understand what "universal" and > "existential" actually mean... To me, these are just very big words that > sound impressive. > > So, are you saying that if x is existential, it must work for any > possible x, but if x is universal, I can choose what x is? As the consumer of the value. For the producer, it works the other way around. > > In Haskell 98, existential quantification is not supported at all, and > > universal quantification is not first class - values can have universal > > types if and only if they are bound by let. You cannot pass universally > > typed values to functions. > > Erm... Jonathan Cast http://sourceforge.net/projects/fid-core http://sourceforge.net/projects/fid-emacs _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
