l4

L4 — Programming Language for Law

Overview

L4 is a statically-typed functional programming language for computational law, inspired by Haskell. It enables legal professionals and developers to encode contracts, regulations, and policies as executable, testable, verifiable programs. L4 bridges the gap between human-readable legal text and machine-executable logic.

Cloud Validation Available: This skill includes a cloud-based validator that connects to wss://jl4.legalese.com/lsp, allowing you to validate L4 code without installing the Haskell toolchain locally. See Section 5 for details.

Core Workflow

When working with L4, follow this systematic approach:

1. Analyze Source Material

When given natural language legal text (PDFs, URLs, legislation):

• Identify the domain ontology: What entities, statuses, and categories exist? (Often unstated in source documents—use world knowledge)
• Extract decision logic: What are the business rules and conditions?
• Map state transitions: What obligations, deadlines, and modalities govern parties over time?

2. Model the Domain (Types)

Use DECLARE to define the type system:

-- Enums: Fixed sets of values
DECLARE RiskCategory IS ONE OF
    LowRisk
    MediumRisk
    HighRisk
    Uninsurable

-- Records: Types with named fields
DECLARE Driver HAS
    name            IS A STRING
    age             IS A NUMBER
    yearsLicensed   IS A NUMBER
    accidentCount   IS A NUMBER
    hasTickets      IS A BOOLEAN

Isomorphic encoding principle: Match the structure of the source text. If legal text has sections 1.1, 1.2, 1.3, your L4 code should reflect that hierarchy with corresponding logical structure (ANDs/ORs forming the same tree).

3. Encode Decision Logic

Use GIVEN/GIVETH/MEANS for functions, DECIDE ... IF for rules:

-- Simple decision rule
GIVEN driver IS A Driver
GIVETH A BOOLEAN
DECIDE `meets minimum age` IF
    driver's age AT LEAST 18

-- Pattern matching with CONSIDER
GIVEN driver IS A Driver
GIVETH A RiskCategory
`assess risk` driver MEANS
    CONSIDER driver's accidentCount
    WHEN 0 THEN
        IF driver's hasTickets
        THEN MediumRisk
        ELSE LowRisk
    WHEN 1 THEN MediumRisk
    WHEN 2 THEN HighRisk
    OTHERWISE Uninsurable

4. Model State Transitions and Obligations (Advanced)

For multi-party contracts with obligations, deadlines, and state transitions, L4 provides regulative rule syntax. This is essential for contracts like promissory notes, loan agreements, and service contracts.

Key Concepts: Traces, Blame, and Reparation

L4's regulative rules are grounded in formal contract semantics (based on research by Tom Hvitved; see Contract Formalisation and Modular Implementation of Domain-Specific Languages, PhD thesis, IT University of Copenhagen).

• Traces: A contract execution is a sequence of timestamped events (actions by parties). Use #TRACE to simulate.
• Blame assignment: Every breach identifies which party failed to meet their obligation.
• Reparation: Missing a primary deadline (violation) can be recovered via LEST clauses; only unrecovered violations become breaches.

The Obligation Pattern

Regulative rules govern party behavior over time:

PARTY   actor
WHO     preconditions      -- Optional: who can perform this action
MUST    action            -- Or MAY
        parameters        -- Details of the action
WITHIN  deadline          -- Deadline in days (number)
HENCE   nextState         -- What happens if fulfilled
LEST    penaltyState      -- What happens if breached (reparation clause)

Key insight: Without a LEST clause, missing the deadline causes immediate breach. With LEST, the party gets a chance to make reparations.

Action Constraints: EXACTLY and PROVIDED

Actions can be constrained in two ways:

EXACTLY — The action must match a specific value:

MUST `pay to` EXACTLY `The Lender`   -- Must be exactly this lender, no substitutes

PROVIDED — The action must satisfy a predicate:

MUST `pay amount`
     `Amount Transferred` PROVIDED
         `Amount Transferred` AT LEAST `Minimum Payment`

Example: Loan Payment with Reparation

GIVEN outstandingAmount IS A Money
PARTY `The Borrower`
MUST  `pay debts to` EXACTLY `The Lender`
      `Amount Transferred` PROVIDED
          `Amount Transferred` AT LEAST outstandingAmount
