On Mon, 13 Aug 2012, Ryan Ingram <ryani.s...@gmail.com> wrote:
On Mon, Aug 13, 2012 at 12:30 PM, Jay Sulzberger <j...@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".
Thanks, ryan!
oo--JS.
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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
