FOR ALL

Universal quantifier for introducing type variables in polymorphic type signatures. Used to declare that a value or function works for any type.

Syntax

FOR ALL typeVar
FOR ALL typeVar1 AND typeVar2
FOR ALL typeVar1 AND typeVar2 AND typeVar3 ...

Purpose

FOR ALL introduces type variables (type parameters) in type signatures, enabling polymorphism. A polymorphic function can operate on values of any type without knowing the specific type in advance.

Examples

Example file:

-- FOR ALL Examples
-- Universal quantifier for polymorphic type signatures

--------------------------------------------------------------------------------
-- Basic Polymorphic Type Declarations
--------------------------------------------------------------------------------

-- Identity function: works for any type
ASSUME identity IS
  FOR ALL a
  A FUNCTION FROM a TO a

-- Constant function: ignores second argument
ASSUME const IS
  FOR ALL a AND b
  A FUNCTION FROM a AND b TO a

--------------------------------------------------------------------------------
-- List Operations (Polymorphic)
--------------------------------------------------------------------------------

-- Map: apply function to each element
ASSUME map IS
  FOR ALL a AND b
  A FUNCTION
    FROM      FUNCTION FROM a TO b
          AND LIST OF a
    TO    LIST OF b

-- Filter: keep elements matching predicate
ASSUME filter IS
  FOR ALL a
  A FUNCTION
    FROM      FUNCTION FROM a TO BOOLEAN
          AND LIST OF a
    TO    LIST OF a

-- Fold: reduce list to single value
ASSUME foldl IS
  FOR ALL a AND b
  A FUNCTION
    FROM      FUNCTION FROM b AND a TO b
          AND b
          AND LIST OF a
    TO    b

--------------------------------------------------------------------------------
-- Custom Algebraic Types with Type Parameters
--------------------------------------------------------------------------------

-- A choice between two types (like Either in Haskell)
DECLARE Choice OF a, b
  IS ONE OF
    Left  HAS payload IS AN a
    Right HAS payload IS A  b

-- Optional value (like Maybe in Haskell)
DECLARE Optional OF a
  IS ONE OF
    None
    Some HAS value IS AN a

-- A pair of two values
DECLARE Pair OF a, b
  HAS first IS AN a
      second IS A b

--------------------------------------------------------------------------------
-- Functions Using Custom Types
--------------------------------------------------------------------------------

-- Handle either alternative of a Choice
ASSUME either IS
  FOR ALL a AND b AND c
  A FUNCTION
    FROM      FUNCTION FROM a TO c
          AND FUNCTION FROM b TO c
          AND Choice OF a, b
    TO    c

-- Extract value from Optional with default
ASSUME fromOptional IS
  FOR ALL a
  A FUNCTION
    FROM      a
          AND Optional OF a
    TO    a

-- Create a pair
ASSUME makePair IS
  FOR ALL a AND b
  A FUNCTION FROM a AND b TO Pair OF a, b

--------------------------------------------------------------------------------
-- Implementing Polymorphic Functions with GIVEN
--------------------------------------------------------------------------------

-- The definition style uses GIVEN ... IS A TYPE
GIVEN a IS A TYPE
      b IS A TYPE
      f IS A FUNCTION FROM a TO b
      list IS A LIST OF a
GIVETH A LIST OF b
myMap f list MEANS
  CONSIDER list
  WHEN EMPTY THEN EMPTY
  WHEN x FOLLOWED BY xs THEN f x FOLLOWED BY myMap f xs

-- Length works for any list type
GIVEN a IS A TYPE
      list IS A LIST OF a
GIVETH A NUMBER
myLength list MEANS
  CONSIDER list
  WHEN EMPTY THEN 0
  WHEN x FOLLOWED BY xs THEN 1 PLUS myLength xs

-- Reverse a list (simplified - just demonstrates the pattern)
GIVEN a IS A TYPE
      list IS A LIST OF a
GIVETH A LIST OF a
myReverse list MEANS
  CONSIDER list
  WHEN EMPTY THEN EMPTY
  WHEN x FOLLOWED BY xs THEN append (myReverse xs) (x FOLLOWED BY EMPTY)

-- Helper for append
GIVEN a IS A TYPE
      list1 IS A LIST OF a
      list2 IS A LIST OF a
GIVETH A LIST OF a
append list1 list2 MEANS
  CONSIDER list1
  WHEN EMPTY THEN list2
  WHEN x FOLLOWED BY xs THEN x FOLLOWED BY append xs list2

--------------------------------------------------------------------------------
-- Using Polymorphic Functions
--------------------------------------------------------------------------------

-- Test data
DECIDE numbers IS LIST 1, 2, 3, 4, 5
DECIDE strings IS LIST "a", "b", "c"

-- Apply myLength to different list types
#EVAL myLength numbers  -- 5
#EVAL myLength strings  -- 3

-- Map with different types
GIVEN n IS A NUMBER
double n MEANS n TIMES 2

#EVAL myMap double numbers  -- LIST 2, 4, 6, 8, 10

--------------------------------------------------------------------------------
-- Higher-Order Polymorphic Functions
--------------------------------------------------------------------------------

-- Function composition
ASSUME compose IS
  FOR ALL a AND b AND c
  A FUNCTION
    FROM      FUNCTION FROM b TO c
          AND FUNCTION FROM a TO b
    TO    FUNCTION FROM a TO c

