- From: <bugzilla@wiggum.w3.org>
- Date: Tue, 06 Jun 2006 00:12:44 +0000
- To: public-qt-comments@w3.org
- CC:
http://www.w3.org/Bugs/Public/show_bug.cgi?id=3273
------- Comment #2 from jmdyck@ibiblio.org 2006-06-06 00:12 -------
I think you misunderstood me somewhat. Please note that I'm talking about
"Values" (i.e., syntactic objects that can be derived from the symbol 'Value')
as distinct from "values" (i.e., members of an abstract value space).
(Similarly for Type vs type.) I agree with what you say about values & the
empty sequence, or types & the empty type, but what concerns me is that the
formal machinery that operates on Values and Types doesn't reflect what we know
to be true of values and types.
To repeat, the inference rules allow me to conclude:
dynEnv |- 1, () => 1 of type xs:integer, ()
but I can find no way to conclude:
dynEnv |- 1, () => 1 of type xs:integer
Similarly, I can conclude:
statEnv |- 1, () : xs:integer, empty
but not:
statEnv |- 1, () : xs:integer
In each case, I think the latter conclusion is necessary to satisfy premises
elsewhere, but it's unreachable.
Perhaps we need rules such as
dynEnv |- Expr => Value, ()
-----------------------------
dynEnv |- Expr => Value
and
statEnv |- Expr : Type, empty
------------------------------
statEnv |- Expr : Type
Received on Tuesday, 6 June 2006 00:12:51 UTC