Paul Snively just made a wonderful comment in private mail. I had said
something to the effect that dependent types tend to "escape" in
pragmatically unpleasant ways. Paul responded:
your point about dependent types escaping a confined scope doesn't resonate
with me; I'm having difficulty seeing how this could be any more of an issue
for types indexed by terms than for, e.g. types indexed by other types, i.e.
good ol' parametric polymorphism
As he so often does, Paul has asked just the right question, and I want to
attempt to answer it.
As a first step, let me make an observation about polymorphism. There are
cases of polymorphism that BitC will not accept. Ultimately, all of the
parametricity of a procedure has to be resolvable at application time. Once
you have fully resolved the types of the arguments and return value, that's
all the resolution you are going to get. It turns out that there are some
cases where that isn't good enough. As an example, consider:
(define (strange-add-one x)
(let ((tmp 1))
(+ tmp 3)
(+ x 1)))
;; Following type is WRONG
strange-add-one: (forall ((Arith 'a)) (fn 'a ->'a))
The problem with this is that we cannot assign a type to the local variable
"tmp", because it is not connected by any operation to any argument or
return value. That is, the correct typing for this procedure would be:
strange-add-one: (forall ((Arith 'a) (Arith 'b))
(fn 'a ->'a))
where 'b is the type assigned to tmp. Note that the constraint cannot be
resolved by application, because 'b does not appear in the function
signature. BitC will reject this procedure as underspecified.
What I'm trying to say here is that there are constraints imposed by the
type system on the functors that can legally arise in a BitC program. The
case above is one example. Another is that there is nothing equivalent to a
LAMBDA construct in the type system. This turns out to be important for
making inference work, and also important for explaining the answer to
Paul's question.
In a sense, Paul is correct; dependent types -- or more precisely, the *
constraints* associated with dependent types -- do not escape in a way that
is different from parametric types. The difference is that because dependent
types contain values, the dependent type system has to admit the behavior of
LAMBDA. To see why this is a problem, let's look at how to express the
dependencies in:
(/ (f x) (g y))
in a dependently typed framework. First, we know that divide is not defined
when the divisor is zero, so the type of divide (pardon the syntax) will be
something like:
/: (forall ((Arith 'a) (Arith 'b) ('b != 0)) (fn 'a 'b -> 'b))
So far so good. So now the problem is that we need to confirm that the call
to g never returns zero. Sometimes this will be easy, but in the general
case this will devolve into a set of constraints on the argument y. Those
constraints can be ARBITRARILY complex.
Assume for a moment that we can see the code for g. In this case, we know
the desired outcome, and we need to attempt some form of backward chaining
inference to derive constraints on y that ensure that (g y) does not return
zero. I'm not aware of any sound and complete inference strategy for this.
In fact, even if we had the appropriate input constraints on g
*declared*for us, it's a theorem proving problem to show at compile
time that those
preconditions ensure the proper postcondition.
But assuming that we can derive backwards to arrive at the preconditions,
note that the constraints on the preconditions are unlikely to have any
obvious relationship to our goal, which was to ensure that (g y) had a
non-zero result. From an expressiveness perspective, what we need to do here
is express conditional constraints, of the form "when you need the result to
be non-zero, then the following preconditions must hold".
Finally, note that divide is not our only use case, and the author of g
cannot possibly anticipate all of the contexts in which g may get called.
Each of those contexts may demand its own backward inference exercise, and
each might induce a requirement for different preconditions on g. This means
that the whole process of generating those preconditions is immodular. In
one program certain preconditions may be necessary. In another (say: where
divide never appears) they may be completely unnecessary.
So Paul is right. It's not the propagation of dependent constraints per se
that worries me. It's the fact that as the dependencies propagate they morph
in strange and context-dependent ways that (a) are very hard for a human to
associate with an end result, and (b) appear to be intrinsically immodular.
For this reason, I tend to believe that dependent typing should be done on a
whole-program basis. It''s clearly very useful, but not something that I
think belongs in the compiler-implemented type system yet.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
