[Haskell-cafe] Data structure containing elements which are instances of the same type class
alex.solla at gmail.com
Tue Aug 14 03:53:11 CEST 2012
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)
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
>> 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
>> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe