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)
--
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 [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