WITHIN `Payment Due Date`
HENCE  FULFILLED
LEST   PARTY `The Borrower`                    -- Reparation clause
       MUST  `pay debts to` EXACTLY `The Lender`
             `Amount Transferred` PROVIDED
                 `Amount Transferred` AT LEAST amountWithPenalty
       WITHIN defaultDeadline
       -- No LEST here: missing this deadline = breach
       WHERE
           amountWithPenalty MEANS
               Money WITH
                   Currency IS outstandingAmount's Currency
                   Value IS outstandingAmount's Value TIMES 1.05
           defaultDeadline MEANS `Payment Due Date` PLUS 30

Deontic Modals

Modal	Meaning	Notes
MUST	Obligatory	Missing deadline triggers LEST (or breach if no LEST)
MAY	Permitted	Party can choose to act or not; no penalty for inaction

Note: SHANT (prohibition) is not yet implemented. See Current Limitations below.

Recursive Obligations with HENCE

For recurring payments (like monthly installments), use recursive HENCE:

GIVEN remainingBalance IS A Money
`Payment Obligations` remainingBalance MEANS
    IF remainingBalance's Value GREATER THAN 0
    THEN PARTY `The Borrower`
         MUST `pay` `monthly payment`
         WITHIN `next due date`
         HENCE `Payment Obligations` newBalance
         LEST `Payment Obligations` penaltyBalance
         WHERE
             newBalance MEANS
                 Money WITH
                     Currency IS remainingBalance's Currency
                     Value IS remainingBalance's Value MINUS `monthly payment`'s Value
             penaltyBalance MEANS
                 Money WITH
                     Currency IS remainingBalance's Currency
                     Value IS remainingBalance's Value PLUS penalty
    ELSE FULFILLED

Testing Temporal Obligations with #TRACE

Use #TRACE to simulate contract execution with a sequence of events:

#TRACE <contract> <initial-args> AT Day <start-date> WITH
    PARTY <who> DOES <action> <args> AT Day <when>
    PARTY <who> DOES <action> <args> AT Day <when>
    ...

Happy path example (from promissory note):

#TRACE `Payment Obligations` `Total Repayment Amount` AT Day (February 4 2025) WITH
    PARTY `The Borrower` DOES `pay monthly installment to` `The Lender` (USD 2256.46) AT Day (March 4 2025)
    PARTY `The Borrower` DOES `pay monthly installment to` `The Lender` (USD 2256.46) AT Day (April 4 2025)
    -- ... all 12 payments on time

Result: FULFILLED — All obligations met.

Late payment example:

#TRACE `Payment Obligations` `Total Repayment Amount` AT Day (February 4 2025) WITH
    PARTY `The Borrower` DOES `pay monthly installment to` `The Lender` (USD 2256.46) AT Day (April 3 2025)

Result: Returns the residual obligation — what's still required:

PARTY `The Borrower`
MUST `pay monthly installment to` EXACTLY `The Lender`
     `Amount Transferred` PROVIDED ... `Next Payment Due Amount With Penalty`
WITHIN `Default After Days Beyond Commencement`
LEST ...

The trace shows the contract is now in the "penalty" state — borrower must pay with penalty or face default.

Contract Composition

Conjunction (AND) — Both obligations must be fulfilled:

`Complete Transaction` MEANS
    PARTY `Seller`
    MUST  `deliver goods`
    WITHIN 14
    AND
    PARTY `Buyer`
    MUST  `make payment`
    WITHIN 30

Disjunction (OR) — At least one must be fulfilled:

`Payment Options` MEANS
    PARTY `Buyer`
    MUST  `pay in full`
    WITHIN 30
    OR
    PARTY `Buyer`
    MUST  `pay first installment`
    WITHIN 30
    HENCE `Installment Schedule`

Note: For OR, L4 requires that the same party is blamed in both branches (deterministic blame).

For more details, see:

• Advanced Course Module A11: Regulative Rules
• jl4/examples/legal/promissory-note.l4

5. Validate with jl4-cli or Cloud Validation

Option A: Local validation (requires jl4-cli installation)

jl4-cli your-file.l4

Option B: Cloud validation (no installation required)

node l4/scripts/validate-cloud.mjs your-file.l4

The cloud validator connects to wss://jl4.legalese.com/lsp and provides the same validation as local jl4-cli, without requiring Haskell toolchain installation. This makes L4 validation accessible from any environment.

Options for cloud validation:

• --url <wss://...>: Use a different LSP server
• --debug: Show detailed protocol messages

Type errors will be reported with line numbers. Iterate until "checking successful".

6. Test with #EVAL and #ASSERT

-- Sample data
`Alice` MEANS Driver WITH
    name          IS "Alice"
    age           IS 25
    yearsLicensed IS 7
    accidentCount IS 0
    hasTickets    IS FALSE

-- Execute tests
#EVAL `meets minimum age` `Alice`
#EVAL `assess risk` `Alice`
#ASSERT `assess risk` `Alice` EQUALS LowRisk

7. Generate Outputs (Optional)

From L4 source, you can generate:

• Web applications (decision trees, forms)
• API services (for integration)
• Documentation (Markdown, PDF)
• Visualizations (ladder diagrams)

Essential L4 Syntax

File Structure

§ `Top-Level Section Title`
§§ `Subsection Title`

IMPORT prelude    -- Standard library
IMPORT daydate    -- Date arithmetic

-- Type declarations
DECLARE TypeName ...

-- Function definitions
GIVEN param IS A Type
GIVETH A ReturnType
functionName param MEANS ...

-- Test execution
#EVAL expression
#ASSERT boolean_expression

Type Declarations

-- Enum (closed set)
DECLARE Status IS ONE OF Value1, Value2, Value3

-- Enum with data (algebraic data type)
DECLARE Outcome IS ONE OF
    Success HAS value IS A NUMBER
    Failure HAS reason IS A STRING

-- Record (product type)
DECLARE Person HAS
    name IS A STRING
    age  IS A NUMBER

-- Lists
LIST a, b, c                 -- list literal
EMPTY                        -- empty list
x FOLLOWED BY xs             -- cons pattern

-- Optional values
MAYBE Type
JUST value                   -- has value
NOTHING                      -- no value

Function Definitions

-- Standard form
GIVEN param1 IS A Type1
      param2 IS A Type2
GIVETH A ReturnType
functionName param1 param2 MEANS expression

-- Mixfix notation (natural language syntax)
GIVEN employee IS AN Employee
      employer IS A Company
GIVETH A BOOLEAN
`employee` `works for` `employer` MEANS ...

-- Decision rules
DECIDE ruleName IF condition1 AND condition2

-- WHERE clauses (local helpers)
mainExpression
WHERE
    helper1 MEANS expression1
    helper2 MEANS expression2

Pattern Matching

-- CONSIDER/WHEN (like switch but type-safe)
CONSIDER value
WHEN Pattern1 THEN Result1
WHEN Pattern2 THEN Result2
OTHERWISE DefaultResult

-- With data extraction
CONSIDER outcome
WHEN Success WITH value THEN
    "Got: " APPEND (STRING value)
WHEN Failure WITH reason THEN
    "Error: " APPEND reason

-- List patterns
CONSIDER list
WHEN EMPTY THEN 0
WHEN x FOLLOWED BY xs THEN
    x PLUS (sum xs)

-- BRANCH (flat multi-way decisions)
BRANCH IF status EQUALS Active   THEN "Running"
       IF ^      EQUALS Inactive THEN "Stopped"
       OTHERWISE "Unknown"

Regulative Rules (State Transitions)

For multi-party contracts with obligations and deadlines:

-- Basic obligation
PARTY actorName
WHO   preconditions      -- Optional qualifier
MUST  action             -- Or MAY (MUST NOT not yet implemented)
      EXACTLY value      -- Must match exactly
      param PROVIDED p   -- Must satisfy predicate p
WITHIN deadline          -- Days (number)
HENCE nextObligation     -- If fulfilled
LEST  reparationClause   -- If deadline missed (violation recovery)

-- Recursive obligations (loans, subscriptions)
GIVEN state IS A StateType
obligationFunction state MEANS
    IF condition
    THEN PARTY actor
         MUST action
         WITHIN deadline
         HENCE obligationFunction newState
         LEST obligationFunction penaltyState
    ELSE FULFILLED

-- Composing obligations
obligation1 AND obligation2   -- Both must be fulfilled
obligation1 OR obligation2    -- At least one (same blame party)

-- Testing temporal behavior
#TRACE obligationFunction initialState AT Day startDate WITH
    PARTY actor DOES action args AT Day when
    PARTY actor DOES action args AT Day when

Key keywords:

• PARTY - Identifies the actor responsible (blamed if they fail)
• WHO - Preconditions for the party (optional)
• MUST / MAY - Deontic modals (obligatory / permitted)
• EXACTLY - Action must match specific value
• PROVIDED - Action must satisfy predicate
• WITHIN - Deadline in days
• HENCE - Next state if obligation fulfilled
• LEST - Reparation clause if deadline missed (no LEST = breach)
• FULFILLED - Terminal success state
• AND / OR - Compose obligations
• #TRACE - Test contract execution with event sequence

