[Haskell-cafe] Existential types (Was: Type vs TypeClass duality)

Dan Weston westondan at imageworks.com
Wed Oct 24 14:59:53 EDT 2007


Thanks for the concise explanation. I do have one minor question though.

 > -+- A more useful example is
 >
 >     ∃a. Show a => a   i.e.  ∃a.(a -> String, a)
 >
 > So, given a value (f,x) :: ∃a.(a -> String, a), we can do
 >
 >     f x :: String
 >
 > but that's pretty much all we can do. The type is isomorphic to a simple
 > String.

Don't you mean *epimorphic* instead of isomorphic (not that it matters)? 
For any existential type a of cardinality less than that of String, it 
is isomorphic, but if a = String, then by Cantor's theorem String -> 
String has a cardinality greater than String and cannot be isomorphic to it.

 >     ∃a.(a -> String, a)  ~  String
 >
 > So, instead of storing a list [∃a. Show a => a], you may as well store a
 > list of strings [String].

True. This loses no observable information because (given the 
existential) even if there may be no unique function for a given String, 
there would be no way to tell any two such apart anyway, as the only 
thing you can do with them is to apply the functions of Show, and they 
all return the same String.

apfelmus wrote:
> TJ wrote:
>>>
>>>     data Showable = forall a. Show a => Showable a
>>>     stuff = [Showable 42, Showable "hello", Showable 'w']
>>
>> Which is exactly the kind of 2nd-rate treatment I dislike.
>>
>> I am saying that Haskell's type system forces me to write boilerplate.
> 
> Nice :) I mean, the already powerful Hindley-Milner type system is free 
> of type annotations (= boilerplate). It's existential types and other 
> higher-rank types that require annotations because type inference in 
> full System F (the basis of Haskell's type system so to speak) is not 
> decidable. In other words, there is simply no way to have System F 
> without boilerplate.
> 
> That being said, there is still the quest for a minimal amount of 
> boilerplate and in the right place. That's quite a hard problem, but 
> people are working on that, see for instance
> 
> http://research.microsoft.com/~simonpj/papers/gadt/index.htm
> http://research.microsoft.com/~simonpj/papers/higher-rank/index.htm
> http://research.microsoft.com/users/daan/download/papers/mlftof.pdf
> http://research.microsoft.com/users/daan/download/papers/existentials.pdf
> 
>>>
>>>      [exists a. Show a => a]
>>
>> I actually don't understand that line. Substituting forall for exists,
>> someone in my previous thread said that it means every element in the
>> list is polymorphic, which I don't understand at all, since trying to
>> cons anything onto the list in GHCi results in type errors.
> 
> Let's clear the eerie fog surrounding universal quantification in this 
> thread.
> 
> -+- The mathematical symbol for  forall  is  ∀  (Unicode)
>                                  exists  is  ∃
> 
> -+- ∀a.(a -> a) means:
>     you give me a function (a -> a) that I can apply
>     to _all_ argument types  a  I want.
> 
>   ∃a.(a -> a) means:
>     you give me a function (a -> a) and tell me that
>     _there is_ a type  a  that I can apply this function to.
>     But you don't tell me the type  a  itself. So, this particular
>     example ∃a.(a -> a) is quite useless and can be replaced with ().
> 
> -+- A more useful example is
> 
>     ∃a. Show a => a   i.e.  ∃a.(a -> String, a)
> 
> So, given a value (f,x) :: ∃a.(a -> String, a), we can do
> 
>     f x :: String
> 
> but that's pretty much all we can do. The type is isomorphic to a simple 
> String.
> 
>     ∃a.(a -> String, a)  ~  String
> 
> So, instead of storing a list [∃a. Show a => a], you may as well store a 
> list of strings [String].
> 
> -+- Since ∀ and ∃ are clearly different, why does Haskell have only one 
> of them and even uses ∀ to declare existential types? The answer is the 
> following relation:
> 
>   ∃a.(a -> a) = ∀b. (∀a.(a -> a) -> b) -> b
> 
> So, how to compute a value  b  from an existential type ∃a.(a -> a)? 
> Well, we have to use a function  ∀a.(a -> a) -> b  that works for any 
> input type (a -> a) since we don't know which one it will be.
> 
> More generally, we have
> 
>   ∃a.(f a)    = ∀b. (∀a.(f a) -> b) -> b
> 
> for any type  f a  that involves a, like
> 
>   f a = Show a => a
>   f a = a -> a
>   f a = (a -> String, a)
> 
> and so on.
> 
> Now, the declaration
> 
>   data Showable = forall a. Show a => Showable a
> 
> means that the constructor Showable gets the type
> 
>   Showable :: ∀a. Show a => a -> Showable
> 
> and the deconstructor is
> 
>   caseS :: Showable -> ∀b. (∀a.(Show a => a) -> b) -> b
>   caseS sx f = case sx of { Showable x -> f x }
> 
> which is the same as
> 
>   caseS :: Showable -> ∃a. Show a => a
> 
> . GADT-notation clearly shows the ∀
> 
>   data Showable where
>     Showable :: ∀a -> Showable
> 
> 
> -+- The position of the quantifier matters.
> - Exercise 1: Explain why
> 
>   [∀a.a]  ∀a.[a]  [∃a.a]  and  ∃a.[a]
> 
> are all different.
> - Exercise 2: ∀ can be lifted along function arrows, whereas ∃ can't. 
> Explain why
> 
>   String -> ∀a.a   =   ∀a.String -> a
>   String -> ∃a.a  =/=  ∃a.String -> a
> 
> Since ∀ can always be lifted to the top, we usually don't write it 
> explicitly in Haskell.
> 
> -+- Existential types are rather limited when used for OO-like stuff but 
> are interesting for ensuring invariants via the type system or when 
> implementing algebraic data types. Here the "mother of all monads" in 
> GADT-notation
> 
>   data FreeMonad a where
>     return :: a -> FreeMonad a
>     (>>=)  :: ∀b. FreeMonad b -> (b -> FreeMonad a) -> FreeMonad a
> 
> Note the existential quantification of  b . (The ∀b can be dropped, like 
> the ∀a has been.)
> 
> 
> Regards,
> apfelmus
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
> 




More information about the Haskell-Cafe mailing list