gadt-implementer
Skill17 starsChanged 9 months agoApache-2.0View on GitHub
Implement Generalized Algebraic Data Types (GADTs) for expressive type-safe data structures.
In this repository98 other files it gives its agents.
- abstract-interpretation-engineSkill
- abstract-machineSkill
- acsl-annotation-assistantSkill
- actor-model-implementerSkill
- algebraic-effectsSkill
- alias-and-points-to-analysisSkill
- axiomatic-semanticsSkill
- bidirectional-type-checkingSkill
- bisimulation-checkerSkill
- capability-systemSkill
- closure-converterSkill
- common-subexpression-eliminatorSkill
- concurrency-verifierSkill
- constant-propagation-passSkill
- contextual-equivalenceSkill
- control-flow-analysisSkill
- coq-proof-assistantSkill
- cps-transformerSkill
- dafny-verifierSkill
- dataflow-analysis-frameworkSkill
- dead-code-eliminatorSkill
- defunctionalizationSkill
- denotational-semantics-builderSkill
- dependent-type-implementerSkill
- dsl-embeddingSkill
- effect-handlers-implementerSkill
- effect-systemSkill
- effect-type-systemSkill
- escape-analysisSkill
- existential-typesSkill
- ffi-designerSkill
- fuzzer-generatorSkill
- garbage-collector-implementerSkill
- graalvm-truffle-implementerSkill
- gradual-typing-implementerSkill
- higher-order-abstract-syntaxSkill
- hoare-logic-verifierSkill
- incremental-computationSkill
- information-flow-analyzerSkill
- inline-expanderSkill
- interprocedural-analysisSkill
- invariant-generatorSkill
- jit-compiler-builderSkill
- lambda-calculus-interpreterSkill
- language-server-protocolSkill
- lean-proverSkill
- lexer-generatorSkill
- linear-type-implementerSkill
- liveness-analysisSkill
- llvm-backend-generatorSkill
- lock-free-data-structureSkill
- loop-optimizerSkill
- loop-termination-proverSkill
- macro-expanderSkill
- memory-allocatorSkill
- message-passing-systemSkill
- mlir-dialect-designerSkill
- model-checkerSkill
- module-systemSkill
- monad-transformerSkill
- The first 60 shown.
The file
We split this skill into the rules it gives an agent
6 rules. About 0 are common, 3 are distinctive, and 3 are very specific to this project.
≈0
Common · estimate
Many files like this have a rule of this kind.
≈3
Distinctive · estimate
This author's own choices. Worth a look.
3
Very specific
Tied to their project's names, files or tools. Probably skip.
- Common
- Distinctive
- Very specific
- Distinctive: line 26
Type Indexing: Use type parameters to track additional information
- Very specific: line 43
Use {-# LANGUAGE GADTs #-} or {-# LANGUAGE GADTSyntax #-} in GHC
- Very specific: line 45
Use TypeApplications for disambiguation
- Very specific: line 47
Consider using ExistentialQuantification with GADTs
- Distinctive: line 84
When simple algebraic data types suffice
- Distinctive: line 86
When type error messages are critical for users
≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.
Files
GADT Implementer
Generalized Algebraic Data Types (GADTs) extend ordinary algebraic data types by allowing constructors to have different return types, enabling more precise type indexing and type-safe encodings.
When to Use This Skill
- Implementing typed abstract syntax trees (ASTs)
- Building type-safe embedded domain-specific languages
- Creating phantom-typed data structures
- Implementing well-typed interpreters
- Encoding invariants in types
What This Skill Does
- GADT Declaration: Define data types where constructors return different type indices
- Type Indexing: Use type parameters to track additional information
- Pattern Matching with Type Refinement: Refine types in pattern branches
- Existential Quantification: Hide type parameters in constructors
- Type-Level Programming: Encode properties in the type system
Key Concepts
| Concept | Description |
| Type Index | Type parameter that tracks additional information |
| Type Refinement | Pattern matching reveals more specific types |
| Existential | Constructors can hide type arguments |
| Phantom Types | Type parameters with no runtime representation |
| Type Witnesses | Values that witness type equalities |
Tips
- Use
{-# LANGUAGE GADTs #-}or{-# LANGUAGE GADTSyntax #-}in GHC - Combine with
DataKindsfor type-level programming - Use
TypeApplicationsfor disambiguation - Pattern matching provides type equalities - use them!
- Consider using
ExistentialQuantificationwith GADTs
Common Use Cases
- Implementing typed ASTs for compilers and interpreters
- Building type-safe protocol implementations
- Creating well-typed generic traversals
- Encoding state machines in types
- Implementing finally tagless interpreters
Related Skills
type-checker-generator- Type checking for GADTsdependent-type-implementer- More expressive than GADTsexistential-types- Existential quantificationsimply-typed-lambda-calculus- Foundation for typed ASTs
Canonical References
| Reference | Why It Matters |
| Xi, Chen & Chen, "Guarded Recursive Datatype Constructors" (POPL 2003) | Original paper introducing GADTs in ML/Haskell |
| Peyton Jones, Vytiniotis, Weirich & Shields, "Practical Type Inference for Arbitrary-Rank Types" (JFP 2007) | Type inference for GADTs and rank-N polymorphism |
| GHC User's Guide "GADTs" | Practical implementation details |
Tradeoffs and Limitations
Approach Tradeoffs
| Approach | Pros | Cons |
| GADTs | Precise types, no runtime checks | Complex type errors |
| Phantom types | Simpler | Less expressive |
| Finally tagless | No GADT syntax needed | Different style |
When NOT to Use This Skill
- When simple algebraic data types suffice
- For performance-critical code (extra indirection)
- When type error messages are critical for users
Limitations
- Type inference is less complete than for normal ADTs
- Cannot use deriving clauses for all type classes
- Pattern matching must be complete for type safety
Assessment Criteria
A high-quality implementation should have:
| Criterion | What to Look For |
| Type Safety | Pattern matching refines types correctly |
| Completeness | Handles all GADT features (existentials, equality) |
| Error Messages | Clear indication of type mismatches |
| Inference | Infers types where possible |
Quality Indicators
✅ Good: Type-safe evaluator with no runtime checks, clear GADT structure ⚠️ Warning: Overuses GADTs when simpler types would work ❌ Bad: GADT structure doesn't actually provide type safety benefits
Research Tools & Artifacts
GADT implementations:
| Tool | Language | What to Learn |
| GHC | Haskell | Production GADTs |
| OCaml | OCaml | GADTs |
| Rust | Rust | GADTs |
Research Frontiers
1. Dependent Types
- Approach: GADTs as mini dependent types
Implementation Pitfalls
| Pitfall | Real Consequence | Solution |
| Type errors | Confusing errors | Better error messages |
Does it work?
Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.
No reviews yet
People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.
- It worked
- Partly
- It didn't
Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.
Your trail
Files you open will collect here, so you can find them again.
Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.
Now do this for your own.
Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.