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

[Alexander Solla]

On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger <jays at panix.com> wrote:

>
>
> 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".
>
>
In a classical logic, the duality is expressed by !E! = A, and !A! = E,
where E and A are backwards/upsidedown and ! represents negation.  In
particular, for a proposition P,

Ex Px <=> !Ax! Px (not all x's are not P)
and
Ax Px <=> !Ex! Px (there does not exist an x which is not P)

Negation is relatively tricky to represent in a constructive logic -- hence
the use of functions/implications and bottoms/contradictions.  The type
ConcreteType -> b represents the negation of ConcreteType, because it shows
that ConcreteType "implies the contradiction".

Put these ideas together, and you will recover the duality as expressed
earlier.


>
>
>
>> 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
>>
>>
> ______________________________**_________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120813/dd98e94b/attachment.htm>