MMT as a parser framework for Scala APIs

[florian-rabe]

@Jazzpirate @jbetzend @kohlhase

This is not urgent but a nice new feature that could be seriously useful for external people. It could be a good student project.

This is inspired by recent work by Jansson et al, which do the same ad hoc and for a limited type theory in Haskell. There is a paper on it, possibly forthcoming.

Consider any Scala API (not necessarily MMT-related). We want to automatically parse strings into it in a safe way.

We can do that as follows:

• Write the API as an MMT theory.
• Tag every MMT constant with the qualified name of the Scala class/method that implements it.
• Have an MMT component that
  1. parses, type-checks, simplifies strings as usual.
  2. turns the resulting term into a Scala object by replacing every constant with the ascribed Scala operator. (Some reflection may be needed.)

[florian-rabe]

It would be even better if the MMT theory weren't needed at all.

Instead, the programmer could annotate the Scala classes/methods that should be exposed. The new MMT component could collect the annotated declarations and build the theory in memory.