Sunday, February 16, 2014

Subtyping, oh subtyping, where art thou?...

I don't know how come I ended up skimming the following report Extending ML F with Higher-Order Types, as System F is nowadays very far from my worries.

 But I did. and this reminded me that I really should try to get my mind clear about what the issues are and how much progress has been made  in the subject of subtyping in System F since I did some very preliminary work on it in the context of the programming language Ponder, when working as an RA in Cambridge.

The report (Subtyping in Ponder) is available from the Computer Lab in Cambridge.

This reminds me, again, of how much I owe Michael Gordon.  And it feels good to be grateful. Btw I love Mike's favicon, will try to copy it sometime...

Posted by at

2 comments:

  1. Harley D. Eades IIIMarch 5, 2014 at 9:52 AM

    Have you read: http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-80.pdf

    This is a rather old paper, but an interesting one. Somewhere near the end he shows that when you add subtyping to system F you gain the correspondence between Church-encoded pairs and categorical products. In plain old system F this is not the case. I found that particularly interesting.

    Harley

    ReplyDelete
    Replies
    1. ValeriaMarch 5, 2014 at 10:08 PM

      hi Harley, I'm not sure if I have read or not the Cardelli paper you've mentioned. I have a vague recollection of being disappointed with it, as the problem I wanted to see solved was type inferencing for SystemF plus subtyping, but I should check it...

      Delete

Subscribe to: Post Comments (Atom)