[Prev][Next][Index][Thread]
[bard@theory.LCS.MIT.EDU: Pavel's address]
You wanted info on Pavel Curtis' talk on strong types for SCHEME here
yesterday.
His talk was interesting in that it clarified the special features of
SCHEME's flavor of tagged types with dynamic branching on the type (tag) of a
value, the interaction of side-effects with polymorphic program typing, and
the possible value of extending ML-style typing with implicit
subtype coercions.
But his actual type system and type checker were seemed ad hoc to me, and
were bith pragmatically limited, and theoretically weak. For example, his
type reconstruction algorithm did not find all the types derivable in his
type derivation logic, and he did not have a decision procedure for
subtypings among the types he could reconstruct--so in fact the programmer
does not get support in fuguring out whether the type the system reconstructs
for his program is consistent with the one he may have intended. The only
theoretcial result claimed was operational soundness: if a type is derivable
for a term, then the term executes without runtime type-errors.
Curtis said he based his approach to the standard weakness of the ML type
system wrt side-effects on Tofte's thesis (which I haven't read), but the fix
appeared to be an unreasonably rigid limitation on the typability of mutable
polymorphic objects. (The best hope to have a comfortable typeing setup in
this case seems to be to build flow-analysis into the type system as in
Gifford's FX language--but FX is explicitly typed, and I'm not aware of much
progress on type reconstrcution algorithms for FX types that are omitted.)
Curtis noted that neither Tofte nor he does flow analysis in the type system,
and didn't offer any special insights into how to overcome the limits of his
current approach--at least while I was around, but I had to leave midway
through the question period and didn't have time for a followup conversation
later.
You can contadt him diretly for his slides and more info at:
pavel.pa@xerox.com
Regards, A.