[bitc-dev] Type quantification and predication
Jonathan S. Shapiro
shap at eros-os.org
Wed Jul 20 22:17:33 EDT 2005
I want to introduce a syntax for purposes of discussion. I'm not
convinced that we will use this syntax in BitC, though it isn't bad. At
this point, I simply want something we can all look at and understand
for purposes of discussion.
The syntax is
(forall ('a0 ... 'aN) T)
where T is some type parameterized over 'a0 .. 'aN
For example, when we have written
(defunion (list 'a):ref nil (cons 'a (list 'a)))
This has always been implicitly understood to introduce the type
(forall ('a) (list 'a))
It is sometimes useful to be able to restrict a polymorphic type. For
example, when we write
(define (cdr x : (list 'a)) ...)
we really mean that "x" takes some anonymously named type 'b that is
restricted to types that can unify with (list 'a). That is, a
parameterized type can be viewed as an infinite closed type class.
There is an obvious extension to the FORALL syntax to deal with this. In
a lambda parameter, when we see x:y, we know that x is an object and y
is a type. In a FORALL, we know that x is a type and we haven't
introduced any use for y. I am proposing that y should be a "set of
types". Thus, the fully elaborated type for CDR would be:
cdr : (forall ('b:(list 'a)) (fn 'b 'b))
If we introduce type classes, we will sometimes want multiple
predicates. For example, we may want to describe types that satisfy
"orderable" and also "lists of some sort". Imagine that there is a type
class Ord that describes the set of orderable types.
For the moment, I propose that we might write this as:
(forall ('a:Ord 'a:(list 'b)) 'a)
Notice that the "parameter" 'a appears twice in the forall. This is okay
because forall is never explicitly instantiated by a programmer and so
we don't have to care syntactically how many times the 'a appears.
Actually, note that this isn't precisely written. It should probably be:
(forall ('a:Ord 'a:(list 'b)) 'a))
which can be simplified (perhaps surprisingly) to:
(forall ('b 'a:Ord 'a:(list 'b)) 'a)
Speaking only for myself, I like this syntax, and I think we should
introduce something like it for scoping type variables. The problem that
it *doesn't* solve well is expressing interdependencies among the types.
Until I understand what needs to be said, I'm not going to try to come
up with a syntax for that.
In any case, if you see this notation running around in the email over
the next few days, you now know what it means.
More information about the bitc-dev