Hmm. This may be turning into a DISCUSS. :-)
Let me define what I mean by "quasi-terms" a bit more rigorously. In
logic, a term is something that can be substituted without changing the
meaning of the logic statement. I'm after something very close to that
for BitC.
Originally, I started with (typed) literals:
1 : int32
2.4
#\c
"abc"
As I got to thinking about the whole mess with typeclass instantiations,
I suddenly realized that procedure labels are also literals (in fact,
this is what justifies the linker in substituting a function address for
its unresolved label).
As I sat down to write my note about quantification over literals, I
looked at the place where I had written:
id : T
and wondered why I was putting arbitrary restrictions on T? What kinds
of things "T" are okay here and what kinds are not?
So immediately I thought "type constructions are okay". But of course,
that isn't necessarily true. Type constructors are certainly okay if all
of the arguments to those constructors are terms, but what about if type
variables get resolved to mutable types?
Well, hang on, because procedure *objects* can clearly be substituted
without a problem, even if the closure of that procedure is mutable.
This is true because the procedure object itself is shallow-immutable
and its location is link-time resolvable (which is what justifies the
linker in substituting the address of the procedure object for its
unresolved label).
So this brings me to quasi-terms. The two requirements of a quasi-term
are:
1. It's value must be shallow-immutable. This is necessary to justify
substitution.
2. It's value must be computable at compile time.
Here is a recursive partial definition of quasi-terms:
1. Literals are quasi-terms.
2. Lambda forms are quasi-terms.
3. If C is a type constructor producing a reference type, an
instantiation (C e1 ... en) is a quasi-term exactly if
all of the argument expressions e1 ... en are quasi-terms.
Note this does not preclude the possibility that the *types* of
those expressions might unify with (mutable 'a).
4. If C is a type constructor producing a value type, an
instantiation (C e1 ... en) is a quasi-term exactly if
all of the argument expressions e1 ... en are quasi-terms
and the value resulting from the construction is shallow-immutable.
We can certainly extend this over a variety of built-in expressions,
over LET, and so forth, but I don't propose to do any of that just yet.
Already we have a very powerful constructive mechanism. Rule 4, for
example, can be viewed as justifying procedure objects, including those
with mutable closures, though I do not propose to adopt that view at the
moment.
So when we write:
(forall (id:T) ... body using "id" as a type ...)
we can specify any T that is a quasi-term. In fact, we could introduce a
notion of a type class defining quasi-terms, and accept:
(forall (id:'a (QuasiTerm 'a)) ...)
Just to be clear, I do NOT propose to go this far, precisely because I
haven't got a clear enough definition of QuasiTerm expressions to carry
it through yet. I'm simply trying to make the idea clear here by
exhaustive obfuscation. :-)
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
