Timeline for Domain Theory and Polymorphism
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 10, 2017 at 13:08 | vote | accept | Jake | ||
| Jun 10, 2017 at 12:54 | answer | added | Andrej Bauer | timeline score: 6 | |
| Jun 10, 2017 at 12:30 | comment | added | Andrej Bauer | @cody: tsk, tsk. | |
| Jun 9, 2017 at 18:53 | answer | added | Nathan BeDell | timeline score: 0 | |
| Nov 24, 2016 at 7:07 | comment | added | Jake | Eh right. I forgot System-F was total. I think I'm more concerned with System-F in the presence of fixed points. Or PCF with parametric polymorphism. I want to know how polymorphism effects computation (or learn a bit about it at least). I haven't nearly finished grokking Paul Taylor's notes yet so I don't know if I'll find that kind of answer there or not. I kind of have a puzzle in mind I'd like to answer. In a lazy language given some function F how many unique inhabitants of F a -> F a are there? Domain theory gives the best answer to the non polymorphic version of this question. | |
| Nov 22, 2016 at 23:50 | history | tweeted | twitter.com/StackCompSci/status/801211347073695744 | ||
| Nov 22, 2016 at 21:12 | comment | added | cody | I see, thanks for your clarifications. The most "domain-theory-like" treatment of system F I know of is Girard's "Coherent Spaces" the treatment of which is outlined here by Paul Taylor. I don't know if this is a "nice theory" as per your request, but to be honest, I don't really see domain theory as being that nice in general for semantics of total languages... | |
| Nov 22, 2016 at 21:07 | comment | added | Jake | I should also add that I understood domain theory to still be set theoretic in principal. That is functions are still set theoretic functions it's just that you only become concerned with the continuous functions when interpreting functions in a calculus. Hence my understandings seem to rule out System-F fitting into a domain theoretic model. Perhaps it is one of my understandings that is wrong here. | |
| Nov 22, 2016 at 20:55 | comment | added | Jake | I understood that there are no models of system F in which functions are interpreted as any kind of function in set theory. I understood there to be no "naive" set theoretic models of the typed lambda calculus but that set theoretic models exist as long as the functions are continuous functions. Then much like the continuous real functions have the same cardinality as the reals so too can the scott-continuous functions have the same size as their (co)domain. I understood this to be how the size problem was resolved. I understood such a solution to not exist for system-F however. | |
| Nov 22, 2016 at 20:42 | comment | added | cody | I'm confused: there are domain-theoretic models of the untyped $\lambda$-calculus, which intuitively is a typed calculus with a type $\alpha\simeq\alpha\rightarrow\alpha$. This, of course, has no models in sets either. Why would you expect there to be no domain models of system F? Have you tried searching online? | |
| Nov 22, 2016 at 3:41 | history | asked | Jake | CC BY-SA 3.0 |