login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit
SandBoxFriCAS2
  ↑ →  Sandbox Errors

SandBoxMaybe
  
last edited 11 years ago by Bill Page

Edit detail for SandBoxMaybe revision 43 of 46
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
Editor: gdr
Time: 2008/05/28 00:05:03 GMT-7
Note: I can reproduce the failure 
added:

From gdr Wed May 28 00:05:03 -0700 2008
From: gdr
Date: Wed, 28 May 2008 00:05:03 -0700
Subject: I can reproduce the failure
Message-ID: <20080528000503-0700@axiom-wiki.newsynthesis.org>
In-Reply-To: <20080527233412-0700@axiom-wiki.newsynthesis.org>

Now, I can -- I failed to copy and paste 
properly.  And on reflection, the fact the
interpreter rejected the code should have alerted
me to close closer.  And yes, the failure
is related to the same bug.







... --gdr,  Mon, 26 May 2008 14:24:29 -0700 reply
\begin{spad}
)abbrev domain MAYBE Maybe
Maybe(T: Type) == Union(T,"failed")
\end{spad}


need result type --Bill Page,  Mon, 26 May 2008 20:25:03 -0700 reply
\begin{spad}
)abbrev domain MAYBE Maybe
Maybe(T: Type):Type == Union(T,"failed")
\end{spad}


\begin{axiom}
)show Maybe
\end{axiom}


need result type --gdr,  Mon, 26 May 2008 22:03:52 -0700 reply
No, there should not be a need for specifying result type.  In fact, if you specify
"Type" as result type, you explicitly ask for not having any exported
operation.  That wasn't the intent.  The intent was to get whatever the
right hand side exported as exports.  Such as in
\begin{spad}
)abbrev domain MYFIELD MyField
MyField() == Fraction Integer
\end{spad}


\begin{axiom}
)sh MyField
\end{axiom}


macro --Bill Page,  Tue, 27 May 2008 07:30:43 -0700 reply
Macro versus domain
\begin{axiom}
macro Maybe(T) == Union(T,"failed")
)sh Maybe(Integer)
\end{axiom}


\begin{axiom}
x:Maybe(Integer)
x:=-3
\end{axiom}


explicit exports --Bill Page,  Tue, 27 May 2008 07:46:20 -0700 reply
\begin{spad}
)abbrev domain MAYBE2 Maybe2
Maybe2(T: Type):with
    _= : (%,%) -> Boolean
    autoCoerce : % -> failed
    autoCoerce : % -> T
    autoCoerce : failed -> %
    autoCoerce : T -> %
    _case: (%,failed) -> Boolean
    _case: (%,T) -> Boolean
    coerce : % -> failed
    coerce : % -> T
    coerce : % -> OutputForm
    coerce : T -> %
  == Union(T,"failed") add
    coerce(x:T):% == autoCoerce(x)
\end{spad}


\begin{axiom}
)show Maybe2
\end{axiom}


\begin{axiom}
y:Maybe2(Integer)
y:=-3
y:=autoCoerce(-3::Integer)
\end{axiom}


macro --gdr,  Tue, 27 May 2008 08:01:39 -0700 reply
But, the use of macro is a workaround a fundamental problem
in the compiler -- which I'm desperately trying to convey.


explicit exports --gdr,  Tue, 27 May 2008 08:03:19 -0700 reply
This and the original bug comes from the same source
in the compiler.  


Re: problem in the compiler --Bill Page,  Tue, 27 May 2008 08:06:29 -0700 reply
I agree. I am just trying to understand it.


Why does:

  Maybe(T: Type) == Union(T,"failed")





and:

  Maybe(T: Type):Type == Union(T,"failed")





have such different semantics? Is this a good thing? Maybe there is a need for something that stands for the type of the rhs:

  Maybe(T: Type):rhs == Union(T,"failed")





Re: problem in the compiler --gdr,  Tue, 27 May 2008 09:20:19 -0700 reply
Remember that Type is a category that exports no operation.  so when you say
Maybe(T: Type): Type, you are exlicitly saying that Maybe(T: Type) is a domain
constructor that exports no operation.  Indeed, if you try )show
with OpenAxiom?, you will see that it say, Maybe has no exported operations.
Which is right.


