IsarMathLib 1.23.0: Rewrite of the presentation layer in F#

I wrote the original isar2html tool 13 years ago in Haskell as a way to learn the language. Since then I was extending it and fixing bugs. Coming back once or twice a year to a language that I was not using professionally had quite a bit of overhead just to recall how the things worked and reconstruct the development environment. As it happened I changed jobs in April this year and the new job required F#, so I decided to rewrite isar2html in F#, again as a way to learn the language. Of course as usual with that type of “big rewrite” (well, not that big here really) projects I underestimated the effort needed so I finished only about a week ago. Now I have exactly the same application implemented the same way in Haskell i F#.

Basic verbosity statistics

The F# syntax is not as clean as Haskell’s so it was a surprise for me that the number of lines required was about 16% less in F# than in Haskell. Still, I would say that F# is slightly more verbose as the total number of characters was 10% higher in F#. Translating the parser of the subset of the Isar formal proof language that is used in IsarMathLib was almost mechanical and boring thanks to FParsec, which is the F# clone of Haskell’s Parsec parser library. I am especially happy with the result of that part of the project – the parsing errors were difficult to debug in Haskell. FParsec has better diagnostics built in – in case of failure it shows the backtracking information which helps a lot to pinpoint the problem in the text being parsed.

On the mathematics side in this release I have added a theorem stating that an ordered loop valued metric space is T2.

I was looking for an interesting example of an ordered loop and I found that nonzero octonions with multiplication form a loop. Octonions are octets of real numbers with naturally defined addition and somewhat less naturally defined multiplication. John Baez, in his excellent exposition characterized octonions as “the crazy old uncle nobody lets out of the attic”. Octonions have applications in physics, although some people think it’s all just hype. I think about them as the next step in the progression real numbers \longrightarrow complex numbers \longrightarrow quaternions. When we go from complex numbers to quaternions we loose commutativity of multiplication, when we go from quaternions to octonions we loose associativity. This makes nonzero octonions a proper loop, more specifically a Moufang loop. To get an ordered loop we can define the partial order on nonzero octonions by setting o_1 \preceq o_2 iff o_1=o_2 \vee \| o_1 \| < \| o_2\| or perhaps o_1=o_2 \vee \| o_1 \| > \| o_2\| if one wants to have the set of the positive element inside of the unit ball.


Tags: , , ,

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: