L4 Types Reference

L4's type system provides strong static typing with type inference, algebraic data types, and polymorphism. This reference documents all types available in L4.

L4 uses a Hindley-Milner-style type system with bidirectional type checking, algebraic data types, and lazy (call-by-need) evaluation. The core is pure functional, with DEONTIC as an effect type for regulative rules.

Overview

L4's type system is inspired by functional programming languages like Haskell and includes:

• Primitive types - Basic data types (NUMBER, STRING, BOOLEAN, DATE, TIME, DATETIME)
• Algebraic types - Records (products) and enums (sums)
• Polymorphic types - Generic types parameterized by other types
• Function types - First-class functions
• Type constructors - Building complex types from simpler ones

---

Primitive Types

NUMBER

Numeric values including integers and rationals.

• Integers: 42, -17, 0
• Rationals: 3.14, -0.5, 2.718, 5.4%
• Arbitrary precision arithmetic
• Examples: Age calculations, financial amounts, quantities, percentages

STRING

Text strings enclosed in double quotes.

• Unicode support
• Escape sequences: \", \\, \n, etc.
• String concatenation with CONCAT or APPEND
• Examples: Names, descriptions, legal text

BOOLEAN

Truth values for logical operations.

• Values: TRUE, FALSE
• Three-valued logic support (with UNKNOWN for partial evaluation)
• Logical operators: AND, OR, NOT, IMPLIES
• Examples: Eligibility checks, conditions, yes/no answers

DATE

Calendar dates for temporal reasoning.

• ISO 8601 format: YYYY-MM-DD
• Date arithmetic and comparison
• Integration with daydate library
• Examples: Deadlines, effective dates, time periods

TIME

Wall-clock time-of-day (no date or timezone component).

• 24-hour format internally: HH:MM:SS
• Time arithmetic with midnight wrapping
• Integration with time library
• Examples: Business hours, curfew checks, scheduling constraints

DATETIME

Absolute points in time combining date, time, and timezone.

• Stored internally as UTC
• Extractors return local values in the stored timezone
• Cross-timezone comparison
• Integration with datetime library
• Examples: Legal deadlines, transaction timestamps, cross-timezone events

---

Algebraic Types

Records

Product types with named fields.

Example:

-- Example: Record type declaration
-- Demonstrates product types with named fields

DECLARE Person
  HAS `full name` IS A STRING
      age         IS A NUMBER

-- Example: Creating a person record
`the applicant` MEANS Person WITH
  `full name` IS "John Doe"
  age         IS 30

#EVAL `the applicant`'s `full name`
#EVAL `the applicant`'s age

• Named fields with types
• Field access with 's
• Construction with WITH keyword
• Examples: Structured data, entities, configurations

Enums

Sum types with named constructors.

Example:

-- Example: Enum type declaration
-- Demonstrates sum types with named constructors

DECLARE Color IS ONE OF
  Red
  Green
  Blue

-- Example usage
`my favorite color` MEANS Red

`name of the color` MEANS
  CONSIDER `my favorite color`
  WHEN Red   THEN "red"
  WHEN Green THEN "green"
  WHEN Blue  THEN "blue"

#EVAL `name of the color`

• Pattern matching with CONSIDER/WHEN
• Constructors with optional fields
• Discriminated unions
• Examples: Status values, categories, variants

PAIR

Two-element product type from prelude.

Note: PAIR is defined in the prelude library. See prelude.l4 for implementation.

• Generic over both element types
• Used in key-value data structures
• Tuple-like functionality
• Examples: Coordinates, key-value pairs, associations

---

Type Correspondence

How L4 types map to concepts in other languages and type theory:

L4 Construct	Type Theory	Haskell	Other Languages	Category Theory
DECLARE T HAS ...	Product	data T = T { ... }	struct/class/interface	Product (x)
IS ONE OF	Sum	data T = A | B	enum/union/variant/sealed class	Coproduct (+)
GIVEN...GIVETH	Arrow	a -> b	function signature/def/fn	Exponential (B^A)
MAYBE T	Option	Maybe T	Optional/null/nil/None/?	T + 1
LIST OF T	List	[T]	Array/List/Vec/Sequence	Free monoid
CONSIDER	Match	case...of	switch/case/match/when	Catamorphism
BRANCH	Guards	| cond = ...	if-elseif chain/cond	-
WHERE / LET...IN	Binding	where / let...in	let/const/var/local	Substitution
DEONTIC	Effect	Custom monad	- (domain-specific)	Kleisli category
's genitive	Accessor	Record field / lens	dot notation / .field	Projection

