# 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

```l4
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:** 

```l4-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

```l4
-- 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

```l4
-- 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

```l4
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

```l4
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

```l4
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`

```l4
-- Valid:
FOR ALL a AND b AND c

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

## Common Patterns

### Identity Function

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

### Constant Function

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

### Function Composition

```l4
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

```l4
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.

```l4
-- 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](/l4/reference/functions/GIVEN.md)** - Function parameters (including type parameters)
- **[TYPE](/l4/reference/types/keywords.md)** - The kind of types
- **[ASSUME](/l4/reference/types/ASSUME.md)** - Declare types without implementation
- **[FUNCTION](/l4/reference/types/keywords.md)** - Function type constructor

## See Also

- **[Types Reference](/l4/reference/types.md)** - Type system overview
- **[Polymorphic Types](/l4/reference/types.md#polymorphic-types)** - LIST, MAYBE, EITHER
- **[Prelude Library](/l4/reference/libraries/prelude.md)** - Polymorphic standard functions