Re: [isabelle] Rational numbers in Isabelle/ML
On Fri, 1 Apr 2016, Manuel Eberl wrote:
I noticed that there is an ML implementation of rational numbers in the
Isabelle distribution (~~/src/Tools/rat.ML).
I don't think this is relevant to isabelle-users. Rat is just one of many
auxiliary modules in the implementation. I will nonetheless continue here,
to avoid cross-mailing list confusion wrt. isabelle-dev.
There are a few issues with this:
â for some reason, it does not use operator overloading for
addition/multiplication/equality/etc. on rational numbers, but introduces a
"+/", "*/" etc. syntax for it.
This follows Standard ML. Adhoc overloading is not defined by the language
and works differently in each implementation.
Since SML/NJ has been discontinued after Isabelle2016 (see
http://sketis.net/2016/isabelle-no-longer-supports-smlnj) and old versions
of Poly/ML as well, we can in principle become more specific to a
particular Poly/ML version. This means that standard-ness is given up, and
the game becomes more like that of OCaml (or Scala, even Haskell/GHC). I
am myself still unsure if this is good or bad.
I have already implemented all of these things in my own little version
of rational numbers (see attachment) and could merge any of them into
the distribution if there is a consensus that that should be done.
There is no need for "consensus" for Isabelle development, but a need for
a critical mass of people (1-3) who understand a certain module or part of
The Mercurial history is the first place to look:
It shows that Florian Haftmann has done the main work in putting and
keeping this in shape.
The history also shows exposes various "fixes" and other amendments. It is
important to check that there is no regression. In half-forgotten Isabelle
jargon, "new" means a failed attempt to do something old in a better way.
Just some formal notes on Isabelle/ML usage:
* Const names etc. should be always used with proper antiquotations;
lack of that is legacy (unmaintainable).
* Option.map is the only canonical operation from that structure,
everything else should be ignored.
This archive was generated by a fusion of
Pipermail (Mailman edition) and