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

[Ryan Ingram]

Also, I have to admit I was a bit handwavy here; I meant P in a
metatheoretic sense, that is "P(a) is some type which contains 'a' as a
free variable", and thus the 'theorem' is really a collection of theorems
parametrized on the P you choose.

For example, P(a) could be "Show a & a -> Int"; in that case we get the
theorem

exists a. (Show a, a -> Int)
 <=>
forall r. (forall a. Show a => (a -> Int) -> r) -> r

as witnessed by the following code (using the ExistentialQuantification and
RankNTypes extensions)

data P = forall a. Show a => MkP (a -> Int)
type CPS_P r = (forall a. Show a => (a -> Int) -> r) -> r

isoR :: P -> forall r. CPS_P r
isoR (MkP f) k =
   -- pattern match on MkP brings a fresh type T into scope,
   --     along with f :: T -> Int, and the constraint Show T.
   -- k :: forall a. Show a => (a -> Int) -> r
   -- so, k {T} f :: r


isoL :: (forall r. CPS_P r) -> P
isoL k = k (\x -> MkP x)
-- k :: forall r. (forall a. Show a => (a -> Int) -> r) -> r
-- k {P} = (forall a. Show a => (a -> Int) -> P) -> P
-- MkP :: forall a. Show a => (a -> Int) -> P
-- therefore, k {P} MkP :: P

Aside: the type 'exists a. (Show a, a -> Int)' is a bit odd, and is another
reason we don't have first class existentials in Haskell.  The 'forall'
side is using currying (a -> b -> r) <=> ((a,b) -> r) which works because
the constraint => can be modeled by dictionary passing.  But we don't have
a simple way to represent the dictionary (Show a) as a member of a tuple.

One answer is to pack it up in another "existential"; I find this a bit of
a misnomer since there's nothing existential about this data type aside
from the dictionary:

data ShowDict a = Show a => MkShowDict

Then the theorem translation is a bit more straightforward:

data P = forall a. MkP (ShowDict a, a -> Int)
type CPS_P r = (forall a. (ShowDict a, a -> Int) -> r) -> r

-- theorem: P <=> forall r. CPS_P r

isoL :: P -> forall r. CPS_P r
isoL (MkP x) k = k x

isoR :: (forall r. CPS_P r) -> P
isoR k = k (\x -> MkP x)

  -- ryan

On Sat, Aug 18, 2012 at 8:24 PM, wren ng thornton <wren at freegeek.org> wrote:

> On 8/17/12 12:54 AM, Alexander Solla wrote:
>
>> On Thu, Aug 16, 2012 at 8:07 PM, wren ng thornton <wren at freegeek.org>
>> wrote:
>>
>>> Though bear in mind we're discussing second-order quantification here,
>>> not
>>> first-order.
>>>
>>
>> Can you expand on what you mean here?  I don't see two kinds of
>> quantification in the type language (at least, reflexively, in the context
>> of what we're discussing).  In particular, I don't see how to quantify
>> over
>> predicates for (or sets of, via the extensions of the predicates) types.
>>
>> Is Haskell's 'forall' doing double duty?
>>
>
> Nope, it's the "forall" of mathematics doing double duty :)
>
> Whenever doing quantification, there's always some domain being quantified
> over, though all too often that domain is left implicit; whence lots of
> confusion over the years. And, of course, there's the scope of the
> quantification, and the entire expression. For example, consider the
> expression:
>
>     forall a. P(a)
>
> The three important collections to bear in mind are:
> (1) the collection of things a ranges over
> (2) the collection of things P(a) belongs to
> (3) the collection of things forall a. P(a) belongs to
>
> So if we think of P as a function from (1) to (2), and name the space of
> such functions (1->2), then we can think of the quantifier as a function
> from (1->2) to (3).
>
>
> When you talk to logicians about quantifiers, the first thing they think
> of is so-called "first-order" quantification. That is, given the above
> expression, they think that the thing being quantified over is a collection
> of "individuals" who live outside of logic itself[1]. For example, we could
> be quantifying over the natural numbers, or over the kinds of animals in
> the world, or any other extra-logical group of entities.
>
> In Haskell, when we see the above expression we think that the thing being
> quantified over is some collection of types[2]. But, that means when we
> think of P as a function it's taking types and returning types! So the
> thing you're quantifying over and the thing you're constructing are from
> the same domain[3]! This gets logicians flustered and so they call it
> "second-order" (or more generally, "higher-order") quantification. If you
> assert the primacy of first-order logic, it makes sense right? In the
> first-order case we're quantifying over individuals; in the second-order
> case we're quantifying over collections of individuals; so third-order
> would be quantifying over collections of collections of individuals; and on
> up to higher orders.
>
>
> Personally, I find the names "first-order" and "second-order" rather
> dubious--- though the distinction is a critical one to make. Part of the
> reason for its dubiousness can be seen when you look at PTSes which make
> explicit that (1), (2), and (3) above can each be the same or different in
> all combinations. First-order quantification is the sort of thing you get
> from Pi/Sigma types in dependently typed languages like LF; second-order
> quantification is the sort of thing you get from the forall/exists
> quantifiers in polymorphic languages like System F. But the Barendregt cube
> makes it clear that these are *orthogonal* features. Neither one of them
> comes "first" or "second"; they just do very different things. Logicians
> thought first of first-order quantification, so they consider that
> primitive and worry about the complications of dealing with
> second-/higher-order quantification. Until recently type theory was focused
> on polymorphism of various sorts, so that's considered primitive or at
> least easier, whereas dependent types are exotic and worrisome/hard.
>
>
> [1] This is also the root of the distinction between "functions",
> "predicates", and "logical connectives" in traditional logic. Functions map
> individuals to individuals; predicates map individuals to
> propositions/truth-values; and connectives map propositions/TVs to
> propositions/TVs. Though, traditionally, the set of connectives is taken to
> be small and fixed whereas functions and predicates are left to be defined
> by a "signature".
>
> [2] Namely monotypes. If we allowed quantified variables to be
> instantiated with polymorphic types, then we'd get "impredicative"
> quantification. Impredicativity can be both good and bad, depending on what
> you're up to.
>
> [3] Well, they're only the same domain for impredicative quantification.
> Otherwise the collection of types you're constructing is "bigger" than the
> collection you're quantifying over.
>
>
> --
> Live well,
> ~wren
>
> ______________________________**_________________
> 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>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120820/596fc0b2/attachment.htm>