[Axiom-math] Re: [fricas-devel] Re: [open-axiom-devel] [fricas-devel] Re: [fricas-devel] Re: iterators and cartesian product.

[Bill Page]

On 10/31/07, Gabriel Dos Reis wrote:
>
> On Wed, 31 Oct 2007, Bill Page wrote:
>
> | On 10/31/07, Gabriel Dos Reis wrote:
> | >
> | > On Wed, 31 Oct 2007, Bill Page wrote:
> | > ...
> | > | It might even be interesting to consider implementing
> | > | something akin to monads in Aldor/SPAD,
> | >
> | > There already existe a domain called Monad in the Axiom family --
> | > it is a well mathematically defined notion.
> | >
> |
> | Perhaps I am being dense but I do not see what this has to do with the
> | concept of Monad in Haskell.
>
> They are the same categorial notion.

That is not clear to me.

> What you have in Haskell is a computer scientist application of the
> categorial notion of `monad'.

Agreed.

> Haskell's take derive from Moggi's work on applying monads to defined
> program semantics.  See his seminal work.

Yes.

> And it is also true that you don't need to understand category
> theory before using `monad's in Haskell.

I don't think that is extraordinary. One doesn't need to know much
about formal semantics of programming languages in general before
starting to program. And more relevant to this thread: I don't think
you need to know anything about category before using Record or Cross
in Axiom/Aldor either, but I would still insist that to describe it
formally as a limit in category theory adds something to the issue of
language and library design.

> Which makes some haskellers say that they did a really bad job
> at picking the name.
>

Well, the language is called *Haskell* afterall. Do those haskellers
who think monad is a bad name even remember who Haskell Curry was!?
;-)  [Rhetorical, don't answer that ...]

> [...]
>
> | > I do not however see myself implement the Haskell solution
> | > | for Axiom. I would prefer a more powerful effect system for
> | > | OpenAxiom.
> | >
> |
> | Could you describe what you mean by "effect system"?
>
>   http://www.irisa.fr/prive/talpin/papers/jfp92.pdf

Ok, thanks. This quote from the article:

"Similar to types, effects describe how expressions affect the store
in a functional language extended with imperative constructs. Types
and effects can be statically computed by algebraic reconstruction
[Jouvelot]."

makes it more clear to me.

>
> | > | but I think you will agree that fundamentally these
> | > | languages were not designed to be purely functional.
> | >
> | > I do not see `purely functional' as as necessity.
> | >
> |
> | In that case what is wrong with effects as implemented in SPAD's
> | imperative-style programming right now?
>
> I did not make a statement to that effect, so I do not exactly what
> you mean. Could you clarify?
>

Your reference above makes it more clear to me what you might have in
mind. Perhaps you are thinking that it might be possible to give a
formal description of effects related to the imperative constructs in
SPAD as it exists now (or perhaps some subset of the imperative part
of the language). I am sceptical but I really don't know enough to
comment further.

> | I am sorry. I don't mean to sound rude, but I just don't understand
> | where your comments lead. Could you say something more about
> | what you are considering for implemention in OpenAxiom?
>
> Among other things, a type and effect system so that I can know which
> domain are purely functional -- therefore the caching implementation
> technique is sound for them -- and which have effects, therefore
> should not be cached.

I think that is a very worthwhile goal. Thanks for explaining.

Regards,
Bill Page.