[Haskell-cafe] Data structure containing elements which are instances of the same type class

[Jay Sulzberger]

On Mon, 13 Aug 2012, Ryan Ingram <ryani.spam at gmail.com> wrote:

> On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger <jays at panix.com> wrote:
>
>> Does Haskell have a word for "existential type" declaration?  I
>> have the impression, and this must be wrong, that "forall" does
>> double duty, that is, it declares a "for all" in some sense like
>> the usual "for all" of the Lower Predicate Calculus, perhaps the
>> "for all" of system F, or something near it.
>>
>
> It's using the forall/exists duality:
>    exsts a. P(a)  <=>  forall r. (forall a. P(a) -> r) -> r

;)

This is, I think, a good joke.  It has taken me a while, but I
now understand that one of the most attractive things about
Haskell is its sense of humor, which is unfailing.

I will try to think about this, after trying your examples.

I did suspect that, in some sense, "constraints" in combination
with "forall" could give the quantifier "exists".

Thanks, ryan!

oo--JS.


>
> For example:
>    (exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r
>
> This also works when you look at the type of a constructor:
>
>    data Showable = forall a. Show a => MkShowable a
>    -- MkShowable :: forall a. Show a => a -> Showable
>
>    caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r
>    caseShowable k (MkShowable x) = k x
>
>    testData :: Showable
>    testData = MkShowable (1 :: Int)
>
>    useData :: Int
>    useData = case testData of (MkShowable x) -> length (show x)
>
>    useData2 :: Int
>    useData2 = caseShowable (length . show) testData
>
> Haskell doesn't currently have first class existentials; you need to wrap
> them in an existential type like this.  Using 'case' to pattern match on
> the constructor unwraps the existential and makes any packed-up constraints
> available to the right-hand-side of the case.
>
> An example of existentials without using constraints directly:
>
>    data Stream a = forall s. MkStream s (s -> Maybe (a,s))
>
>    viewStream :: Stream a -> Maybe (a, Stream a)
>    viewStream (MkStream s k) = case k s of
>        Nothing -> Nothing
>        Just (a, s') -> Just (a, MkStream s' k)
>
>    takeStream :: Int -> Stream a -> [a]
>    takeStream 0 _ = []
>    takeStream n s = case viewStream s of
>        Nothing -> []
>        Just (a, s') -> a : takeStream (n-1) s'
>
>    fibStream :: Stream Integer
>    fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))
>
> Here the 'constraint' made visible by pattern matching on MkStream (in
> viewStream) is that the "s" type stored in the stream matches the "s" type
> taken and returned by the 'get next element' function.  This allows the
> construction of another stream with the same function but a new state --
> MkStream s' k.
>
> It also allows the stream function in fibStream to be non-recursive which
> greatly aids the GHC optimizer in certain situations.
>
>  -- ryan
>