On Dec 7, 2008, at 8:01 PM, Jonathan S. Shapiro wrote:
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 polymorphismAs he so often does, Paul has asked just the right question, and I want to attempt to answer it.
Jonathan is being far too kind--had I given the issue another moment's thought, I'd have arrived at the conclusion that he articulated, on the basis of my experiments using Coq. There's also support for the conclusion on LtU, in a slightly different context, rooted at <http://lambda-the-ultimate.org/node/3132#comment-45686 >. Interestingly, my launching-off point for this part of the discussion revolves around my efforts to understand "parametricity as static security tool" in a sense that Tim Sweeney had hinted at in private correspondence, has come to "having to support lambda behavior in types can cause some real head-scratching when that type propagates outward in scope," and now has led me to think that this is neither more nor less than the object-capability security community's fear of leaking authority expressed in dependent types.
I'll be spending a lot of time groking Washburn and Weirich's work, I think. Matt and Tim's comments in the thread that I link to are exactly about "type-directed programming," and Washburn and Weirich's work is exactly about generalizing parametricity with information flow so that we can have type-directed programming without violating parametricity. Highly recommended.
Best regards, Paul
PGP.sig
Description: This is a digitally signed message part
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
