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 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 system.

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).

  * 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 MHonArc.