Operators

Boolean Logic:

condition1 AND condition2
condition1 OR condition2
NOT condition
IF cond THEN expr1 ELSE expr2

Comparisons:

x EQUALS y
x GREATER THAN y
x LESS THAN y
x AT LEAST y              -- >=
x AT MOST y               -- <=

Arithmetic:

x PLUS y                  -- +
x MINUS y                 -- -
x TIMES y                 -- *
x DIVIDED BY y            -- /
x MODULO y                -- %
SQRT x                    -- square root
x EXPONENT y  or  x ^ y   -- exponentiation

Strings:

STRINGLENGTH str          -- length
TOUPPER str               -- to uppercase
TOLOWER str               -- to lowercase
TRIM str                  -- remove whitespace
CONTAINS str substring    -- check contains
STARTSWITH str prefix     -- check starts with
ENDSWITH str suffix       -- check ends with
SPLIT str delimiter       -- split into list
SUBSTRING str start len   -- extract substring
REPLACE str old new       -- replace all
CHARAT str index          -- character at index
str1 APPEND str2          -- concatenate

Record Construction and Access

-- Construction
Person WITH
    name IS "Alice"
    age  IS 30

-- Field access
person's name
person's age

-- Chaining
application's employee's nationality

Common List Operations

map function list         -- apply function to each element
filter predicate list     -- keep elements matching predicate
fold function init list   -- reduce list to single value
any predicate list        -- TRUE if any element matches
all predicate list        -- TRUE if all elements match
`length of` list          -- count elements
at list index             -- get element at index

Best Practices

Isomorphic Encoding

Match the structure of source legal text:

Source text:

Section 1.2: Coverage applies if:
  (a) Damage is not caused by rodents, insects, vermin, or birds, and
  (b) Damage is to contents caused by birds, or
  (c) An animal causes water escape from appliance/pool/plumbing

L4 encoding (isomorphic structure):

DECIDE `coverage applies` IF
        NOT `caused by excluded pests` damage
    AND (   `bird damage to contents` damage
         OR `animal caused water escape` damage)

Type-Driven Development

1. Start with types (domain model)
2. Write function signatures
3. Implement function bodies
4. Add tests with #EVAL/#ASSERT
5. Validate with jl4-cli

Mixfix for Readability

Use mixfix notation to make code read like legal prose:

-- Instead of: eligible(employee, employer)
-- Write:
`employee` `eligible for work pass with` `employer`

Exhaustiveness

Always handle all cases in pattern matching. The compiler will warn about missing cases:

CONSIDER status
WHEN Active THEN "Running"
WHEN Inactive THEN "Stopped"
-- Add OTHERWISE or handle Suspended if it exists
OTHERWISE "Unknown"

Test Coverage

For each rule, provide:

• Positive test cases (rule holds)
• Negative test cases (rule fails)
• Edge cases (boundary conditions)

#ASSERT `is adult` (Person WITH age IS 18)
#ASSERT NOT `is adult` (Person WITH age IS 17)

Common Patterns

Decision Trees

GIVEN application IS A Application
GIVETH A String
`eligibility decision` application MEANS
    IF NOT `age requirement met`
    THEN "Rejected: Age"
    ELSE IF NOT `education requirement met`
    THEN "Rejected: Education"
    ELSE IF NOT `salary requirement met`
    THEN "Rejected: Salary"
    ELSE "Approved"
    WHERE
        `age requirement met` MEANS ...
        `education requirement met` MEANS ...
        `salary requirement met` MEANS ...

Multi-Stage Pipelines

GIVEN input IS A InputData
GIVETH A FinalResult
`process application` input MEANS
    FinalResult WITH
        stage1Result IS result1
        stage2Result IS result2
        stage3Result IS result3
    WHERE
        result1 MEANS `stage 1 processing` input
        result2 MEANS `stage 2 processing` result1
        result3 MEANS `stage 3 processing` result2

Recursive List Processing

GIVEN list IS A LIST OF T
GIVETH A ReturnType
processRecursive list MEANS
    CONSIDER list
    WHEN EMPTY THEN baseCase
    WHEN head FOLLOWED BY tail THEN
        combineResults (process head) (processRecursive tail)

Contractual State Machines

For contracts with sequential obligations:

-- Simple two-party contract
PARTY `The Seller`
MAY `offer` product price
HENCE PARTY `The Buyer`
      MAY `accept`
      HENCE PARTY `The Buyer`
            MUST `pay` price
            WITHIN (DATE OF 15, 3, 2025)
            HENCE PARTY `The Seller`
                  MUST `deliver` product
                  WITHIN (DATE OF 30, 3, 2025)
                  HENCE FULFILLED
                  LEST BREACH
            LEST BREACH
      LEST FULFILLED  -- Buyer declines, contract ends

