Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)




Exactly. Over 10 years I have given many talks and written many papers about
Isabelle/Scala in contrast to Isabelle/ML. The main idea:

  * Isabelle/Scala is for systems-programming / system integration

  * Isabelle/ML is for mathematical logic

Sometimes there is a bit of overlap, and some freedom to decide where things
happen. But when you start to do term operations in Isabelle/Scala it is
probably wrong.

Good. Then I got things right. So we have a clear separation of purposes between Isabelle/Scala and scala-isabelle.

Anythings that can be done in scala-isabelle can also be done in Isabelle/ML, of course. (And vice versa.) However, if due to the constraints of the project, we want to use Scala (or any other JVM language), then scala-isabelle would be the right choice.

For example, in scala-isabelle, you can directly and transparently work on
terms, cterms, thms, etc. (For example, I can do something like
"thm.proposition match { case Const("HOL.Trueprop", t) => do something with
term t }". (And references on the scala side to Isabelle values can get
automatically garbage collected etc.)
So why not do this in Isabelle/ML? It works much better. E.g. you have proper
antiquotations for the const name "HOL.Trueprop" above --- without that it is
not going to last very long.

There can be several reasons (it depends on the project):

About the antiquotation: This was just an illustrative example. You can also use antiquotations in Scala, so you could write something like term match { case term"?x ==> Trueprop ?y" => print(x); print(y) }.

Why give up static scopes and types by pretending that ML operations can
happen in Scala?

Since Scala has a rich type system on its own, there is no need to give up on those things. ML types can be mirrored on the Scala side.

Best wishes,
Dominique.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.