Haskell, Functor, Monad, Maybe

[oldk1331]

There's a long thread in 2011 talking about monad,
but that discussion is not very clear and not what
I am going to talk about.
https://groups.google.com/d/msg/fricas-devel/UCFkQGgOOf0/oj9-FygocVgJ

The motivation get me into this topic is simple:
In OpenAxiom, I see there's a Maybe domain instead
of Union(T, "failed"). I want to have Maybe in FriCAS.

However, unlike Haskell, Maybe in OpenAxiom is not
a Monad.

So I did some research about how to implement Monad
in FriCAS:

## Functor
First, a simpler concept, Functor. OpenAxiom has this
Category defined, basicly, exports 'map(S->S, %)->%'.

I think FriCAS should also use this Categoty, ")dis op map" gives
81 exposed and 15 unexposed signature, that's too messy.

This Functor category is easy to understand, but it can't
handle more than 2 types:
map : (A->B, Functor A) : Functor B
It is impossible to export this signature in a category, and I use
a "hacky" method to implement it, see FunctorPackage bellow.

## Maybe
Maybe is an abstraction over Union(T, "failed"), but it also has
some property: Maybe is a Functor and a Monad.

See the implementation of "map" in Maybe and FunctorPackage.

## Monad
Functor is a category exports map : (S -> S, %) -> %,
Monad is a category exports bind : (S -> %, %) -> %,
or its infix form (% >>= (S -> %)) : %

For more than 2 types,
bind : (A -> Monad B, Monad A) -> Monad B
>>= : (Monad A, A -> Monad B) -> Monad B

It seems that FriCAS doesn't support infix operator with
3 letters, I use "_>_>" in the code bellow.

## Usage
This is just a simple example:

myinv(x:FRAC INT):Maybe FRAC INT == if x = 0 then nothing()$Maybe(FRAC
INT) else just(1/x)

(3) -> myinv 4

1
(3) ─
4
Type: Maybe(Fraction(Integer))
(4) -> myinv 0

(4) ()
Type: Maybe(Fraction(Integer))
(5) -> myinv 4 >> myinv

(5) 4
Type: Maybe(Fraction(Integer))
(6) -> myinv 0 >> myinv

(6) ()
Type: Maybe(Fraction(Integer))

Compared with:
(7) -> inv 4

1
(7) ─
4
Type: Fraction(Integer)
(8) -> inv inv 4

(8) 4
Type: Fraction(Integer)
(9) -> inv inv 0

>> Error detected within library code:
not invertible

##

This is just a "proof of concept" version, you can see the
Haskell version of Maybe from here:
https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Maybe.html

So, do you support implement such Functor/Monad/Maybe
in FriCAS?