However, when one says Maybe(T: Type) == Union(T, "failed"), one is saying
that Maybe(T) is exactly like Union(T,"failed"), except for the name.
Consequently, Maybe has the exports inferred from the right hand side.
This works for all domains, except the `builtin' domains.  If you
try Record or Enumeration, you should hit a bug in the compiler at some
point.


exports inferred from RHS --Bill Page,  Tue, 27 May 2008 12:58:47 -0700 reply
\begin{spad}
)abbrev domain MYPAIR MyPair?
MyPair?(T:Type) == Record(X:T,Y:T)
\end{spad}


\begin{axiom}
)show MyPair?(Integer)
\end{axiom}


\begin{spad}
)abbrev domain MYPAIR2 MyPair2?
MyPair2?(T:Type): with
    _= : (%,%) -> Boolean
    coerce : % -> OutputForm?
    copy : % -> %
    _. : (%,X) -> Integer
    _. : (%,Y) -> Integer
    setelt : (%,X,Integer) -> Integer
    setelt : (%,Y,Integer) -> Integer
    _~_= : (%,%) -> Boolean
    construct : (Integer,Integer) -> %
  == Record(X:T,Y:T)
\end{spad}


\begin{axiom}
)show MyPair2?(Integer)
\end{axiom}


\begin{axiom}
x2:MyPair2?(INT):=[-1,-2]?
\end{axiom}


Maybe(T:Type)== --Bill Page,  Tue, 27 May 2008 13:37:18 -0700 reply
gdr wrote:



    

  • one is saying that Maybe(T) is exactly like Union(T,"failed")
    • 




What is the advantage of this notation over the use of a macro?


Besides domain composition, constant substitution and passing of
parameters, like:

  Maybe(T: Type) == Union(Fraction T,"failed")





what other useful expressions are allowed on the rhs?


Persumably add would not make sense because we cannot
specify new exports - at least not without explicitly
specifying all exports.


This is a common problem for possible re-use of code
(subject of another thread). For example:

   NonNegativeInteger():rhs
     without
       _-:(%,%) -> %
     with
       subtractIfCan:(%,%)->Union(%,"failed")
   == Integer add
     subtractIfCan(x,y) ==
       x > y => x-y
       "failed"





What should I put instead of rhs? Should I be able to
explicitly "forget" (or replace) some exports?


\begin{spad}
)abbrev domain MYNNI MyNonNegativeInteger?
MyNonNegativeInteger?():IntegerNumberSystem? with
    subtractIfCan:(%,%)->Union(%,"failed")
  == Integer add
    subtractIfCan(x:%,y:%):Union(%,"failed") ==
      x > y => x-y
      "failed"
\end{spad}


... --gdr,  Tue, 27 May 2008 15:28:30 -0700 reply
A macro name is not a constructor name, so that makes a fundamental
difference.


... --gdr,  Tue, 27 May 2008 15:29:31 -0700 reply
Do we have a `without' construct?


... --gdr,  Tue, 27 May 2008 15:39:25 -0700 reply
With an OpenAxiom? built on May 16, 2008 I have a different behaviour: The assignment
is rejected because there is no conversion from [-1,2] to MyPair2(INT).  Which is right.
The output of the compiler indicates to me that the website is running
a very old OpenAxiom?.


not so old --page,  Tue, 27 May 2008 15:45:24 -0700 reply
The version of OpenAxiom? being used for this page was build from svn on May 27, 2008:
\begin{axiom}
)version
\end{axiom}


Re: without construct --page,  Tue, 27 May 2008 15:46:58 -0700 reply
No, it's only in my imagination.


Re: macro --page,  Tue, 27 May 2008 16:52:11 -0700 reply
Previously Bill Page wrote:

  Macro versus domain

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





gdr wrote:

  But, the use of macro is a workaround a fundamental problem
  in the compiler ...





