[Haskell-cafe] monads with take-out options

[Jonathan Cast]

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