i am interested in a first-principles notion of data. Neither lambda nor ð-calculus come with a criterion for determining which terms represent data and which programs. You can shoe-horn in such notions -- and it is clear that practical programming relies on such a separation -- 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...) One step towards a first-principles characterization of data (as separate from program) is a first-principles characterization of containers.

Along these lines Barry Jay's pattern-matching calculus is an intriguing step towards such a characterization. This also links up with Foldable and Traversable.
i also looked at variants of Wischik's fusion calculus in which Abramsky's proof expressions characterize the notion of shippable data. (Part of the intuition here is that shippable data really ought to have a terminating access property for access to some interior region. The linear types for proof expressions guarantee such a property for all well-typed terms.)

There is a real tension between nominal strategies and structural strategies for accessing data. This is very stark when one starts adding notions of data to the ð-calculus -- which is entirely nominal in characterization. Moreover, accessing some piece of data by path is natural, obvious and programmatically extensible. Accessing something by name is fast. These two ideas come together if one's nominal technology (think Gabbay-Pitt's freshness widgetry) comes with a notion of names that have structure.*
Finally, i think the notion of take-out option has something to do with being able to demarcate regions. In this sense i think there is a very deep connection with Oleg's investigations of delimited continuations and -- forgive the leap -- Linda tuple spaces.

As i've tried to indicate, in much the same way that monad is a very, very general abstraction, i believe that there are suitably general abstractions that account for a broad range of phenomena and still usefully separate a notion of data from a notion of program. The category theoretic account of monad plays a very central role in exposing the generality of the abstraction (while Haskell's presentation has played a very central role in understanding the utility of such a general abstractin). A similarly axiomatic account of the separation of program from data could have applicability and utility we haven't even dreamed of yet.

* i simply cannot resist re-counting an insight that i got from Walter Fontana, Harvard Systems Biology, when we worked together. In some sense the dividing line between alchemy and chemistry is the periodic table. Before the development of the periodic table a good deal of human investigation of material properties could be seen as falling under the rubric alchemy. After it, chemistry. If you stare at the periodic table you see that the element names do not matter. They are merely convenient ways of referring to the positional information of the table. From a position in the table you can account for and predict all kind of properties of elements (notice that all the noble gases line up on the right!). Positions in the table -- kinds of element -- can be seen as 'names with structure', the structure of which determines the properties of instances of said kind. i believe that a first-principles account of the separation of program and data could have as big an impact on our understanding of the properties of computation as the development of the periodic table had on our understanding of material properties.

On Mon, Nov 24, 2008 at 2:30 PM, Jonathan Cast <jonathanccast@fastmail.fm> wrote:

On Mon, 2008-11-24 at 14:06 -0800, Greg Meredith wrote:
> Haskellians,

> Some monads come with take-out options, e.g.
> * List
> * Set
> In the sense that if unit : A -> List A is given by unit a = [a], then
> taking the head of a list can be used to retrieve values from inside
> the monad.

> Some monads do not come with take-out options, IO being a notorious
> example.

> Some monads, like Maybe, sit on the fence about take-out. They'll
> provide it when it's available.

It might be pointed out that List and Set are also in this region. In
fact, Maybe is better, in this regard, since you know, if fromJust
succeeds, that it will only have once value to return. head might find
one value to return, no values, or even multiple values.

A better example of a monad that always has a left inverse to return is
((,) w), where w is a monoid. In this case,

snd . return = id :: a -> a

as desired (we always have the left inverses

join . return = id :: m a -> m a

where join a = a >>= id).

> Now, are there references for a theory of monads and take-out options?
> For example, it seems that all sensible notions of containers have
> take-out.

Sounds reasonable. Foldable gives you something:

foldr const undefined

will pull out the last value visited by foldr, and agrees with head at [].

> Can we make the leap and define a container as a monad with a notion
> of take-out?

If you want. I'd rather define a container to be Traversable; it
doesn't exclude anything interesting (that I'm aware of), and is mostly
more powerful.

> Has this been done?

Are you familiar at all with Foldable
(http://haskell.org/ghc/docs/latest/html/libraries/base/Data-Foldable.html#t%3AFoldable) and Traversable (http://haskell.org/ghc/docs/latest/html/libraries/base/Data-Traversable.html#t%3ATraversable)

jcc

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105

+1 206.650.3740

http://biosimilarity.blogspot.com