Bill Page wrote:

  Agreed, but what is the advantage of this notation:

    Maybe(T:Type) == Union(T,"failed")

  over the use of a macro?





gdr wrote:

  A macro name is not a constructor name, so that makes
  a fundamental difference.





Of course there is a difference to the compiler but is
there a "fundamental difference" to the programmer? Does
the language benefit from being able to compile domains
with an identical list exports as some other domain?


I suppose here's one possible advantage:



    

  • To provide standard simplified interfaces to more
  complex domains defined in the library.
    • 

  • Macros are not stored as part of the Axiom library.
    • 




macro --gdr,  Tue, 27 May 2008 16:58:18 -0700 reply
Well, as you said, macros are not stored in the databases.
In OpenAxiom?, one can use constructor names as arguments to functions.
That does not work with macro names -- they don't really define a
new category or domain or package.


Something you can only do in OpenAxiom?! --page,  Tue, 27 May 2008 17:42:52 -0700 reply
Because you can pass domains as arguments to functions:
\begin{axiom}
Maybe3(T: Domain):Domain == Union(T,"failed")
x:Maybe3(Integer):=-2
x:="failed"
\end{axiom}


Internal Error --page,  Tue, 27 May 2008 20:49:00 -0700 reply
gdr wrote:

  With an OpenAxiom built on May 16, 2008 I have a different behaviour:
  The assignment is rejected because there is no conversion from
  [-1,2] to MyPair2(INT).





After upgrading this page to OpenAxiom? built with current (May 27, 2008 Rev: 614) source:
\begin{axiom}
)version
\end{axiom}


This example still fails:
\begin{axiom}
xy:MyPair2?(INT):=[-1,2]?
\end{axiom}


... --gdr,  Tue, 27 May 2008 23:34:12 -0700 reply
this is weird: I cannot reproduce the failure.




I can reproduce the failure --gdr,  Wed, 28 May 2008 00:05:03 -0700 reply
Now, I can


I failed to copy and paste 
properly.  And on reflection, the fact the
interpreter rejected the code should have alerted
me to close closer.  And yes, the failure
is related to the same bug.




    Some or all expressions may not have rendered properly,
    because Axiom returned the following error:
Error: export AXIOM=/usr/local/lib/open-axiom/x86_64-unknown-linux/1.2.0-2008-05-25; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 600; export LD_LIBRARY_PATH=/usr/local/lib/open-axiom/x86_64-unknown-linux/1.2.0-2008-05-25/lib; LANG=en_US.UTF-8 $AXIOM/bin/AXIOMsys < /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/8189285174477700121-25px.axm
/bin/sh: /usr/local/lib/open-axiom/x86_64-unknown-linux/1.2.0-2008-05-25/bin/AXIOMsys: not found
Some or all expressions may not have rendered properly, because Latex returned the following error:
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6)
 \write18 enabled.
 %&-line parsing enabled.
