tag:blogger.com,1999:blog-4249190426304084757.post6862049350633054630..comments2024-01-22T00:34:59.225-08:00Comments on Logic ForAll: Subtyping, oh subtyping, where art thou?...Valeriahttp://www.blogger.com/profile/01336528462208811726noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-4249190426304084757.post-44727816883374119152014-03-05T22:08:17.784-08:002014-03-05T22:08:17.784-08:00hi Harley, I'm not sure if I have read or not ...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...Valeriahttps://www.blogger.com/profile/01336528462208811726noreply@blogger.comtag:blogger.com,1999:blog-4249190426304084757.post-9406712115279931992014-03-05T09:52:33.908-08:002014-03-05T09:52:33.908-08:00Have you read: http://www.hpl.hp.com/techreports/...Have you read: http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-80.pdf<br /><br />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.<br /><br />HarleyHarley D. Eades IIIhttps://www.blogger.com/profile/03155494277810217708noreply@blogger.com