---

Polymorphic Types

LIST

Ordered collection of elements of the same type.

Example:

-- Example: List type usage
-- Demonstrates list literals and cons operator

-- List literal syntax
`first list` MEANS LIST 1, 2, 3

-- Cons operator (FOLLOWED BY)
`second list` MEANS 1 FOLLOWED BY 2 FOLLOWED BY 3 FOLLOWED BY EMPTY

#EVAL `first list`
#EVAL `second list`

• Homogeneous (all elements same type)
• Recursive structure
• Rich prelude functions: map, filter, fold, etc.
• Examples: Collections, sequences, ordered data

MAYBE

Optional values that may be present or absent.

Example:

-- Example: Maybe type usage
-- Demonstrates optional values with JUST and NOTHING

`value is present` MEANS JUST OF 42
`value is absent` MEANS NOTHING

`get the value or default to zero` MEANS
  CONSIDER `value is present`
  WHEN JUST OF x THEN x
  WHEN NOTHING THEN 0

#EVAL `get the value or default to zero`

• Handles nullability explicitly
• No null pointer errors
• Pattern matching for safety
• Examples: Optional fields, lookup results, partial functions

EITHER

Choice between two alternative values.

Example:

-- Example: Either type usage
-- Either represents a choice: LEFT for errors, RIGHT for success values

-- Declare a result with explicit EITHER type
ASSUME `api result` IS AN EITHER STRING NUMBER

-- Create specific Either values
`error case` MEANS LEFT OF "Error occurred"
`success case` MEANS RIGHT OF 42

-- Pattern match to handle both cases
GIVEN result IS AN EITHER STRING NUMBER
`handle the result` result MEANS
  CONSIDER result
  WHEN LEFT OF err THEN CONCAT "Error: ", err
  WHEN RIGHT OF val THEN CONCAT "Success: ", TOSTRING val

#EVAL `handle the result` `error case`
#EVAL `handle the result` `success case`

• Discriminated union of two types
• Often used for error handling
• Pattern matching to handle both cases
• Examples: Success/failure, validation, branching logic

Dictionary

Associative map from keys to values (from prelude).

Note: Dictionary is defined in the prelude library. See prelude.l4 for implementation.

• Generic key-value store
• Lookup by key
• Rich API: insert, delete, update, union, etc.
• Examples: Configuration, mappings, indexes

---

Type Constructors

TYPE

The kind of types (a type of types).

• Used in type signatures
• IS A TYPE declares a type parameter
• Enables polymorphism
• Examples: Generic functions, type parameters

FUNCTION

Function types.

Example:

-- Example: Function type
-- Demonstrates function type signature

GIVEN x IS A NUMBER
      y IS A NUMBER
GIVETH A NUMBER
add x y MEANS x PLUS y

#EVAL add 5 3

• First-class functions
• Multi-parameter with AND
• Higher-order functions supported
• Examples: Callbacks, operators, combinators

---

Type System Features

Type Inference

L4 can often infer types automatically.

Example:

GIVEN x IS A NUMBER
      y IS A NUMBER
`add two numbers` x y MEANS x PLUS y

Type Annotations

Explicit types improve clarity and catch errors. See examples throughout the type reference pages.

Polymorphism

Generic types work with any type.

Example:

-- Example: Polymorphic function
-- Demonstrates generic types that work with any type

GIVEN a IS A TYPE
      list IS A LIST OF a
GIVETH A NUMBER
`length of list` list MEANS go 0 list
  WHERE
    go acc l MEANS
      CONSIDER l
      WHEN EMPTY THEN acc
      WHEN x FOLLOWED BY xs THEN go (acc + 1) xs

#EVAL `length of list` (LIST 1, 2, 3)
#EVAL `length of list` (LIST "a", "b", "c")

Algebraic Data Types

Combine product (AND) and sum (OR) types:

• Products: Multiple fields together (records)
• Sums: One of several alternatives (enums)
• Composable and nestable

---

Type Compatibility

Coercion

Built-in conversion functions:

