[Haskell-cafe] monads with take-out options

[Greg Meredith]

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. 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.

Best wishes,

--greg

* 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 at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081124/42d0a8ad/attachment.htm