On 6 October 2017 at 19:59, oldk1331 <[email protected]> wrote: > > Monad is practical in FriCAS. But just like this time, we couldn't > agree on a lot of things. So instead of introducing Monad first, Maybe > later; I think introducing Maybe first, then add Monad later will be > easier. >
For me FriCAS/Axiom is first and foremost about mathematics and mathematics does not require consensus, only rigor, so discussion is useful in order to consider broader issues but it is not necessary to agree in order to proceed. In the end the utility of a particular construction will determine whether or not it is widely adopted. Unfortunately our community is very small so this process can take a long time. > On Fri, Oct 6, 2017 at 11:40 PM, Martin Baker <[email protected]> wrote: >> Also the terminology is well known from Haskell (where maybe is >> an instance of monad) so its best not to diverge from that unless >> necessary for a genuine mathematical reason. > > In previous discussion on Monad, we couldn't agree on the name > 'Functor', because we already use that for Domain Constructor. > I agree with you that we should borrow terminology from Haskell > instead of introducing new one. > It seems to me that in FriCAS, methodologies from computer science are only a means to the end of implementing more mathematically-oriented functionality. So I think mathematical notions from category theory actually trump specific implementations such as represented by Haskell. However Haskell does represent a significant advance as a semantically rigorous programming language and can certainly serve as a good example for FriCAS. >> I believe that monads are an (endo) functor with two natural >> transformations: >> >> M M X -> M X >> X -> M X >> >> In the maybe instance: >> >> Maybe Maybe X -> Maybe X >> X -> Maybe X > > That's another difficult for Monad in previous discussion. > In Category Monad, you can't express signature like "Maybe Maybe X", > where % stands for Maybe X. > > There's another set of natural transformations for Monad: > > return : X -> Maybe X >>>= : (Maybe X, X -> Maybe X) -> Maybe X > The term "natural transformation" has a very specific meaning in category theory. See for example "Monads Made Difficult" by Stephen Diehl http://www.stephendiehl.com/posts/monads.html I do not see how you can treat "return" and "bind" (>>=) as natural transformations but they can be defined in terms of the 'eta' and 'mu' natural transformations together with 'fmap' from Functor. >> I'm not sure about the practicalities but perhaps to chain something like >> subtractIfCan would require a signature like: >> >> (Maybe X,Maybe X) -> Maybe X >> rather than: >> (X,X) -> Maybe X >> >> but I have not really thought this through. Does anyone know how Maybe is >> used in Haskell? > > It's the >>= I mentioned above. It can chain single argument > functions together. > > f : X -> Maybe X > g : X -> Maybe X > > a >>= f >>= g > See the 'bind' implementation for 'Maybe' in the attached file. (1) -> )co maybe Compiling FriCAS source code from file /home/wspage/maybe.spad using old system compiler. MAYBE abbreviates domain Maybe ------------------------------------------------------------------------ Maybe is now explicitly exposed in frame frame1 Maybe will be automatically loaded when needed from /home/wspage/MAYBE.NRLIB/MAYBE MAYBE2 abbreviates package MaybeFunctions2 ------------------------------------------------------------------------ MaybeFunctions2 is now explicitly exposed in frame frame1 MaybeFunctions2 will be automatically loaded when needed from /home/wspage/MAYBE2.NRLIB/MAYBE2 MAYBE1 abbreviates package MaybeFunctions1 ------------------------------------------------------------------------ MaybeFunctions1 is now explicitly exposed in frame frame1 MaybeFunctions1 will be automatically loaded when needed from /home/wspage/MAYBE1.NRLIB/MAYBE1 (1) -> minus1(x:NNI):Maybe NNI == if x>0 then return x-1 else return empty()$Maybe(NNI) Function declaration minus1 : NonNegativeInteger -> Maybe( NonNegativeInteger) has been added to workspace. Type: Void Time: 0 sec (2) -> M1:Maybe NNI := 1 (2) [1] Type: Maybe(NonNegativeInteger) Time: 0 sec (3) -> M0:=bind(M1,minus1) Compiling function minus1 with type NonNegativeInteger -> Maybe( NonNegativeInteger) (3) [0] Type: Maybe(NonNegativeInteger) Time: 0.00 (IN) + 0.04 (OT) = 0.04 sec (4) -> bind(M0,minus1) (4) [] Type: Maybe(NonNegativeInteger) Time: 0 sec (5) -> M:Maybe NNI := empty() (5) [] Type: Maybe(NonNegativeInteger) Time: 0 sec (6) -> bind(M,minus1) (6) [] Type: Maybe(NonNegativeInteger) Time: 0 sec Note that I have used the notation [ ] for "failed" and that R-values in 'Maybe R' are also shown inside brackets. Bill Page -- 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.
maybe.spad
Description: Binary data
