<br><br><div class="gmail_quote">On Mon, Aug 13, 2012 at 6:25 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">
<div class="im"><br>
<br>
On Mon, 13 Aug 2012, Ryan Ingram <<a href="mailto:ryani.spam@gmail.com" target="_blank">ryani.spam@gmail.com</a>> wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger <<a href="mailto:jays@panix.com" target="_blank">jays@panix.com</a>> wrote:<br>
<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>
<br>
</blockquote>
<br>
It's using the forall/exists duality:<br>
exsts a. P(a) <=> forall r. (forall a. P(a) -> r) -> r<br>
</blockquote>
<br></div>
;)<br>
<br>
This is, I think, a good joke. It has taken me a while, but I<br>
now understand that one of the most attractive things about<br>
Haskell is its sense of humor, which is unfailing.<br>
<br>
I will try to think about this, after trying your examples.<br>
<br>
I did suspect that, in some sense, "constraints" in combination<br>
with "forall" could give the quantifier "exists".<br><br></blockquote><div><br></div><div>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,</div>
<div><br></div><div>Ex Px <=> !Ax! Px (not all x's are not P)</div><div>and</div><div>Ax Px <=> !Ex! Px (there does not exist an x which is not P)</div><div><br></div><div>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".</div>
<div><br></div><div>Put these ideas together, and you will recover the duality as expressed earlier.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb">
<div class="h5">
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<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<br>
them in an existential type like this. Using 'case' to pattern match on<br>
the constructor unwraps the existential and makes any packed-up constraints<br>
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<br>
viewStream) is that the "s" type stored in the stream matches the "s" type<br>
taken and returned by the 'get next element' function. This allows the<br>
construction of another stream with the same function but a new state --<br>
MkStream s' k.<br>
<br>
It also allows the stream function in fibStream to be non-recursive which<br>
greatly aids the GHC optimizer in certain situations.<br>
<br>
-- ryan<br>
<br>
</blockquote>
<br></div></div><div class="HOEnZb"><div class="h5">
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>