Re: Generative record types

[Guillermo J. Rozas <gjr@martigny.ai.mit.edu>]

|   Date: Tue, 30 Apr 1996 10:14:14 +0000
|   From: William D Clinger <will@ccs.neu.edu>
||
|   > B. Type inference.  Why not add a type facility to the record
|   >    proposal?
|   > 
|   >    For example, you could qualify each field with a predicate that the
|   >    corresponding components must satisfy.  The mutators generated
|   >    could then check and guarantee no inconsistencies.
|
|   I don't think this is likely to work.  How would you construct
|   a predicate for the following type?
|
|     forall (a, b)  (a * (a -> b)) -> b
|
|   This is hardly an esoteric example, since it is the type that
|   would be inferred for
|
|     (lambda (x f) (f x))
|
|   Will

This is a great example of the stuff you cannot do when procedures are
completely opaque.  Isn't it a shame that we are so adamant on that one?

If you have a syntactic type system, the properties that you are
trying to deduce could just as well be proven at run time given simple
procedure inspection facilities, since the static version could not
have used more than the form.  If you have a statically decidable
algorithm, it can be applied locally at run time and still be
decidable.

In other words, I claim (no proof) that any statically-decidable type
system can be modified into a similarly-hampered (avoids
undecidability) dynamic type system given suitable inspection
facilities for procedures.