<br><br><div class="gmail_quote">On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger <span dir="ltr"><<a href="mailto:jays@panix.com" target="_blank">jays@panix.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Does Haskell have a word for "existential type" declaration? I<br>
have the impression, and this must be wrong, that "forall" does<br>
double duty, that is, it declares a "for all" in some sense like<br>
the usual "for all" of the Lower Predicate Calculus, perhaps the<br>
"for all" of system F, or something near it.<br></blockquote></div><br>It's using the forall/exists duality:<br> exsts a. P(a) <=> forall r. (forall a. P(a) -> r) -> r<br><br>For example:<br>
(exists a. Show a => a) <=> forall r. (forall a. Show a => a -> r) -> r<br><br>This also works when you look at the type of a constructor:<br><br> data Showable = forall a. Show a => MkShowable a<br>
-- MkShowable :: forall a. Show a => a -> Showable<br><br> caseShowable :: forall r. (forall a. Show a => a -> r) -> Showable -> r<br> caseShowable k (MkShowable x) = k x<br><br> testData :: Showable<br>
testData = MkShowable (1 :: Int)<br> <br> useData :: Int<br> useData = case testData of (MkShowable x) -> length (show x)<br><br> useData2 :: Int<br> useData2 = caseShowable (length . show) testData<br>
<br>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.<br>
<br>An example of existentials without using constraints directly:<br><br> data Stream a = forall s. MkStream s (s -> Maybe (a,s))<br><br> viewStream :: Stream a -> Maybe (a, Stream a)<br> viewStream (MkStream s k) = case k s of<br>
Nothing -> Nothing<br> Just (a, s') -> Just (a, MkStream s' k)<br><br> takeStream :: Int -> Stream a -> [a]<br> takeStream 0 _ = []<br> takeStream n s = case viewStream s of<br>
Nothing -> []<br> Just (a, s') -> a : takeStream (n-1) s'<br><br> fibStream :: Stream Integer<br> fibStream = Stream (0,1) (\(x,y) -> Just (x, (y, x+y)))<br><br>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.<br>
<br>It also allows the stream function in fibStream to be non-recursive which greatly aids the GHC optimizer in certain situations.<br><br> -- ryan<br>