A generalized algebraic data type (GADT) is an algebraic data type whose constructors can state more precise result types than the type’s general declaration. That lets a constructor carry both an operation and the exact kind of value that operation produces. The compiler can preserve this relationship when code constructs, pattern-matches, or interprets the value, moving part of a program’s correctness logic into types. section 2.1.2 section 6.4.2
The practical problem appears when an embedded domain-specific language contains operations with different result types. A controller-status request returns an Either HardwareFailure ControllerStatus, while a sensor read returns an Either HardwareFailure Measurement. With an ordinary constructor returning DeviceControlMethod a, that distinction is hidden behind an unconstrained type variable. A GADT instead gives each constructor its own explicit result type, so an interpreter must return the result promised by the operation it matches. section 6.4.2 section 6.4.2
Typed device-control operations
A GADT can model a small API as typed requests: GetStatus accepts a Controller and produces DeviceControlMethod (Either HardwareFailure ControllerStatus); ReadSensor accepts a Controller and ComponentIndex and produces DeviceControlMethod (Either HardwareFailure Measurement). Pattern matching on GetStatus therefore commits the interpreter to produce a controller status, while matching ReadSensor commits it to produce a measurement. Smart constructors can then lift either request into a larger LogicControl language without losing its result type. section 6.4.2 section 6.4.2
Listing 13.15 GADT interface with smart constructors
data AstroService a where
ReportMeteorGADT
:: MeteorTemplate
-> AstroService (Either ReportingError MeteorId)
ReportAsteroidGADT
:: AsteroidTemplate
-> AstroService (Either ReportingError AsteroidId)
reportMeteorGadt
:: MeteorTemplate
-> AstroService (Either ReportingError MeteorId)
reportMeteorGadt m = ReportMeteorGADT m
reportAsteroidGadt
:: AsteroidTemplate
-> AstroService (Either ReportingError AsteroidId)
reportAsteroidGadt a = ReportAsteroidGADT a
This interface assigns a distinct AstroService result type to each reporting operation, then exposes ordinary helper functions for constructing those requests. section 13.2.5
GADTs also support embedding scripts whose result types vary from occurrence to occurrence. An EvalHdl constructor can package an Hdl a together with a continuation a -> next. The locally quantified type variable ties the script’s returned value to the continuation that consumes it, without forcing every embedded Hdl operation in the surrounding language to return one global type. The same pattern can embed operations from more than one sublanguage. section 6.4.2 section 6.4.2
Choose a GADT when its typed constructors match the shape of the interface:
- Use it for API-like interfaces: independent service operations can have distinct, compiler-checked return types and be interpreted by pattern matching. section 13.2.5
- Inject a runner such as forall a. AstroService a -> AppL a so business logic depends on the service language rather than a concrete reporting channel. section 13.2.5
- Prefer a free monad when operations must form sequential scripts; GADT values lack continuation fields and do not directly provide that sequencing structure. section 13.2.5 section 6.5
A GADT is not automatically a replacement for a free-monad language. Its concise typed requests suit a service API where calls are made individually. Free monads add continuations and a domain algebra parameterization, making them better suited to scenario-like, sequential languages and to chaining nested scripts. The design choice is therefore architectural: preserve precise per-operation result types with a GADT, or add a sequential scripting structure when the domain needs it. section 13.2.5 section 6.5
