# System F

> Implement System F (polymorphic lambda calculus) with type abstraction and application. Use when this capability is needed.

- Skill: `tomevault-io/system-f` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add tomevault-io/system-f`
- Raw SKILL.md: https://api.skillmd.com/api/skills/tomevault-io/system-f/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: tomevault-io (https://skillmd.com/u/tomevault-io)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/tomevault-io/system-f

---


# System F (Polymorphic Lambda Calculus)

System F, also known as the polymorphic lambda calculus or Girard-Reynolds calculus, extends the simply-typed lambda calculus with type abstraction and type application, enabling universal quantification over types.

## When to Use This Skill

- Implementing polymorphic type systems
- Building generic programming constructs
- Researching type theory foundations
- Implementing ML-style module systems
- Understanding parametric polymorphism

## What This Skill Does

1. **Type Abstraction (Λ)**: Bind type variables in terms, written as `Λα. t`
2. **Type Application**: Instantiate polymorphic terms with concrete types, written as `t [T]`
3. **Universal Types**: Express types like `∀α. τ` for polymorphic values
4. **Kind System**: Handle type-level computation and classification
5. **Type Safety**: Prove progress and preservation theorems

## Key Concepts

| Concept | Description |
|---------|-------------|
| Type Abstraction | `Λα.t` binds type variable α in term t |
| Type Application | `t [T]` instantiates polymorphic term with type T |
| Universal Quantification | `∀α.τ` represents polymorphic types |
| Parametricity | Polymorphic functions behave uniformly across types |
| Predicativity | Type variables range only over "small" types |

## Tips

- Use De Bruijn indices for type variables to avoid capture
- Implement type substitution carefully to avoid variable capture
- Consider adding kind checking for higher-rank types
- Test with Church encodings to verify polymorphism
- Use bidirectional type checking for better error messages

## Common Use Cases

- Implementing generic data structures (lists, trees, maps)
- Building type-safe container libraries
- Researching type inference algorithms
- Understanding ML-style let-polymorphism
- Formalizing parametricity theorems

## Related Skills

- `simply-typed-lambda-calculus` - Foundation before System F
- `type-inference-engine` - Algorithm W for Hindley-Milner
- `type-class-implementer` - Type classes as alternative to System F
- `existential-types` - Dual to universal types

## Canonical References

| Reference | Why It Matters |
|-----------|----------------|
| **Girard, Lafont, Taylor, "Proofs and Types" (1989)** | Original System F presentation |
| **Pierce, "Types and Programming Languages" Ch. 23-24** | Modern textbook treatment |
| **Reynolds, "Types, Abstraction and Parametric Polymorphism" (1983)** | Parametricity theorem |
| **Wadler, "Theorems for Free!" (FPCA 1989)** | Practical parametricity results |

## Tradeoffs and Limitations

### Approach Tradeoffs

| Approach | Pros | Cons |
|----------|------|------|
| Explicit type abstraction | Simple, predictable | Verbose syntax |
| Type inference (HM) | Concise code | Less expressive than full System F |
| Bidirectional checking | Good error messages | Requires annotations at boundaries |

### When NOT to Use This Skill

- When Hindley-Milner type inference suffices (use `type-inference-engine`)
- For simple monomorphic programs (use `simply-typed-lambda-calculus`)
- When performance is critical (type erasure complicates optimization)

### Limitations

- Type reconstruction is undecidable for full System F
- Rank-N types require explicit annotations
- No built-in recursion (must add fixpoint combinator)

## Assessment Criteria

A high-quality implementation should have:

| Criterion | What to Look For |
|-----------|------------------|
| Type Safety | Proven progress and preservation |
| Substitution | Capture-avoiding type substitution |
| Error Messages | Clear indication of type mismatches |
| Parametricity | Polymorphic functions behave uniformly |

### Quality Indicators

✅ **Good**: Implements full System F with type abstraction/application, proven type safety
⚠️ **Warning**: Only handles rank-1 types, missing explicit type application
❌ **Bad**: No type abstraction, just simply-typed lambda calculus

## Research Tools & Artifacts

System F implementations:

| Tool | What to Learn |
|------|---------------|
| **GHC Core** | System F in practice |
| **Twelf** | Logical framework |

## Research Frontiers

### 1. Higher-Rank Types
- **Challenge**: Type inference for rank-N polymorphism
- **Approach**: Bidirectional type checking with annotations
- **Papers**: Peyton Jones et al. "Practical type inference for arbitrary-rank types" (ICFP 2004)

### 2. Kind Systems
- **Challenge**: Higher-kinded polymorphism
- **Approach**: Kind inference and checking
- **Papers**: "System Fω" (Girard)

## Implementation Pitfalls

| Pitfall | Real Consequence | Solution |
|---------|-----------------|----------|
| **Type inference undecidable** | Non-termination | Use bidirectional checking |
| **Variable capture** | Wrong types | De Bruijn indices |
| **Missing type application** | Runtime errors | Explicit instantiation |

---
> Converted and distributed by [TomeVault](https://tomevault.io/claim/rainoftime) — claim your Tome and manage your conversions.
<!-- tomevault:4.0:skill_md:2026-04-11 -->