At 10:34 +0100 2003/04/22, Simon Marlow wrote:

If the quantifier is outside the constructor, then it scopes over all the fields of the constructor. So, if you write

data T = forall a . C t1 .. tn

what should this mean (assuming you want a non-existential interpretation)?

I think you have problem here because, you apply the quantifier to something which is not a predicate. This practise makes it hard to figure out what the semantics should be. For example, in the original example:

At 09:02 +0100 2003/04/17, Simon Peyton-Jones wrote: data T = forall a. Foo a (a -> Int) if T is a well formed formula in a quantification theory there is an associated predicate P(a) = Foo a (a -> Int) from which one gets T := all a: P(a).

One of the quantification axioms that I listed said: axiom Q4. t free for x in A |- (all x: A) => [x\t]A. It means that from T, one can plug in a value t (a term) [a\t]T = [a\t]P(a) to get Foo t (t -> Int) Is that not what you want? However, in math, quantifiers are only applied to predicates, not sets. For sets, one uses operations such as union, intersection and complement. It seems me that data types correspond to sets, not predicates. Thus, one should not use quantifiers "all" and "exist" at all on them, but something corresponding to sets instead. In naive set theory, one identifies the set S := { x | P(x) } with the predicate P(x). If one should get the set S from the closed formula T above, one first applies the axiom Q4 to get P(x) := [a\x]T, and then one can get S from P(x). In the example above, the set becomes S = { a | Foo a (a -> Int) } To begin with, this does not make logically sense, as Foo a (a -> Int) is supposed to return not logical values as is required by a predicate, but data of type T. It seems me that one should instead have someting like data T = union a. Foo a (a -> Int) or data T = disjointUnion a. Foo a (a -> Int) Then, when one instantiates, one will create another addition to the data type, which is how I think is what you really want. Right? Hans Aberg