Timeline for Is functional programming a branch of mathematics?
Current License: CC BY-SA 2.5
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 19, 2010 at 23:32 | comment | added | Neel Krishnaswami | Er, sure it does. You just take the universal domain to be a coalesced sum including an error case, and blatantly ill-typed stuff denotes the error value. The error is conventionally called Wrong, which is where the "wrong" in the phrase "well-typed programs don't go wrong" comes from. | |
| Jan 19, 2010 at 20:16 | comment | added | Adam | Scott's model of PCF terms as "simply typed lambda expressions of infinite type" was a work of truly incredible vision, but its result was only to add non-normalizing terms to the simply typed lambda calculus, and the result was still a cartesian closed category. The $D_\infty$ construction does not allow for the sort of blatantly ill-typed terms like (4+"Fred") that are allowed in LISP, Python, Ruby -- nor should it!. | |
| Jan 19, 2010 at 9:37 | comment | added | Neel Krishnaswami | The theory of the untyped lambda calculus is much, much richer than the simply-typed case, and is actually why Scott invented domain theory. Giving a model for it requires finding a category where the isomorphism $D == D -> D$ holds non-trivially, which is a pretty bold thing to imagine. (In fact, Scott wrote a paper arguing against the untyped lambda calculus, on the grounds that there was no way anyone could come up with such a model, shortly before he came up with one!) | |
| Jan 18, 2010 at 23:19 | history | answered | Adam | CC BY-SA 2.5 |