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