======

)abbrev category FUNCTOR Functor
Functor(S : Type) : Category == Type with
map: (S -> S, %) -> %

)abbrev category MONAD Monad
Monad(S : Type) : Category == Type with
_>_> : (%, S -> %) -> %

)abbrev domain MAYBE Maybe
Maybe(T : Type) : Public == Private where
Public == Join(RetractableTo T, Functor T, Monad T) with
just : T -> %
++ \spad{just x} injects the value `x' into %.
fromJust : % -> T
nothing? : % -> Boolean
nothing : () -> %
++ \spad{nothing} represents failure or absence of value.
if T has CoercibleTo OutputForm then CoercibleTo OutputForm
Private == add
Rep := Union(T, "failed")
just x == x
nothing() == "failed"
nothing? x == x case "failed"
fromJust x ==
nothing? x => error "nothing in fromJust"
x@T
map(f, x) ==
nothing? x => nothing()
just f fromJust x
_>_>(x, f) ==
nothing? x => nothing()
f fromJust x
if T has CoercibleTo OutputForm then
coerce(x: %): OutputForm ==
nothing? x => paren(empty()$OutputForm)$OutputForm
(x@T)::OutputForm

)abbrev package FUNCTOR2 FunctorPackage
FunctorPackage(A : Type, B : Type, FA : Functor A, FB : Functor B) :
Exports == Implementation where
Exports == with
map : (A -> B, FA) -> FB
Implementation == add
if FA is Maybe A and FB is Maybe B then
map(f, fa) ==
if nothing?(fa)$Maybe(A) then nothing()$Maybe(B)
just f fromJust fa

)abbrev package MONADPKG MonadPackage
MonadPackage(A : Type, B : Type, MA : Monad A, MB : Monad B) :
Exports == Implementation where
Exports == with
bind : (A -> MB, MA) -> MB
_>_> : (MA, A -> MB) -> MB
Implementation == add
if MA is Maybe A and MB is Maybe B then
bind(f, fa) ==
if nothing?(fa)$Maybe(A) then nothing()$Maybe(B)
f fromJust fa
_>_>(fa, f) ==
bind(f, fa)

[Waldek Hebisch]

Well, FriCAS lexer has fixed set non-alphabetic tokens and '>>='
is not one but two tokens ('>>' followed by '=').

> ## Usage
> This is just a simple example:
>
> myinv(x:FRAC INT):Maybe FRAC INT == if x = 0 then nothing()$Maybe(FRAC
> INT) else just(1/x)
>
> (3) -> myinv 4
>
> 1

> (3) â

> 4
> Type: Maybe(Fraction(Integer))
> (4) -> myinv 0
>
> (4) ()
> Type: Maybe(Fraction(Integer))
> (5) -> myinv 4 >> myinv
>
> (5) 4
> Type: Maybe(Fraction(Integer))
> (6) -> myinv 0 >> myinv
>
> (6) ()
> Type: Maybe(Fraction(Integer))
>
> Compared with:
> (7) -> inv 4
>
> 1

> (7) â

> 4
> Type: Fraction(Integer)
> (8) -> inv inv 4
>
> (8) 4
> Type: Fraction(Integer)
> (9) -> inv inv 0
>
> >> Error detected within library code:
> not invertible
>
> ##
>
> This is just a "proof of concept" version, you can see the
> Haskell version of Maybe from here:
> https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Maybe.html
>
> So, do you support implement such Functor/Monad/Maybe
> in FriCAS?

I do not understand why you want this. One problem is length
of 'Union(Something, "failed")', but we can use macros like:

Maybe(T) ==> Union(T, "failed")

UF(T) ==> Union(T, "failed")

or

UF1 ==> Union(Something, "failed")

You seem to want to use '>>' to convert functions from
T to Union(T, "failed") into functions from
Union(T, "failed") to Union(T, "failed"). I am not sure
if this will work well: currently both Spad compiler and
interpteter have very limited ability to "invent" new
types. Actually Spad compiler need some explicit or
implicit import to use a type. Interpeter has a bunch
of hardcoded rules, go beyond them and it can not
find type. So there is good chance that you will have
to explicitely import your packages/domains for all
involved T-s.

Also, Spad compiler knows about unions, so we can use
code like:

ru := retractIfCan(x)@Union(T, "failed")
ru case "failed" => "failed"
r := ru::T

and Spad compiler knows that coercion in third line is legit,
because we excluded the other possibility in line 2. With
'Maybe' compiler will no longer accept code like above. Of course
you may add explicit functions to test for failure and explicit
function for coercion which calls error if value is not T, but
then you loose static checking: once you add such coercion you
can call it without performing check before.

--
Waldek Hebisch

[oldk1331]

> You seem to want to use '>>' to convert functions from
> T to Union(T, "failed") into functions from
> Union(T, "failed") to Union(T, "failed").

No, it doesn't create new functions, just "combine" them.

Say we want to apply a series of functions, first f, then g:

x:INT, f:INT->INT, g:INT->INT
The result of f(x) can go directly into g: g(f(x))

x:List INT (or Maybe INT), f:INT->INT, g:INT->INT
We can use map: map(g, (map(f, x))

x:Maybe INT, f:INT->Maybe INT, g:INT->Maybe INT
Now we can't use map, or we have to manually check
for failure at every call, or we can use >>:
x >> f >> g

> Actually Spad compiler need some explicit or
> implicit import to use a type. Interpeter has a bunch
> of hardcoded rules, go beyond them and it can not

> fand Spad compiler knows that coercion in third line is legit,
because we excluded the other possibility in line 2.ind type. So

there is good chance that you will have
> to explicitely import your packages/domains for all
> involved T-s.

I just checked, for the same type (A->Maybe A), there's
no problem. But for more than 2 types: (A->Maybe B, B->Maybe C),
you have to explicitly import from MonadPackage in Spad,
and explicitly construct typed anonymous function wrapper
in interpreter.

> and Spad compiler knows that coercion in third line is legit,
> because we excluded the other possibility in line 2.

> .... but then you loose static checking:

This is the advantage of Maybe: in your example, there's
no point doing such things, just return the Maybe type:

ru := retractIfCan(x)@Maybe(T)

The following code that deals with ru should handle Maybe(T).
Say the following lines that handle ru is function "g" (the continuation).

In your example, it is:

ru := retractIfCan(x)@Union(T, "failed")
ru case "failed" => "failed"
r := ru::T

g : T->T2
g(r)

In my example,
ru := retractIfCan(x)@Maybe(T)
g : T->T2
map(g, ru)

If there's still a failure in g:
ru := retractIfCan(x)@Maybe(T)
g : T->Maybe T2
ru >> g

[oldk1331]

Use Functor category to abstract the 'map' function,
to reduce the number of ')display op map', what do
you think?

[Bill Page]

+1

[oldk1331]

Bill, you were in the previous Monad discussion thread,
what do you think of the Monad this time?

[Waldek Hebisch]

We have more than 50 packages named '*Functions2' which
implement 'map' between two domains. In principle
they could use single signature from single category. However:

- Functor is quite loaded name and may lead to confusion.
Something like 'MapCategory2' seem to fit better existing
naming scheme.
- What documentatin do you propose for the 'map' function?
Current scheme with several signatures has a separate
documentation slot per signature. Common signature would
be quite abstract, so hard to specify.

--
Waldek Hebisch

[oldk1331]

> We have more than 50 packages named '*Functions2' which
> implement 'map' between two domains.

I am not suggesting replace those packages that deals with
more than two domains. I'm talking about
map : (S->S, %) -> % , where % has a parameter S
There are about 15 map signatures like this.

> Functor is quite loaded name and may lead to confusion.

Yes, the name is a problem. OpenAxiom uses "Functorial".
But I think Functor is fine, given the context that Haskell is
using this name.

> - What documentatin do you propose for the 'map' function?

From https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Functor.html ,
"uniform action over a parameterized type".

[Ralf Hemmecke]

>> Functor is quite loaded name and may lead to confusion.
>
> Yes, the name is a problem. OpenAxiom uses "Functorial".
> But I think Functor is fine, given the context that Haskell is
> using this name.

BTW, in Aldor the "Maybe" domain is called "Partial".
https://github.com/pippijn/aldor/blob/master/aldor/lib/aldor/src/base/sal_partial.as

Traditionally, my usage of the term "functor" in the context of
AXIOM/FriCAS would be that it is any parametrized domain.

If a (domain)constructor with name Functor is introduced, that would
confuse me a bit, if that thing is restricted to just export

map: (S -> S, %) -> %

Additionally, if the definition is

Functor(S : Type) : Category == Type with

map: (S -> S, %) -> %

then this "Functor" is of type "Category" and this I find rather
strange. If one defines "Foo(X: Category): Category == ..." then I would
be tempted to call Foo (which can be seen as a "function" with type
Category->Category) as a Functor, but you want "Functor" instead of
"Foo" and that does not fit with category theory in my understanding.

Like Waldek, I also think that MapCategory2 would fit better into
FriCAS. I am not so much in favour of copying the terminology of
Haskell. In particular, if FriCAS is going to implement

> Monad(S : Type) : Category == Type with
> _>_> : (%, S -> %) -> %

that would confuse me quite a bit.

Naming of functions and domains aside, I find this implementation
somewhat hacky, in particular the line starting with "if FA is Maybe A".

> )abbrev package FUNCTOR2 FunctorPackage
> FunctorPackage(A : Type, B : Type, FA : Functor A, FB : Functor B) :
> Exports == Implementation where
> Exports == with
> map : (A -> B, FA) -> FB
> Implementation == add
> if FA is Maybe A and FB is Maybe B then
> map(f, fa) ==
> if nothing?(fa)$Maybe(A) then nothing()$Maybe(B)
> just f fromJust fa

If FA and FB are restricted to just one domain, then why would one want
to put them as parameters?

FunctorPackage(A : Type, B : Type) :
Exports == Implementation where
FA ==> Maybe A
FB ==> Maybe B

Exports == with
map : (A -> B, FA) -> FB
Implementation == add

map(f, fa) ==
if nothing?(fa)$FA then nothing()$FB
just f fromJust fa

You probably suggested that, because the "if" line shouldn't be there
and you actually wanted something that applies to all pairs of monads.
But your FunctorPackage just does the lifting of map for only one
particular monad (namely Maybe).

I'm still of the opinion that the concept of monads cannot be nicely
defined in SPAD.
https://groups.google.com/d/msg/fricas-devel/UCFkQGgOOf0/RzbEtrbYIHUJ

Note that in

https://wiki.haskell.org/Monad
class Monad m where
(>>=) :: m a -> (a -> m b) -> m b
(>>) :: m a -> m b -> m b
return :: a -> m a
fail :: String -> m a

the "m" appears in front of a and in front of b. I'm not aware of a
SPAD/Aldor syntax that can describe this situation.

Ralf

[oldk1331]

On Mon, Oct 17, 2016 at 3:53 PM, Ralf Hemmecke <ra...@hemmecke.org> wrote:
>>> Functor is quite loaded name and may lead to confusion.
>>
>> Yes, the name is a problem. OpenAxiom uses "Functorial".
>> But I think Functor is fine, given the context that Haskell is
>> using this name.
>
> BTW, in Aldor the "Maybe" domain is called "Partial".
> https://github.com/pippijn/aldor/blob/master/aldor/lib/aldor/src/base/sal_partial.as

I'd be OK to adopt this name.

> You probably suggested that, because the "if" line shouldn't be there
> and you actually wanted something that applies to all pairs of monads.
> But your FunctorPackage just does the lifting of map for only one
> particular monad (namely Maybe).

Yes, that package is supposed for ALL Funtors, to
(potenially) replace current 50+ '*Functions2' package,
not invent a new one solely for Maybe:
if FA is Maybe A and FB is Maybe B then ...
if FA is X A and FB is X B then ...
if FA is Y A and FB is Y B then ...

> I'm still of the opinion that the concept of monads cannot be nicely
> defined in SPAD.
> https://groups.google.com/d/msg/fricas-devel/UCFkQGgOOf0/RzbEtrbYIHUJ
>
> Note that in
>
> https://wiki.haskell.org/Monad
> class Monad m where
> (>>=) :: m a -> (a -> m b) -> m b
> (>>) :: m a -> m b -> m b
> return :: a -> m a
> fail :: String -> m a
>
> the "m" appears in front of a and in front of b. I'm not aware of a
> SPAD/Aldor syntax that can describe this situation.

That "m" stands for "the same Monad constructor", Spad don't have similar
syntax, that's why I have to simulate it by "if FA is Maybe A and FB
is Maybe B".
This package doesn't forbid MONADPKG(String, Integer, Maybe String,
List Integer),
which is obviously wrong.

[Martin Baker]

It seems to me that there are two possible reasons for implementing
category theoretic structures in FriCAS:

1) Because FriCAS should implement as many mathematical structures as
possible and because much of modern mathematics is done in the language
of categories and FriCAS should reflect the structures mathematicians
are using.

2) To implement Haskel-like structures. This is aimed at separating the
'pure' from the 'impure' in particular chaining together sequences of
potentially impure functions.

I think this distinction is important because it determines what type of
structure is used. In the first case we might use this:

class Monad m where
unit :: a -> m a
mult :: m (m a) -> m a

But in the second case we might use this:

class Monad m where
(>>=) :: m a -> (a -> m b) -> m b
(>>) :: m a -> m b -> m b
return :: a -> m a
fail :: String -> m a

So in the case of Maybe, in the second case we could chain together a
whole sequence of functions with a signature like this:

Something -> Maybe Something

into a combined function, this would mean that we would not have to test
for "fail" in-between each function call.

In the first case we would have a structure like this:

Maybe (Maybe Something)

which, presumably would return "fail" if either the inner or outer Maybe
failed.

I suspect this is all a bit academic because I get the impression that
the FriCAS compiler is too unpredictable to make the changes to the type
system that would be required for a more general category theoretic
structures. Please tell me I'm wrong as it would be really wonderful if
FriCAS could support this in its most general form.

Martin B

[Bill Page]

On 16 October 2016 at 22:26, oldk1331 <oldk...@gmail.com> wrote:
> Bill, you were in the previous Monad discussion thread,
> what do you think of the Monad this time?
>

As you can see, everyone is already quite fixed in their opinions
therefore I am very happy for your interest and in your suggestions.
In general I am in favor of your approach but given Waldek's more
pragmatic orientation I am not certain that it is a good match for
FriCAS. Rather than Haskell per se, personally I am most interested in
the "category theory" approach summarized in Martin's email, therefore
I prefer the alternative definition of monads as a domain satisfying
Functor

map :: (a -> b) -> M a -> M b

with these two additional operations:

return :: a -> M a
join :: M (M a) -> M a

instead of "bind".

https://en.wikibooks.org/wiki/Haskell/Understanding_monads#Monads_and_Category_Theory

I am not so concerned about any possible confusion between the name
"Functor" and the its earlier association with type constructors in
Axiom but I do like Ralf's suggestion to adopt the Aldor name
"Partial" rather than "Maybe". I think the usage of "Functor" in
Haskell is in this case a better match.

Concerning your hack for FunctorPackage and MonadPackage you might be
interested in another OpenAxiom innovation implementing the "forall"
universal quantifier which often eliminates the need to write separate
packages.

Bill Page.

[oldk1331]

> Rather than Haskell per se, personally I am most interested in
> the "category theory" approach summarized in Martin's email, therefore
> I prefer the alternative definition of monads as a domain satisfying
> Functor
>
> map :: (a -> b) -> M a -> M b
>
> with these two additional operations:
>
> return :: a -> M a
> join :: M (M a) -> M a
>
> instead of "bind".

We can have both. BTW, the 'join' operation is impossible to deal
with more than one type?

> Concerning your hack for FunctorPackage and MonadPackage you might be
> interested in another OpenAxiom innovation implementing the "forall"
> universal quantifier which often eliminates the need to write separate
> packages.

Yes! One thing I felt lacking in FriCAS is the "forall" quantifier, aka
anonymous packages. Another thing is category/domain constructor
as first class entity: in principle Maybe is a domain constructor with
type Domain->Domain, and a member of Monad, but FriCAS only
recognize "Maybe INT has Monad INT", not "Maybe has Monad" nor
"x : Monad" in package parameter.

[Bill Page]

On 17 October 2016 at 10:52, oldk1331 <oldk...@gmail.com> wrote:
>> Rather than Haskell per se, personally I am most interested in
>> the "category theory" approach summarized in Martin's email, therefore
>> I prefer the alternative definition of monads as a domain satisfying
>> Functor
>>
>> map :: (a -> b) -> M a -> M b
>>
>> with these two additional operations:
>>
>> return :: a -> M a
>> join :: M (M a) -> M a
>>
>> instead of "bind".
>
> We can have both. BTW, the 'join' operation is impossible to deal
> with more than one type?

In 'join' more than one type is not necessary. The main work is done
by 'map' which is presumed to be able to handle this case.

>
>> Concerning your hack for FunctorPackage and MonadPackage you might
>> be interested in another OpenAxiom innovation implementing the "forall"
>> universal quantifier which often eliminates the need to write separate
>> packages.
>
> Yes! One thing I felt lacking in FriCAS is the "forall" quantifier, aka
> anonymous packages. Another thing is category/domain constructor
> as first class entity: in principle Maybe is a domain constructor with
> type Domain->Domain, and a member of Monad, but FriCAS only
> recognize "Maybe INT has Monad INT", not "Maybe has Monad" nor
> "x : Monad" in package parameter.
>

Here is another rather long and related thread on this subject from 2011:

https://groups.google.com/d/msg/fricas-devel/DEu215PYERg/m7SAlBDNofQJ

Unfortunately it did not end in a complete resolution even in
OpenAxiom. Perhaps now with your interest we can make some more
progress?

Bill Page.

[Kurt Pagani]

Am 17.10.2016 um 11:13 schrieb Martin Baker:

> I suspect this is all a bit academic because I get the impression that the
> FriCAS compiler is too unpredictable to make the changes to the type system that
> would be required for a more general category theoretic structures. Please tell
> me I'm wrong as it would be really wonderful if FriCAS could support this in its
> most general form.
>
> Martin B
>
>

It's a bit academic, indeed. I use macros as Waldek described in a former post -
just a pragmatic approach. However, it would certainly be desirable to have a
'maybe' monad in fricas, and I see no reason why it shouldn't be feasible. In
OCaml for instance, the monad is implemented in the module 'Option' and seems to
me a pretty straightforward approach. On the other hand I'd rather like a
"partial" monad instead of "maybe" (which usually means a single terminal symbol
"failed"), that is a product type M(T)=T x Q, where Q is a monoid, such that the
Kleisli composition evaluates the two programs in sequence and combines their Q
output. Example: Q=(String, conctenation).

[oldk1331]

> On the other hand I'd rather like a
> "partial" monad instead of "maybe" (which usually means a single terminal symbol
> "failed"), that is a product type M(T)=T x Q, where Q is a monoid, such that the
> Kleisli composition evaluates the two programs in sequence and combines their Q
> output. Example: Q=(String, conctenation).

That would be a little like Haskell's IO Monad, because it concatenates string
one by one, useful for logging, for example. That can be considered.

[Bill Page]

On 17 October 2016 at 12:27, Kurt Pagani <nil...@gmail.com> wrote:

> ... On the other hand I'd rather like a "partial" monad instead of "maybe"

> (which usually means a single terminal symbol "failed"), that is a product
> type M(T)=T x Q, where Q is a monoid, such that the Kleisli composition
> evaluates the two programs in sequence and combines their Q output.
> Example: Q=(String, conctenation).
>

Doesn't that conflate two different ideas? E.g. a partial function
like division by 0, versus a function whose definition is such that
attempting to compute it may never return such as general equality of
functions? Or perhaps I am not properly understanding these Haskellish
notions.

[Kurt Pagani]

A great source where my half-baken knowledge about monads comes from is:

https://ncatlab.org/nlab/show/monad
https://ncatlab.org/nlab/show/monad+%28in+computer+science%29

Especially the section "For imperative programs in functional programming" in the page of the last link will describe what I meant with "partial" (admittedly an unhappy invention of mine). I had to look for the link some time but now we'll see that it essentially is an IO monad as oldk already pointed out.

I think it might be useful to implement it in this generality because the usual "maybe" is included and there are other interesting cases besides IO (I used it once in Pure to implement the Martelli-Montanari unification algorithm w. side effects).

So don't be confused by the "partial" notion.

--
You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email to fricas-devel+unsubscribe@googlegroups.com.
To post to this group, send email to fricas...@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.

[Bill Page]

On 19 October 2016 at 14:51, Kurt Pagani <nil...@gmail.com> wrote:
> A great source where my half-baken knowledge about monads comes from is:
>
> https://ncatlab.org/nlab/show/monad
> https://ncatlab.org/nlab/show/monad+%28in+computer+science%29
>
> Especially the section "For imperative programs in functional programming"
> in the page of the last link will describe what I meant with "partial"
> (admittedly an unhappy invention of mine). I had to look for the link some
> time but now we'll see that it essentially is an IO monad as oldk already
> pointed out.
> I think it might be useful to implement it in this generality because the
> usual "maybe" is included and there are other interesting cases besides IO
> (I used it once in Pure to implement the Martelli-Montanari unification
> algorithm w. side effects).
>
> So don't be confused by the "partial" notion.

Ah, OK that makes sense.

I thought perhaps you meant something along this line ...

https://www.reddit.com/r/haskell/comments/1bjfx9/partial_function_maybe/c98fd8h