On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger <j...@panix.com> wrote:
> > > 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". > > 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) and 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 earlier. > > > >> 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<http://www.haskell.org/mailman/listinfo/haskell-cafe> >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
