Hi! If you aren’t a L4 internal developer, or if you aren’t already familiar with L4, you might want to look at LegalSS first. This documentation is primarily intended for core devs – programmers working on the compiler toolchain and IDE for L4 itself.
The L4 language family currently comprises:
The syntax uses a plethora of English keywords arranged in a sentence-like structure, similar to languages like SQL.
The current IDE is a spreadsheet environment. In the future, we may add support for text-mode IDEs if there is demand.
The compiler consists of a parser, interpreter, and transpiler to a variety of downstream targets.
Please see https://github.com/smucclaw/baby-l4 and the L4 Language Report.
L4 transpiles to the following targets. An L4 “program” can be exported to these formats:
| Target | Purpose | Status (Dec 2022) |
|---|---|---|
| Purescript | decision logic | stable |
| Haskell | expose AST & IR internals | stable |
| Org-Mode | expose AST & IR internals | stable |
| Epilog | decision logic | early release |
| ASP (Answer Set Programming) | abduction | early release |
| Markdown | human readability | early release |
| Petri Nets | workflows and verification | early release |
| Typescript | data schema as class types | early release |
| JSON | instance data values | early release |
| Prolog | decision logic | in progress |
| Pro B | formal verification | in progress |
| DMN | decision logic | in progress |
| mCRL2 | formal verification | evaluation |
| Uppaal | formal verification | evaluation |
| Tapaal | formal verification | evaluation |
| BPMN | workflows for execution | on roadmap |
| DocAssemble | document assembly | on roadmap |
| Catala | decision logic | on roadmap |
| Blawx | decision logic, ontology | on roadmap |
| MorphIR | decision logic, ontology | on roadmap |
| Word | human readability | on roadmap |
| human readability, signing | on roadmap | |
| LegalDocumentML | standards-based interop | on roadmap |
| Alloy | formal verification | on roadmap |
After a successful run of the natural4 interpreter you will find exports udner the workdir directory.
LegalSS contains examples of L4 “source code”.
L4 developers – the legal engineers working with L4 source code to build legal infrastructure and applications – are supported by a sidebar in the spreadsheet that displays warnings, errors, and exported files.
That sidebar is generated by the L4 toolchain, which makes sense of L4 source code from the spreadsheet.
That L4 toolchain is, in turn, supported by the L4 internal developer community. We also refer to internal developers as core developers.
Operating instructions for the parts of the toolchain that bring up a web-based development environment (Google Sheets) and web application (end-user-facing Vue app) are available at https://docs.google.com/document/d/1EvyiQhSgapumBRt9UloRpwiRcgVhF-m65FVdAz3chfs/edit
The rest of this documentation introduces the logic and semantics of natural4, its internal data structures, and its surface syntax.
Along the way it discusses the internal structure of our compiler codebase.
- Clone this repository.
- (For Nix users only:) You will have your own setup universe which we won’t go into here, but if you use Nix you already probably have Haskell well in hand. You are using Nix if your
$PATHcontains$HOME/.nix-profile/bin/ - If you’re not a Nix user, install GHCup.
- After installing GHCup, your
$PATHshould contain$HOME/.ghcup/bin/ - Use GHCup to install Stack by running
ghcup tui. - After installing Stack, your
$PATHshould contain$HOME/.local/bin/ - For VS Code and emacs users: use GHCup to install HLS by manually running
ghcup compile hls --git-ref master --ghc 9.2.5 --cabal-update - For Emacs users: proceed to the instructions at lsp-haskell.
- For VS Code users: proceed to the instructions at vscode-haskell.
After your Haskell setup is working well enough to run stack,
src/smucclaw/dsl$ cd lib/haskell/natural4 natural4$ stack test
It may take some time to compile ghc, plus a whole raft of dependencies.
A number of sample CSV inputs can be found in the test/examples directory.
(The following should be run from the lib/haskell/natural4 subdirectory.)
natural4$ stack run -- --workdir=workdir --toasp --tomd test/examples/mustsing-latest.csv
This should compile the l4 parser, and produce a bunch of output under the workdir/ directory.
You can browse that output using any text editor or filesystem explorer.
If you’re happy with the above output,
natural4$ stack installwill put a natural4-exe somewhere in your $HOME/.local/bin directory. After the above installation procedure, that directory should appear in your $PATH.
natural4$ stack haddockwill generate Haddock documentation from the Haskell source. The output takes the form of .html files; pay attention to the last dozen lines or so of the stack haddock run output to get the actual pathnames.
The typical user drafts an L4 program in a spreadsheet.
That program can be downloaded as a CSV, which this toolchain consumes.
Example: Go to the “Case Study: PDPA DBNO” tab in LegalSS, and click File/ Download / as CSV.
The downloaded filename will probably be quite long. For the sake of concision, we will call it pdpadbno.csv
Is there some other way to obtain the same CSV using only the command line? Yes. If you just want to use the stock CSV, you can do
wget -O pdpadbno.csv 'https://docs.google.com/spreadsheets/d/e/2PACX-1vSbknuGFkvvk_Pv9e97iDW9BInxd-Cj27-xC8d_SwveP1PxERV7ZmiAIU7PWXas2CEMH2bl8PyyD6X3/pub?gid=0&single=true&output=csv'
Otherwise, if you want to make your own changes and get the resulting spreadsheet in CSV form, you should make a copy (File > Make a Copy in Google Sheets), if you haven’t already, and make your changes in that copy. Then, to get the URL for wget, click on File / Share / Publish to web, choose the appropriate tab under ‘Link’ and select CSV as the output format under ‘Embed’, and finally click on Publish. You will then be presented with a URL; this URL is what should replace that in the wget eaxmple block above.
Is this more or less the same file as what’s already present in test/casestudypdpadbno-latest.csv? Yes, it is. But now you know how to get a copy fresh from any edits you make.
The job of a compiler / transpiler / parser / interpreter toolchain is to transform user code to some useful target representation.
We’ll first want to output all the target representations to disk. To do that, navigate to dsl/lib/haskell/natural4 and run
$ stack run -- --workdir=workdir --toasp --tomd pdpadbno.csv
The result will be something like:
$ tree workdir
workdir
└── no-uuid
├── aasvg
│ ├── 2022-12-01T08:56:17.579Z
│ │ ├── Assessment-anyall.hs
│ │ ├── Assessment-anyall.json
│ │ ├── Assessment-full.svg
│ │ ├── Assessment-qjson.json
│ │ ├── Assessment-qtree.hs
│ │ ├── Assessment-tiny.svg
│ │ ├── Notify_Individuals-N-anyall.hs
│ │ ├── Notify_Individuals-N-anyall.json
│ │ ├── Notify_Individuals-N-full.svg
│ │ ├── Notify_Individuals-N-qjson.json
│ │ ├── Notify_Individuals-N-qtree.hs
│ │ ├── Notify_Individuals-N-tiny.svg
│ │ └── index.html
│ ├── 2022-12-07T10:01:07.764Z
│ │ ├── Assessment-anyall.hs
│ │ ├── Assessment-anyall.json
│ │ ├── Assessment-full.svg
│ │ ├── Assessment-qjson.json
│ │ ├── Assessment-qtree.hs
│ │ ├── Assessment-tiny.svg
│ │ ├── Notify_Individuals-N-anyall.hs
│ │ ├── Notify_Individuals-N-anyall.json
│ │ ├── Notify_Individuals-N-full.svg
│ │ ├── Notify_Individuals-N-qjson.json
│ │ ├── Notify_Individuals-N-qtree.hs
│ │ ├── Notify_Individuals-N-tiny.svg
│ │ └── index.html
│ └── LATEST -> 2022-12-07T10:01:07.764Z
├── asp
│ ├── 2022-12-01T08:55:44.907Z.lp
│ └── 2022-12-07T09:35:17.752Z.lp
├── babyl4
│ ├── 2022-12-07T10:01:07.764Z.l4
│ └── LATEST.l4 -> 2022-12-07T10:01:07.764Z.l4
├── corel4
│ ├── 2022-12-07T10:01:07.764Z.l4
│ └── LATEST.l4 -> 2022-12-07T10:01:07.764Z.l4
├── grounds
│ ├── 2022-12-07T10:01:07.764Z.txt
│ └── LATEST.txt -> 2022-12-07T10:01:07.764Z.txt
├── json
│ ├── 2022-12-07T10:01:07.764Z.json
│ └── LATEST.json -> 2022-12-07T10:01:07.764Z.json
├── native
│ ├── 2022-12-07T10:01:07.764Z.hs
│ └── LATEST.hs -> 2022-12-07T10:01:07.764Z.hs
├── natlang
│ ├── 2022-12-07T10:01:07.764Z.txt
│ └── LATEST.txt -> 2022-12-07T10:01:07.764Z.txt
├── org
│ ├── 2022-12-07T10:01:07.764Z.org
│ └── LATEST.org -> 2022-12-07T10:01:07.764Z.org
├── petri
│ ├── 2022-12-07T10:01:07.764Z.dot
│ └── LATEST.dot -> 2022-12-07T10:01:07.764Z.dot
├── prolog
│ ├── 2022-12-07T10:01:07.764Z.pl
│ └── LATEST.pl -> 2022-12-07T10:01:07.764Z.pl
├── purs
│ ├── 2022-12-07T10:01:07.764Z.purs
│ └── LATEST.purs -> 2022-12-07T10:01:07.764Z.purs
└── ts
├── 2022-12-07T10:01:07.764Z.ts
└── LATEST.ts -> 2022-12-07T10:01:07.764Z.ts
These outputs correspond to the transpilation targets enumerated above, and can be further transformed if necessary before being put in front of the end-user’s eyeballs.
The above run disabled two of the output targets because they are still works in progress: --toasp --tomd
You can remove those options from the command line to enable those output channels, but they may not work.
The initial AST produced by the natural4 parser is found in the native/ output directory as LATEST.hs.
Subsequently, that AST is transformed by the Interpreter module to a data structure output to the org/ output directory as LATEST.org.
From there, it is further transformed to an intermediate representation called CoreL4, also known as Baby L4. That transformation is currently under renovation: there is a plaintext code generator which is slightly older, and a slightly newer initiative to perform direct in-memory conversion from one set of types to another. In our defense, this high-level/low-level dichotomy is also present in GHC; and the old/new pair of transformation pathways also appears in GHC’s history.
This is the simplest output mode. It confirms the parse happened as intended.
You should see a LATEST.hs file under the workdir/*/native/ output directory. You can get just that output by running
natural4$ stack run -- --only native test/casestudypdpadbno-latest.csv
This should produce a screenful of output. If all went well, the output will be in the format of a Haskell data structure, containing the rules that have been parsed. It will look something like this:
[ Regulative
{ every = "Person"
, who = Just
( All
( Pre "Who" )
[ Leaf "walks"
, Any
( Pre "any of:" )
[ Leaf "eats"
, Leaf "drinks"
]
]
)
, cond = Nothing
, deontic = DMust
, action =
( "sing"
, []
)
, temporal = Nothing
, hence = Nothing
, lest = Nothing
, rlabel = Nothing
, lsource = Nothing
, srcref = Nothing
, upon = Nothing
, given = Nothing
}
]
[ Regulative
{ every = "Person"
, who = Just
( All
( Pre "Who" )
[ Leaf "walks"
, Any
( Pre "any of:" )
[ Leaf "eats"
, Leaf "drinks"
]
]
)
, cond = Nothing
, deontic = DMust
, action =
( "sing"
, []
)
, temporal = Nothing
, hence = Nothing
, lest = Nothing
, rlabel = Nothing
, lsource = Nothing
, srcref = Nothing
, upon = Nothing
, given = Nothing
}
]
[ Constitutive
{ term = "The rule-level checkbox is checked"
, cond = Just
( Any
( Pre "any of:" )
[ Leaf "the conditions do not hold"
, All
( Pre "all of:" )
[ Leaf "the conditions do hold"
, Leaf "the action is satisfied"
]
]
)
, rlabel = Nothing
, lsource = Nothing
, srcref = Nothing
}
]
[ Regulative
{ every = "Person"
, who = Just
( Leaf "Qualifies" )
, cond = Nothing
, deontic = DMust
, action =
( "sing"
, []
)
, temporal = Nothing
, hence = Nothing
, lest = Nothing
, rlabel = Nothing
, lsource = Nothing
, srcref = Nothing
, upon = Nothing
, given = Nothing
}
, Constitutive
{ term = "Qualifies"
, cond = Just
( All
( Pre "all of:" )
[ Leaf "walks"
, Any
( Pre "any of:" )
[ Leaf "eats"
, Leaf "drinks"
]
]
)
, rlabel = Nothing
, lsource = Nothing
, srcref = Nothing
}
]The semantics of this data structure will be outlined below. This outline complements other documentation:
- Haddock documentation for the LS.* modules (produced by the *Generate Haddock documentation procedure above
- the L4 Manual tab of the LegalSS
- the operating instructions Google Doc
The following documentation focuses on the parsing and interpretation aspects of the toolchain and the data structures in particular.
The interpreter performs a number of transformations. For your convenience it writes each stage of those transformations out to the org/LATEST.org output file, in a format compatible with org-mode.
If you are an Emacs user, you have native support for org-mode built in; opening the LATEST.org output file should automatically load org-mode.
If you are a VS Code user you will need to install the relevant extensions.
This is a formally rigorous language representing decision logic, ontology, and workflow rules.
This is where some of the type-checking and type inference occurs.
Some of the downstream targets are produced by transpilers which proceed from CoreL4.
For details, please see https://github.com/smucclaw/baby-l4 and the L4 Language Report.
This section is still under construction. It will give a short explanation of each transpilation target and its intended use.
Those elements of L4 which correspond to first-order logic can be transpiled to a Prolog-like syntax.
The inspiration is The British Nationality Act as a Logic Program. In principle it should be possible to express the British Nationality Act as an L4 program, from which we can extract a Prolog program.
We usually see decision-related reasoning in the context of constitutive rules: an X counts as a Y if Z holds. In the trivial case, an X counts as true if Z holds:
constitutiveRule(X) :- Z.
bna(isBritishCitizen,X) :- bna(isBritishCitizen,Y), parent(Y, X).The reasoning used is backward-chaining deduction. Given a goal statement, the task is to decide if that goal is true or false. “It depends.” What does it depend on? We work through all the dependencies, backtracking, until the goal can be proven true – or false.
Prolog’s other great strength – abductive reasoning through unification – does not arise in our current swipl implementation. We do want to use this feature for planning problems, in the future.
Our current transpilation pathway to Prolog actually runs through the CoreL4 language. It is possible that in future we will go direct from Natural4.
Within the Prolog family of targets we differentiate:
One of the workdir outputs is a Petri (workflow) net in GraphViz dot format. This is like a state diagram.
To convert it to an SVG which can be opened in a web browser, you will need GraphViz installed. Then run
dot -Tsvg workdir/no-uuid/petri/LATEST.dot > workdir/no-uuid/petri/LATEST.svg
It is not exactly a state diagram because things can be in multiple sub-states at once. Petri Nets are good at showing that.
This is consumed by the Vue web application documented in the Operating Instructions Google Doc.
If you know Haskell, you will be able to read Purescript.
Sometimes, a downloaded CSV may not agree with the parser.
If a parse error occurs, you can enable debugging by adding --dbug to the command line. An alternative way to enable debugging is to set the environment variable MP_DEBUG=True.
Debugging output is super verbose. We process it with the following idiom:
filename=casestudypdpadbno-latest; MP_DEBUG=True stack run test/$filename.csv |& bin/debug2org > out/$filename.org
The debug2org script rewrites the raw debugging output into a format which is more easily viewed in Emacs org-mode. Mostly, it’s about folding: the parser’s output is organized to reflect its attempts to parse various expressions. Most of those parse attempts are “desired failures” and are not of interest; org-mode lets you hide them by pressing TAB.
Making sense of the parser debug output requires some familiarity with programming language theory, with compiler theory, and with the specifics of our L4 parser toolchain.
This little script (on Mac at least) watches your Downloads folder so every time you Save As CSV it moves the new download over to the test/ directory. Run from home directory. You may need to edit to taste.
fswatch -x ~/Downloads/ | perl -nle 'if (my ($fn, $target) = /(Legal(?:SSv| Spreadsheets - )(.*).csv) Created.*Renamed/) { for ($target) { $_ = lc $_; s/[^a-z]//g }; rename (qq(Downloads/$fn), qq(src/smucclaw/dsl/lib/haskell/natural4/test/$target-latest.csv)) && print(qq($fn -> $target)) && system(qq(cd src/smucclaw/dsl/lib/haskell/natural4; teedate=`date +%Y%m%d-%H%M%S`.txt; stack run -- --workdir=workdir test/$target-latest.csv > workdir/no-uuid/\$teedate; ln -sf \$teedate workdir/no-uuid/LATEST.txt; head \$teedate; echo done ))} BEGIN { $|++ }'
We should probably turn this into an actual shell script, not a command-line “one-liner”.
The parser consumes CSV and produces a list of rules largely corresponding to the input.
Along the way, some “inline” rules are promoted to top-level.
In some positions, a term can be assigned a default value using the TYPICALLY keyword.
Such uses result in a top-level rule: DefTypically.
Suppose we have
EVERY Person
WHO Qualifies
MEANS walks
AND eats
OR drinks
MUST sing
(This is from the Waddington example.)
This parses to two top-level rules:
- a regulative rule
EVERY person WHO Qualifies MUST sing. - a constitutive rule
Qualifies MEANS walks AND eats OR drinks.
This promotion is accomplished thanks to the Monad Writer context of the Natural L4 Parser.
https://github.com/smucclaw/dsl/blob/main/lib/haskell/natural4/src/LS/Types.hs#L151-L152
The Interpreter conducts multiple passes over the Parser’s AST.
The following passes are on the roadmap for the Interpreter.
Let’s declare as a Class anything that has attributes and instances.
How do we deal with subclasses, inheritance, and diamonds?
Subclasses are constructed using the EXTENDS keyword.
HAS-A relationships are dealt with using nesting of the HAS keyword.
Diamond inheritance is excluded.
Construct trees of ANDs and ORs. How do we deal with a particular defined term appearing in multiple locations?
E.g. given a shopping cart with both alcohol and cigarettes, a LegalCheckout may refer to the “subroutine” for AgeOfMajority twice; do we need to “cache” to result of evaluation, or is that a problem for the runtimes? Perhaps we can assist by at least giving identifiers so the runtime can do the right thing.
The AnyAll library is responsible for most of this work.
The result of this transformation stage is visible in the qaHornsR and qaHornsT functions.
If the language has support for user-defined macros or other forms of syntactic sugar, evaluate those macros and desugar to canonical form.
Filter all instances of TypedMulti in our AST where the snd is Just; collect the explicit type annotations.
Filter all instances of TypedMulti in our AST where the snd is Nothing; attempt type inference based on observations of how the fst element is used elsewhere. For top marks, Implement Hindley-Milner inference.
This work may be delegated to the Core L4.
Alternatively, we may be able to call GHC as a library.
After the parser succeeds, we have in our hands a list of Rules.
It is now the interpreter’s job to think about the Rules, get organized, and prepare for the next step – transpilation.
The transpilers will be wanting answers to questions like:
The DECLARE and DEFINE keywords together construct class and instance definitions.
We need to find a way to relate different entities with one another – an Employee may have an Employer. In a database, they may be connected explicitly by id fields or they may be connected implicitly.
In our system, we allow DECLARE / HAS to nest, so that multiple levels of nesting can be created. This is analogous to records containing other records, and to HAS-A relationships between classes.
The TypedMulti alias looks like this:
type KVsPair = (NonEmpty Text.Text, Maybe TypeSig) --- so really there are multiple Values
type TypedMulti = KVsPair --- | apple | orange | banana | :: | Fruit |The Maybe TypeSig part can be used for both explicitly annotated types and inferred types.
In particular, the interpreter might be able to perform tree-shaking, dead code identification, and identify null pointer references.
It might also be able to identify race conditions. Maybe one transpiler can request to view the output of another transpiler backend, so the formal verification module ends up running first and then the other transpilers read output from that.
The Parser produces decent source locations, but the transformations performed by the Interpreter may muddy the trail.
If not, then for each node in the AST, can we at least get a link back to a source reference in the original program text?
And even beyond – because in the left column of L4 we have the (Act 1.2) cells which provide links even farther back to the source legislation.
The interpreter needs to get its head around how all the BoolStructs go together.
Our NLG component, for instance, needs to convert text like X gives birth to live young. to Does X give birth to live young?
So it will want to know every single “ground term” which we need to ask the user about.
The Shannon/Allen visualizer and the JSON outputters will want to know how those terms fit together: the BoolStructs with their Labels.
The web app interface builder may expect the interpreter to do some kind of reduction/optimization of the questions – see ROBDD.
This is of particular interest to the visualizer that produces a Petri net.
The interpreter needs to get its head around how all the HENCE and LEST blocks connect.
We are literally looking at capitalization to determine what’s a Defined Term.
Each transpiler under XPile can expect an Interpretation containing the interpreter’s analysis of the rules.
That analysis consists of
- classtable
- of type
ClsTab, a table of all the top-level classes declared - scopetable
- of type
ScopeTabs, a table of all the rule scopes defined
That Interpretation also contains
- origrules
- a list of rules (
[Rule]) as returned by the Parser
See Haddock reference.
Classes contain ontological semantics according to the conventional OOP paradigm, excluding diamond inheritance.
Classes can contain other classes, in a HAS-A relationship, using nested HAS keywords.
Classes can extend other classes, in an IS-A relationship, using the EXTENDS keyword.
Scopes in L4 are intended to constrain certain definitions, reflecting source text such as
For the purposes of Sections 1 and 2, “work-week” is defined to include half a day on Saturdays, in addition to Mondays through Fridays, but excludes Sundays.
For the purposes of Sections 3 and 4, “work-week” is defined to exclude Saturdays and Sundays.
Scopes allow us to represent these kinds of statements.
See Haddock reference.
See the LegalSS L4 Manual.