-- Recurring obligations (subscriptions, loans)
GIVEN remaining IS A NUMBER
`monthly obligations` remaining MEANS
    IF remaining GREATER THAN 0
    THEN PARTY subscriber
         MUST pay monthlyFee
         WITHIN nextDueDate
         HENCE `monthly obligations` (remaining MINUS 1)
         LEST `late payment process` remaining
    ELSE FULFILLED

Troubleshooting

Type Errors

Error: "Expected NUMBER but got STRING" Fix: Check field types in records, ensure arithmetic only on numbers

Error: "Pattern match not exhaustive" Fix: Add OTHERWISE clause or handle all enum constructors

Layout Errors

Error: "Parse error: unexpected token" Fix: Check indentation—L4 is layout-sensitive like Python/Haskell

Undefined Functions

Error: "Not in scope: function name" Fix: Ensure function is defined before use, or add IMPORT statement

Current Limitations (Regulative Rules)

No MUST NOT (Prohibitions)

L4 currently lacks a MUST NOT keyword for prohibitions.

Workaround: Model prohibitions as actions that, if performed, trigger an impossible-to-fulfill obligation:

-- Prohibition: Employee must not disclose for 5 years
IF Disclosure happens within 5 years
   THEN PARTY Employee
        MUST `do impossible action` PROVIDED FALSE
        WITHIN 0   -- Immediate breach
   ELSE FULFILLED

A future MUST NOT keyword will provide cleaner syntax and enable static analysis.

BREACH is an Outcome, Not a Keyword

You don't write BREACH in L4 code. A breach occurs when:

1. A WITHIN deadline passes
2. No LEST clause handles the failure

The evaluator produces a breach result with:

• Which party breached
• What action was required
• What deadline was missed

MAY Has Limited Use

MAY exists but is essentially an option: the party can act or not. Without consequences for counter-parties, MAY is a no-op. Most real contracts use MUST with LEST reparation clauses.

Resources

This skill includes comprehensive reference materials about L4:

references/

• syntax-quick-ref.md: Concise syntax reference for all L4 constructs
• github-resources.md: Links to documentation, examples, and source code in the l4-ide repository
• workflow-guide.md: Detailed step-by-step workflow from legal text to deployed application

Consult these references when you need:

• Syntax reminders for specific constructs
• Links to example programs
• Guidance on the complete formalization workflow

Academic Background

• Tom Hvitved: Contract Formalisation and Modular Implementation of Domain-Specific Languages (PhD thesis, IT University of Copenhagen) — Theoretical foundation for L4's regulative rules

L4 Documentation

• Foundation Course: Basic L4 syntax, types, and functions
• Advanced Course Module A11: Detailed treatment of regulative rules with promissory note walkthrough
• jl4/examples/legal/promissory-note.l4: Complete executable example

scripts/

• validate.sh: Wrapper script for jl4-cli validation

assets/

• template.l4: Basic L4 file template with common structure
• example-parking.l4: Complete working example (parking fee calculation)

Key Takeaways

1. L4 is functional and type-safe like Haskell, designed for legal reasoning
2. DECLARE defines types (enums with IS ONE OF, records with HAS)
3. GIVEN/GIVETH/MEANS defines functions with mandatory type signatures
4. Pattern matching with CONSIDER/WHEN is more powerful than switch/case
5. Mixfix notation enables natural language function names
6. Validate with jl4-cli or cloud validator before testing
7. #EVAL and #ASSERT for comprehensive testing
8. Regulative rules (PARTY/MUST/WITHIN/HENCE/LEST) model contracts with deadlines, blame, and reparation
9. #TRACE simulates contract execution and shows residual obligations
10. AND/OR compose obligations; LEST provides reparation before breach
11. Current limitations: No MUST NOT yet; BREACH is an evaluation outcome, not syntax
12. Isomorphic encoding: Match legal text structure in code structure
13. Import prelude and daydate for standard library functions
14. Use WHERE clauses for local helpers and cleaner code

For complete tutorials, see:

• Foundation Course: https://github.com/smucclaw/l4-ide/tree/main/doc/foundation-course-ai
• Advanced Course Module A11 (Regulative Rules): https://github.com/smucclaw/l4-ide/tree/main/doc/advanced-course-ai