Skip to content

The 'Explainable' codebase

The Explainable codebase includes the following components.

  • MathLang: a DSL for arithmetic expressions and predicates
  • Explainable: a monad for evaluating MathLang expressions and providing explanations for the (intermediate and final) results

These components of the Explainable codebase were intended to:

  • illustrate an evaluation-tree approach to logging computation for explainability purposes; and
  • provide a parallel implementation of infrastructure to support the insurance use case in 2023.

On 'MathLang'

To head off potential confusion right away: 'MathLang' can refer to several things:

  • some kind of functional programming based DSL
  • the specific embedded DSL Meng had created during the insurance usecase for his own experimentation and testing, and that was not wired up to the L4 codebase
  • the version of that that Inari and YM worked on, and that is wired up to the wider L4 codebase

These will be further explained in due course.

Historical Context

Let's start with: Why 'MathLang', when we already had the Logical English dialect? Recall that Meng did not like how the Logical English backend had been slow in its handling of requests, and that he had preferred a more functional approach to encoding contracts.

During the insurance usecase, Meng had written an embedded DSL, and wanted that to be further developed (hence the work that Inari and YM did). In particular, he wanted something like that that could compute things and give traces for its computations, and crucially, do it fast.

While the primary codepaths for the insurance use case ran with L4 and Logical English, this Explainable codebase allowed Meng to experiment with alternative formulations, and to do "cleanroom testing" of the primary codebase.

Interestingly, this codebase features twin implementations in Haskell and Typescript, with working runtimes in both languages.

We wanted a Typescript runtime so that the computations could run in the end-user's browser.

See also:

Links to Meng's embedded DSL:

That embedded DSL should give you some sense for what Meng has in mind with his 'MathLang'.

Use

In 2023, the "business logic" of the use case was independently encoded in Haskell and then pretty-printed to Typescript for evaluation.


graph TB;

    classDef tsruntime fill:#9ff,stroke:#333;

    A1["ToMathLang.hs\n(usecases/sect10-haskell/src/)"]

    A1 -- "imports" --> B;
    B["Explainable/MathLang.hs"]

    A1 -- "defines" --> A2["user-space decision logic\n(in internal DSL)"]

    A2 -- "has type" --> A3["Explainable.MathLang.Expr"];

    A3 -- "can be natively evaluated by" -->B

    B -- "pretty-prints Exprs to" -->C["Typescript output\n(sect10-typescript/src/\npau.ts)"]

    C -- "imports" -->D["mathlang.ts\n(sect10-typescript/src/\nmathlang.ts)"]

    F["The Abstract MathLang Language"]
    D -- "implements\nin Typescript" -->F
    B -- "implements\nin Haskell"    -->F

    C -- "imported by" -->G["crunch.ts\n(sect10-typescript/src/crunch.ts)"]

    G -- "outputs to" -->H["sect10-typescript/\ntests/\ndot/"]

    class C,G,H,D tsruntime

All the above is orchestrated by a Makefile under sect10-typescript.

Note that the business logic was independently encoded in the internal MathLang DSL and was not wired up to read from the Natural4 spreadsheets. As a clean-room re-implementation, that's fine, but in the long run, the DRY principle suggests that future MathLang toolchains should read from the spreadsheet or whatever natural4 encoding is canonical, rather than a reimplementation in ToMathLang.hs.

(YM's note: the above discussion is about Meng's 'internal MathLang DSL' (i.e., his embedded DSL). This is different from the MathLang codebase that Inari and YM had worked on. The latter does work off the output from the Natural L4 parser.)

'Generic MathLang' vs 'MathLang'

The term 'MathLang' is used in a couple of different ways. On the broadest sense, MathLang is supposed to be some kind of functional programming language. But there are also more specific senses; for example, it could also refer to the specific embedded DSL Meng had whipped up (see above) --- a DSL that departs from a more 'generic' / 'undergrad-textbook' functional programming language in some ways that make the translation to it more effortful.

It is in this context that 'Generic MathLang' should be understood. Because the specific embedded-in-Haskell DSL that Meng had whipped up was

  1. was written in a way that was hard to understand (I think Joe has been working on improving the code quality, though) and

  2. departs from a more 'generic' / 'undergrad-textbook' functional programming language in some ways that make the translation to it more effortful --- indeed, unnecessarily effortful, given the ostensible mandate ('get some kind of lambda calculus based thing out asap')

YM decided to first translate the output from the Natural L4 parser to an intermediate representation that he called Generic MathLang --- an intermediate representation that amounted to more generic, untyped lambda-calculus-looking AST --- before further translating it to other formats. That is, the envisioned pipeline was something like

Natural L4 parser => Generic MathLang => (e.g.) serialization of Generic MathLang for an in-browser interpreter | Meng's MathLang | ...etc

Doing this allows us, not only to (in principle) get a lot more quickly to a working web form backed by an in-browser interpreter (because, again, serializing Generic MathLang and then writing an in-browser interpreter with tracing would be a lot faster than having to read and test Meng's code carefully), but also improves code reuse, since we now have a lambda-calculus-y intermediate representation that we can work from if we need to experiment with producing other MathLang variants.

YM had started implementing this over Dec 2023 - Jan 2024, but subsequently passed the baton on to Inari.

This was admittedly YM's own understanding of Generic MathLang, but YM sees that Inari seems to also have stuck to this understanding of Generic MathLang; see her docs on the Generic MathLang codebase.

Meng's diagram of the architecture

graph TB;
    A1["Google Sheets tab\n(via API)"] -- "L4/Refresh" --> C;
    A2["command-line invocation\n(perhaps involving fswatch)"] -- calls --> C;
    classDef highlight fill:#f9f,stroke:#333,stroke-width:2px;

    subgraph C ["natural4-exe (app/Main.hs)"]
        Parser --> Interpreter;
    end

    C --"runs"--> C1["the Generic MathLang codebase\n(2024)"];

    C1--"imports"-->D[["LS/XPile/MathLang"]];
    C1--"imports"-->F

    D--"transpiles to"-->E[("workdir/uuid/\nmathlangGen\nmathlangTS")];
    class C1,D,E highlight;

    classDef tsruntime fill:#9ff,stroke:#333;

    E--"hopefully somehow\nbackward-compatible with"-->F["Explainable/MathLang.hs"];

    F --"which takes it the rest of the way to"-->G["the Typescript runtime"]
 class F,G tsruntime

Types

type ExplainableIO  r st a = RWST         (HistoryPath,r) [String] st IO (a,XP)
type Explainable    r st a = ExplainableIO r st a

Evaluation

See the Explainable README.