-- Flip argument order
ASSUME flip IS
  FOR ALL a AND b AND c
  A FUNCTION
    FROM      FUNCTION FROM a AND b TO c
    TO    FUNCTION FROM b AND a TO c

--------------------------------------------------------------------------------
-- Polymorphic Tree Type
--------------------------------------------------------------------------------

DECLARE Tree OF a
  IS ONE OF
    Leaf HAS value IS AN a
    Node HAS
      left IS A Tree OF a
      right IS A Tree OF a

-- Count nodes in a tree
GIVEN a IS A TYPE
      tree IS A Tree OF a
GIVETH A NUMBER
treeSize tree MEANS
  CONSIDER tree
  WHEN Leaf v THEN 1
  WHEN Node l r THEN treeSize l PLUS treeSize r

-- Example tree
DECIDE exampleTree IS
  Node WITH
    left IS Leaf WITH value IS 1
    right IS Node WITH
      left IS Leaf WITH value IS 2
      right IS Leaf WITH value IS 3

#EVAL treeSize exampleTree  -- 3

Single Type Variable

-- A function that works for any type 'a'
ASSUME identity IS
  FOR ALL a
  A FUNCTION FROM a TO a

This declares identity as a function that takes a value of any type and returns a value of the same type.

Multiple Type Variables

-- The classic 'map' function for lists
ASSUME map IS
  FOR ALL a AND b
  A FUNCTION
    FROM      FUNCTION FROM a TO b
          AND LIST OF a
    TO    LIST OF b

This says: "For all types a and b, map is a function that takes:

• a function from a to b
• a list of a values

and returns a list of b values."

With Custom Types

DECLARE Choice OF a, b
  IS ONE OF
    Left  HAS payload IS AN a
    Right HAS payload IS A  b

-- A function that handles either alternative
ASSUME choose IS
  FOR ALL a AND b AND c
  A FUNCTION
    FROM      FUNCTION FROM a TO c
          AND FUNCTION FROM b TO c
          AND Choice OF a, b
    TO    c

Usage Context

FOR ALL is used with ASSUME to declare the type of external or primitive functions. It's the declaration-style way to express polymorphism.

ASSUME vs GIVEN

There are two ways to write polymorphic functions:

Declaration style (FOR ALL): Declares a type signature without implementation

ASSUME map IS
  FOR ALL a AND b
  A FUNCTION
    FROM FUNCTION FROM a TO b AND LIST OF a
    TO LIST OF b

Definition style (GIVEN ... IS A TYPE): Defines a function with implementation

GIVEN a IS A TYPE
      b IS A TYPE
      f IS A FUNCTION FROM a TO b
      list IS A LIST OF a
GIVETH A LIST OF b
map f list MEANS
  CONSIDER list
  WHEN EMPTY THEN EMPTY
  WHEN x FOLLOWED BY xs THEN f x FOLLOWED BY map f xs

Both express the same polymorphic type, but:

• FOR ALL is for type declarations (no implementation)
• GIVEN ... IS A TYPE is for function definitions (with implementation)

Type Variables

Type variables introduced by FOR ALL:

• Are conventionally single lowercase letters: a, b, c
• Can be any valid identifier
• Are scoped to the type signature
• Must be distinct within the same FOR ALL

-- Valid:
FOR ALL a AND b AND c

-- Invalid (duplicate):
-- FOR ALL a AND a  -- Error: duplicate type variable

Common Patterns

Identity Function

ASSUME identity IS
  FOR ALL a
  A FUNCTION FROM a TO a

Constant Function

ASSUME const IS
  FOR ALL a AND b
  A FUNCTION FROM a AND b TO a

Function Composition

ASSUME compose IS
  FOR ALL a AND b AND c
  A FUNCTION
    FROM      FUNCTION FROM b TO c
          AND FUNCTION FROM a TO b
    TO    FUNCTION FROM a TO c

List Operations

ASSUME head IS
  FOR ALL a
  A FUNCTION FROM LIST OF a TO MAYBE a

ASSUME tail IS
  FOR ALL a
  A FUNCTION FROM LIST OF a TO LIST OF a

ASSUME filter IS
  FOR ALL a
  A FUNCTION
    FROM      FUNCTION FROM a TO BOOLEAN
          AND LIST OF a
    TO    LIST OF a

NOT a Runtime Quantifier

Important: FOR ALL is a type-level construct, not a runtime quantifier over lists or collections.

-- WRONG - FOR ALL is not for iterating over lists:
-- FOR ALL x IN myList CHECK x > 0  -- NOT VALID L4!

-- CORRECT - use prelude functions for list quantification:
all (GIVEN x YIELD x > 0) myList    -- Check all elements
any (GIVEN x YIELD x > 0) myList    -- Check if any element

Comparison with Other Languages

L4	Haskell	TypeScript	Java
FOR ALL a	forall a.	<T>	<T>
FOR ALL a AND b	forall a b.	<T, U>	<T, U>

Related Keywords

• GIVEN - Function parameters (including type parameters)
• TYPE - The kind of types
• ASSUME - Declare types without implementation
• FUNCTION - Function type constructor

See Also

• Types Reference - Type system overview
• Polymorphic Types - LIST, MAYBE, EITHER
• Prelude Library - Polymorphic standard functions