[Haskell-cafe] Data structure containing elements which are instances of the same type class

[Jay Sulzberger]

On Mon, 13 Aug 2012, Alexander Solla <alex.solla at gmail.com> wrote:

> On Mon, Aug 13, 2012 at 6:25 PM, Jay Sulzberger <jays at panix.com> wrote:
>
>>
>>
>> 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".
>>
>>
> 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)

Yes.

>
> 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".

I am becoming sensitized to this distinction.  I now, I think,
feel the impulse toward "constructivism", that is, the
assumption/delusion^Waspiration that all functions from the reals
to the reals are continuous.  One argument that helped me goes:

  The reals between 0 and 1 are functions from the integers to say {0, 1}.

  They are attained as limits of functions f: iota(n) -> {0, 1}, as
  n becomes larger and larger and ... , where iota(n) is a set with
  n elements, n a finite integer.

  So, our objects, the reals, are attained as limits.  And the
  process of proceeding toward the limit is "natural", "functorial"
  in the sense of category theory.

  Thus so also our morphisms, that is functions from the reals to
  the reals, must be produced functorially as limits of maps
  between objects f: iota(n) -> {0, 1}.

>
> Put these ideas together, and you will recover the duality as expressed
> earlier.

Thanks!  I am reading some blog posts and I was impressed by the
buffalo hair here:

   http://existentialtype.wordpress.com/2012/08/11/extensionality-intensionality-and-brouwers-dictum/

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 at haskell.org
>> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>>
>