On Mon, 2008-11-24 at 15:06 -0800, Greg Meredith wrote:
Jonathan,
Nice! Thanks. In addition to implementations, do we have more mathematical accounts? Let me expose more of my motives. * i am interested in a first-principles notion of data.
Hunh. I have to say I'm not. The difference between Bool -> alpha and (alpha, alpha) is not one I've ever felt a need to elaborate. And I'm not sure you *could* elaborate it, within a mathematical context --- which to me means you only work up to isomorphism anyway.
Neither lambda nor π-calculus come with a criterion for determining which terms represent data and which programs.
As you know, lambda-calculus was originally designed to provide a foundation for mathematics in which every mathematical object --- sets, numbers, function, etc. --- would be a function (a lambda-term) under the hood. It was designed to abstract away the distinction between values and functions, not really to express it.
You can shoe-horn in such notions -- and it is clear that practical programming relies on such a separation
What? `Practical programming' in my experience relies on the readiness to see functions as first-class values (as near to data as possible). Implementations want to distinguish them, in various ways --- but then once you draw that distinction, programmers want to use data structures like tries, to get your `data structure' implementation for the program design's `function' types (or some of them...) As near as I can tell, the distinction between data and code is fundamentally one of performance, which makes it quite implementation-dependent. And, for me, boring.
-- but along come nice abstractions like generic programming and the boundary starts moving again. (Note, also that one of the reasons i mention π-calculus is because when you start shipping data between processes you'd like to know that this term really is data and not some nasty little program...)
It's not nice to call my children^Wprograms nasty :) I think, though, that the real problem is to distinguish values with finite canonical forms (which can be communicated to another process in finite time) from values with infinite canonical forms (which cannot). The problem then is defining what a `canonical form' is. But characterizing the problem in terms of data vs. code isn't going to help: \ b -> if b then 0 else 1 is a perfectly good finite canonical form of type Bool -> Int, while repeat 0 is a perfectly good term of type [Int] (a data type!) with no finite canonical form (not even a finite normal form). I'm sure this fails to engage your point, but perhaps it might clarify some points you hadn't considered. jcc