• TOSTRING - Convert to STRING
• TONUMBER - Convert to NUMBER
• TODATE - Convert to DATE
• TOTIME - Convert to TIME
• TODATETIME - Convert to DATETIME
• TRUNC - Truncate to integer

See Built-ins and coercions for details.

Comparison

• Equality (EQUALS, =) works for most types
• Ordering (<, >, <=, >=) for NUMBER, STRING, DATE, TIME, DATETIME
• Custom comparison via functions

Maybe and Nullability

L4 uses MAYBE for optional values, not null.

-- Example: Maybe type usage
-- Demonstrates optional values with JUST and NOTHING

`value is present` MEANS JUST OF 42
`value is absent` MEANS NOTHING

`get the value or default to zero` MEANS
  CONSIDER `value is present`
  WHEN JUST OF x THEN x
  WHEN NOTHING THEN 0

#EVAL `get the value or default to zero`

for usage patterns.

---

Common Patterns

Option Type Pattern

Use MAYBE for nullable values. See prelude's lookup function

-- Example: Maybe type usage
-- Demonstrates optional values with JUST and NOTHING

`value is present` MEANS JUST OF 42
`value is absent` MEANS NOTHING

`get the value or default to zero` MEANS
  CONSIDER `value is present`
  WHEN JUST OF x THEN x
  WHEN NOTHING THEN 0

#EVAL `get the value or default to zero`

Either for Errors

Use EITHER for success/failure.

-- Example: Either type usage
-- Either represents a choice: LEFT for errors, RIGHT for success values

-- Declare a result with explicit EITHER type
ASSUME `api result` IS AN EITHER STRING NUMBER

-- Create specific Either values
`error case` MEANS LEFT OF "Error occurred"
`success case` MEANS RIGHT OF 42

-- Pattern match to handle both cases
GIVEN result IS AN EITHER STRING NUMBER
`handle the result` result MEANS
  CONSIDER result
  WHEN LEFT OF err THEN CONCAT "Error: ", err
  WHEN RIGHT OF val THEN CONCAT "Success: ", TOSTRING val

#EVAL `handle the result` `error case`
#EVAL `handle the result` `success case`

Lists for Collections

Use LIST for ordered data. See prelude's sum function

-- Example: List type usage
-- Demonstrates list literals and cons operator

-- List literal syntax
`first list` MEANS LIST 1, 2, 3

-- Cons operator (FOLLOWED BY)
`second list` MEANS 1 FOLLOWED BY 2 FOLLOWED BY 3 FOLLOWED BY EMPTY

#EVAL `first list`
#EVAL `second list`

Records for Structured Data

Use records for entities.

-- Example: Record type declaration
-- Demonstrates product types with named fields

DECLARE Person
  HAS `full name` IS A STRING
      age         IS A NUMBER

-- Example: Creating a person record
`the applicant` MEANS Person WITH
  `full name` IS "John Doe"
  age         IS 30

#EVAL `the applicant`'s `full name`
#EVAL `the applicant`'s age

---

Type Hierarchy

TYPE
  ├─ Primitive Types
  │   ├─ NUMBER
  │   ├─ STRING
  │   ├─ BOOLEAN
  │   ├─ DATE
  │   ├─ TIME
  │   └─ DATETIME
  │
  ├─ Algebraic Types
  │   ├─ Records (product types)
  │   └─ Enums (sum types)
  │
  ├─ Polymorphic Types
  │   ├─ LIST OF a
  │   ├─ MAYBE a
  │   ├─ EITHER a b
  │   ├─ PAIR OF a, b
  │   └─ Dictionary k v
  │
  ├─ Function Types
  │   └─ FUNCTION FROM args TO result
  │
  └─ Effect Types
      └─ DEONTIC (MUST / MAY / SHANT)

---

Learning Path

Beginners

1. Start with primitive types: NUMBER, STRING, BOOLEAN
2. Learn records for structured data
3. Understand LIST for collections

Intermediate

1. Master MAYBE for optional values
2. Use enums for variants
3. Explore EITHER for error handling

Advanced

1. Write polymorphic functions with type parameters
2. Use Dictionary for complex data structures
3. Master higher-order functions

---

See Also

• GLOSSARY - Complete language index
• Functions - Function keywords
• Operators - Operations on types
• Type Theory - Formal type inference rules, bidirectional checking, and advanced type system details
• Specifications - Technical specifications