[Haskell-cafe] Data structure containing elements which are instances of the same type class
jays at panix.com
Tue Aug 14 03:25:47 CEST 2012
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".
> 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
More information about the Haskell-Cafe