entering extended mode
(./8657816242270770496-16.0px.tex
LaTeX2e <2005/12/01>
Babel <v3.8h> and hyphenation patterns for english, usenglishmax, dumylang, noh
yphenation, arabic, farsi, croatian, ukrainian, russian, bulgarian, czech, slov
ak, danish, dutch, finnish, basque, french, german, ngerman, ibycus, greek, mon
ogreek, ancientgreek, hungarian, italian, latin, mongolian, norsk, icelandic, i
nterlingua, turkish, coptic, romanian, welsh, serbian, slovenian, estonian, esp
eranto, uppersorbian, indonesian, polish, portuguese, spanish, catalan, galicia
n, swedish, ukenglish, pinyin, loaded.
(/usr/share/texmf-texlive/tex/latex/base/article.cls
Document Class: article 2005/09/16 v1.4f Standard LaTeX document class
(/usr/share/texmf-texlive/tex/latex/base/size12.clo))
(/usr/share/texmf-texlive/tex/latex/ucs/ucs.sty
(/usr/share/texmf-texlive/tex/latex/ucs/data/uni-global.def))
(/usr/share/texmf-texlive/tex/latex/base/inputenc.sty
(/usr/share/texmf-texlive/tex/latex/ucs/utf8x.def))
(/usr/share/texmf-texlive/tex/latex/bbm/bbm.sty)
(/usr/share/texmf-texlive/tex/latex/jknapltx/mathrsfs.sty)
(/usr/share/texmf-texlive/tex/latex/base/fontenc.sty
(/usr/share/texmf-texlive/tex/latex/base/t1enc.def))
(/usr/share/texmf-texlive/tex/latex/pstricks/pstricks.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.tex
`PSTricks' v1.15  <2006/12/22> (tvz)
(/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.con))
(/usr/share/texmf/tex/latex/xcolor/xcolor.sty
(/etc/texmf/tex/latex/config/color.cfg)
(/usr/share/texmf-texlive/tex/latex/graphics/dvips.def)
(/usr/share/texmf-texlive/tex/latex/graphics/dvipsnam.def)))
(/usr/share/texmf-texlive/tex/latex/graphics/epsfig.sty
(/usr/share/texmf-texlive/tex/latex/graphics/graphicx.sty
(/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty)
(/usr/share/texmf-texlive/tex/latex/graphics/graphics.sty
(/usr/share/texmf-texlive/tex/latex/graphics/trig.sty)
(/etc/texmf/tex/latex/config/graphics.cfg))))
(/usr/share/texmf-texlive/tex/latex/pst-grad/pst-grad.sty
(/usr/share/texmf-texlive/tex/generic/pst-grad/pst-grad.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/pst-xkey.tex
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.sty
(/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.tex)))
`pst-plot' v1.05, 2006/11/04 (tvz,dg,hv)))
(/usr/share/texmf-texlive/tex/latex/pstricks/pst-plot.sty
(/usr/share/texmf-texlive/tex/generic/pstricks/pst-plot.tex
 v97 patch 2, 1999/12/12
(/usr/share/texmf-texlive/tex/generic/multido/multido.tex
 v1.41, 2004/05/18 <tvz>)))
(/usr/share/texmf-texlive/tex/latex/geometry/geometry.sty
(/usr/share/texmf-texlive/tex/xelatex/xetexconfig/geometry.cfg)


Package geometry Warning: `lmargin' and `rmargin' result in NEGATIVE (-108.405p
t).
    `width' should be shortened in length.


) (/usr/share/texmf-texlive/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `? option.
(/usr/share/texmf-texlive/tex/latex/amsmath/amstext.sty
(/usr/share/texmf-texlive/tex/latex/amsmath/amsgen.sty))
(/usr/share/texmf-texlive/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texmf-texlive/tex/latex/amsmath/amsopn.sty))
(/usr/share/texmf-texlive/tex/latex/amsfonts/amsfonts.sty)
(/usr/share/texmf-texlive/tex/latex/amsfonts/amssymb.sty)
(/usr/share/texmf-texlive/tex/latex/amscls/amsthm.sty)
(/usr/share/texmf-texlive/tex/latex/setspace/setspace.sty
Package: `setspace 6.7 <2000/12/01>
) (/usr/share/texmf-texlive/tex/generic/xypic/xy.sty
(/usr/share/texmf-texlive/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes,
docmode, (/usr/share/texmf-texlive/tex/generic/xypic/xyrecat.tex)
(/usr/share/texmf-texlive/tex/generic/xypic/xyidioms.tex)
 Xy-pic version 3.7 <1999/02/16>
 Copyright (c) 1991-1998 by Kristoffer H. Rose <krisrose@ens-lyon.fr>
 Xy-pic is free software: see the User's Guide for details.




Loading kernel: messages; fonts; allocations: state, direction,
utility macros; pictures: \xy, positions, objects, decorations;
kernel objects: directionals, circles, text; options; algorithms: directions,
edges, connections;  Xy-pic loaded))
(/usr/share/texmf-texlive/tex/generic/xypic/xyall.tex
 Xy-pic option: All features v.3.3
(/usr/share/texmf-texlive/tex/generic/xypic/xycurve.tex
 Xy-pic option: Curve and Spline extension v.3.7 curve, circles, loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyframe.tex
 Xy-pic option: Frame and Bracket extension v.3.7 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xycmtip.tex
 Xy-pic option: Computer Modern tip extension v.3.3
(/usr/share/texmf-texlive/tex/generic/xypic/xytips.tex
 Xy-pic option: More Tips extension v.3.3 loaded) loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyline.tex
 Xy-pic option: Line styles extension v.3.6 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyrotate.tex
 Xy-pic option: Rotate and Scale extension v.3.3 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xycolor.tex
 Xy-pic option: Colour extension v.3.3 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xymatrix.tex
 Xy-pic option: Matrix feature v.3.4 loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xyarrow.tex
 Xy-pic option: Arrow and Path feature v.3.5 path, \ar, loaded)
(/usr/share/texmf-texlive/tex/generic/xypic/xygraph.tex
 Xy-pic option: Graph feature v.3.7 loaded) loaded)
(/usr/share/texmf-texlive/tex/latex/tools/verbatim.sty)
(/usr/share/texmf/tex/latex/graphviz/graphviz.sty
(/usr/share/texmf-texlive/tex/latex/psfrag/psfrag.sty))
(/usr/share/texmf/tex/latex/sagetex.sty
Writing sage input file 8657816242270770496-16.0px.sage
(./8657816242270770496-16.0px.sout))
(/usr/share/texmf-texlive/tex/latex/gnuplottex/gnuplottex.sty
(/usr/share/texmf-texlive/tex/latex/base/latexsym.sty)
(/usr/share/texmf-texlive/tex/latex/moreverb/moreverb.sty)
(/usr/share/texmf-texlive/tex/latex/base/ifthen.sty))
(./8657816242270770496-16.0px.aux)
(/usr/share/texmf-texlive/tex/latex/ucs/ucsencs.def) [1] [2]
(/usr/share/texmf-texlive/tex/latex/base/t1cmtt.fd)


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 131.


[3]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 138.


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 142.


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 146.


 Missing $ inserted.
<inserted text> 
                $
l.150     _
           = : (%,%) -> Boolean
(/usr/share/texmf-texlive/tex/latex/jknapltx/ursfs.fd)
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd)
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsb.fd)
(/usr/share/texmf-texlive/tex/latex/base/ulasy.fd)
 Missing $ inserted.
<inserted text> 
                $
l.163 \end{spad}
                \newpage
[4]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 166.


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 171.


[5]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 178.


 Missing $ inserted.
<inserted text> 
                $
l.182     _
           = : (%,%) -> Boolean
 Missing { inserted.
<to be read again> 
                   \unhbox 
l.189     _~
            _= : (%,%) -> Boolean
 Missing } inserted.
<inserted text> 
                }
l.192 \end{spad}
                \newpage
 Missing $ inserted.
<inserted text> 
                $
l.192 \end{spad}
                \newpage


Overfull \hbox (9.20914pt too wide) in paragraph at lines 180--192
\T1/cmr/m/n/12 )abbrev do-main MY-PAIR2 My-Pair2 My-Pair2(T:Type): with $[] \OT
1/cmr/m/n/12 : (\OML/cmm/m/it/12 coerce \OT1/cmr/m/n/12 : \OML/cmm/m/it/12 copy
 \OT1/cmr/m/n/12 :[]: ([]: (\OML/cmm/m/it/12 setelt \OT1/cmr/m/n/12 : (\OML/cmm
/m/it/12 setelt \OT1/cmr/m/n/12 : ([]$ 
[6]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 195.


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 198.


[7]


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 210.


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 215.


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 218.


LaTeX Warning: Characters dropped after `\end{axiom}' on input line 221.


[8] (./8657816242270770496-16.0px.aux) )
(see the transcript file for additional information)
Output written on 8657816242270770496-16.0px.dvi (8 pages, 4176 bytes).
Transcript written on 8657816242270770496-16.0px.log.