[bitc-dev] BitC/Dependent Types

[Paul Snively]

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 polymorphism
>
> As 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.coyotos.org/pipermail/bitc-dev/attachments/20081220/10f2bd33/attachment.html 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 194 bytes
Desc: This is a digitally signed message part
Url : http://www.coyotos.org/pipermail/bitc-dev/attachments/20081220/10f2bd33/attachment.bin