# 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:** ```l4-file -- 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:** ```l4-file -- 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](https://github.com/smucclaw/l4-ide/blob/main/jl4-core/libraries/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:** ```l4-file -- 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:** ```l4-file -- 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:** ```l4-file -- 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](https://github.com/smucclaw/l4-ide/blob/main/jl4-core/libraries/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:** ```l4-file -- 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:** ```l4-file 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:** ```l4-file -- 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](/l4/reference/builtins.md) and [coercions](/l4/reference/types/coercions.md) 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. ```l4-file -- 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 ```l4-file -- 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. ```l4-file -- 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 ```l4-file -- 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. ```l4-file -- 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](/l4/reference/GLOSSARY.md)** - Complete language index - **[Functions](/l4/reference/functions.md)** - Function keywords - **[Operators](/l4/reference/operators.md)** - Operations on types - **[Type Theory](/l4/reference/types/type-theory.md)** - Formal type inference rules, bidirectional checking, and advanced type system details - **[Specifications](https://github.com/smucclaw/l4-ide/tree/main/specs)** - Technical specifications