# \#gadt **URL:** https://discuss.ocaml.org/tag/gadt/101.md [Latest](https://discuss.ocaml.org/latest.md) · [Categories](https://discuss.ocaml.org/categories.md) · [Tags](https://discuss.ocaml.org/tags.md) --- ## [Tutorial on GADTs](https://discuss.ocaml.org/t/tutorial-on-gadts/14040)
**Author:** [@raphael-proust](https://discuss.ocaml.org/u/raphael-proust)\ **Replies:** 35\ **Last updated:** [October 7, 2026, 8:13am UTC](https://discuss.ocaml.org/t/tutorial-on-gadts/14040 "2026-10-07T08:13:54Z")
I’ve written a three-part tutorial on GADTs. The first part shows the very basic. It is intended for anyone who already knows OCaml but hasn’t written a GADT before. The second part is a collection of different techniq… --- ## [Question on GADT and variance annotation](https://discuss.ocaml.org/t/question-on-gadt-and-variance-annotation/14598)
**Author:** [@pveber](https://discuss.ocaml.org/u/pveber)\ **Replies:** 7\ **Last updated:** [October 23, 2025, 1:16pm UTC](https://discuss.ocaml.org/t/question-on-gadt-and-variance-annotation/14598 "2025-10-23T13:16:10Z")
Dear all, I don’t understand why the following type definition is not accepted: type +\_ u = U : 'a -\> 'a list u Error: In this GADT definition, the variance of some parameter cannot be checked Could someone exp… --- ## [GADT to encode function arity](https://discuss.ocaml.org/t/gadt-to-encode-function-arity/17033)
**Author:** [@dlesbre](https://discuss.ocaml.org/u/dlesbre)\ **Replies:** 5\ **Last updated:** [August 4, 2025, 7:03am UTC](https://discuss.ocaml.org/t/gadt-to-encode-function-arity/17033 "2025-08-04T07:03:11Z")
Tentative minimal example Is there a way to create a GADT to encode a function return type and arity, leaving the function argument type as a parameter? I would like to create a type that encodes Equalhas two arguments… --- ## [Parameterized GADT type witnesses](https://discuss.ocaml.org/t/parameterized-gadt-type-witnesses/16827)
**Author:** [@joelreymont](https://discuss.ocaml.org/u/joelreymont)\ **Replies:** 6\ **Last updated:** [June 16, 2025, 12:47pm UTC](https://discuss.ocaml.org/t/parameterized-gadt-type-witnesses/16827 "2025-06-16T12:47:09Z")
My compiler’s AST is initially annotated with location but I dislike how location shows up in my expect tests. I’d like to strip location before testing, e.g. by replacing location with unit. This requires that my AST be… --- ## [Syntax for returning existential types from a function](https://discuss.ocaml.org/t/syntax-for-returning-existential-types-from-a-function/16452)
**Author:** [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Replies:** 1\ **Last updated:** [April 8, 2025, 7:53am UTC](https://discuss.ocaml.org/t/syntax-for-returning-existential-types-from-a-function/16452 "2025-04-08T07:53:19Z")
When working with parametrized types I often find myself doing things like this to “return an existential type” from a function: type (\_, \_) my\_func\_result = My\_func\_result : ('a, 'c) foo \* ('b, 'c) bar -\> ('a, 'b) my… --- ## [Telling the type checker that two GADTs are equal](https://discuss.ocaml.org/t/telling-the-type-checker-that-two-gadts-are-equal/16368)
**Author:** [@droyo](https://discuss.ocaml.org/u/droyo)\ **Replies:** 6\ **Last updated:** [March 24, 2025, 11:03pm UTC](https://discuss.ocaml.org/t/telling-the-type-checker-that-two-gadts-are-equal/16368 "2025-03-24T23:03:06Z")
I’ve been working on a side-project in OCaml that binds to the libmnl library to interact with netlink sockets to add/remove/update network links. I have been taking my time and experimenting to learn more about OCaml… --- ## [Reads for GADT, existential types, universally quantified type code](https://discuss.ocaml.org/t/reads-for-gadt-existential-types-universally-quantified-type-code/5464)
**Author:** [@milvi](https://discuss.ocaml.org/u/milvi)\ **Replies:** 4\ **Last updated:** [March 20, 2025, 7:39pm UTC](https://discuss.ocaml.org/t/reads-for-gadt-existential-types-universally-quantified-type-code/5464 "2025-03-20T19:39:15Z")
Hello :slight\_smile: Do you know code with plenty of GADT, existential types, universally quantified types ? I would like to read such things. Thanks ! --- ## [Reducing a recursively parameterized data type?](https://discuss.ocaml.org/t/reducing-a-recursively-parameterized-data-type/16240)
**Author:** [@sporkl](https://discuss.ocaml.org/u/sporkl)\ **Replies:** 6\ **Last updated:** [March 8, 2025, 11:38pm UTC](https://discuss.ocaml.org/t/reducing-a-recursively-parameterized-data-type/16240 "2025-03-08T23:38:00Z")
Suppose I have the following tree type: type \_ weirdtree = | Leaf : int -\> int weirdtree | Node : ('a weirdtree \* 'a weirdtree) -\> 'a weirdtree weirdtree Suppose I want to convert the tree into a list: let rec lis… --- ## [Using GADTs to track properties of a state type. Help and alternative approaches?](https://discuss.ocaml.org/t/using-gadts-to-track-properties-of-a-state-type-help-and-alternative-approaches/15867)
**Author:** [@kentookura](https://discuss.ocaml.org/u/kentookura)\ **Replies:** 3\ **Last updated:** [January 6, 2025, 4:32pm UTC](https://discuss.ocaml.org/t/using-gadts-to-track-properties-of-a-state-type-help-and-alternative-approaches/15867 "2025-01-06T16:32:49Z")
I have a compiler that features multiple compilation phases. Consider the following simplified example: module M = Map.Make(String) type state = { phase1: string M.t; phase2: int M.t; phase3: string M.t; } let s… --- ## [Avoiding extra matching with extensible GADTs](https://discuss.ocaml.org/t/avoiding-extra-matching-with-extensible-gadts/15282)
**Author:** [@s.t.s](https://discuss.ocaml.org/u/s.t.s)\ **Replies:** 19\ **Last updated:** [September 21, 2024, 12:25am UTC](https://discuss.ocaml.org/t/avoiding-extra-matching-with-extensible-gadts/15282 "2024-09-21T00:25:58Z")
It is very inspiring that the extensible GADTs (the GADT types that could be extended like extensible variant types, cf. manual as well as this post) are now available in OCaml. They do bring a promise of typed data ann… --- ## [Does using object types in GADTs get you any more power?](https://discuss.ocaml.org/t/does-using-object-types-in-gadts-get-you-any-more-power/14042)
**Author:** [@Joel](https://discuss.ocaml.org/u/Joel)\ **Replies:** 10\ **Last updated:** [September 16, 2024, 2:41pm UTC](https://discuss.ocaml.org/t/does-using-object-types-in-gadts-get-you-any-more-power/14042 "2024-09-16T14:41:32Z")
I recently learned that you could use object types in GADTs! In this example it’s just used as a “type-level record”, which if I understand correctly means that it isn’t much more powerful that using \* or -\> types, with … --- ## [Best approach for implementing open recursion over extensible types](https://discuss.ocaml.org/t/best-approach-for-implementing-open-recursion-over-extensible-types/11678)
**Author:** [@Gopiandcode](https://discuss.ocaml.org/u/Gopiandcode)\ **Replies:** 7\ **Last updated:** [September 15, 2024, 12:30am UTC](https://discuss.ocaml.org/t/best-approach-for-implementing-open-recursion-over-extensible-types/11678 "2024-09-15T00:30:38Z")
I have a datatype, designed to be user-extensible, with particular constructors defined in different sub-modules: type 'a expr = .. type 'a expr += | Int : int -\> int expr | Add : 'a expr \* 'a expr -\> 'a expr | S… --- ## [Binding existentials in a non-uniform GADT](https://discuss.ocaml.org/t/binding-existentials-in-a-non-uniform-gadt/14809)
**Author:** [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Replies:** 1\ **Last updated:** [June 18, 2024, 8:38am UTC](https://discuss.ocaml.org/t/binding-existentials-in-a-non-uniform-gadt/14809 "2024-06-18T08:38:51Z")
I learned recently that you can explicitly name the existentials when pattern-matching on a GADT. However, this doesn’t seem to work when the type parameters of the GADT are non-uniform: type \_ foo = Foo : 'a \* 'b -\> (… --- ## [Annotating by an existential type](https://discuss.ocaml.org/t/annotating-by-an-existential-type/14721)
**Author:** [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Replies:** 6\ **Last updated:** [June 4, 2024, 6:37am UTC](https://discuss.ocaml.org/t/annotating-by-an-existential-type/14721 "2024-06-04T06:37:25Z")
When using GADTs I often find myself needing to give a type annotation that’s impossible to give because it involves existential types that I don’t have a name for. For instance, consider the following code: type bar =… --- ## [Narrowing variant types alternatives](https://discuss.ocaml.org/t/narrowing-variant-types-alternatives/3806)
**Author:** [@ale](https://discuss.ocaml.org/u/ale)\ **Replies:** 11\ **Last updated:** [May 21, 2024, 11:22am UTC](https://discuss.ocaml.org/t/narrowing-variant-types-alternatives/3806 "2024-05-21T11:22:55Z")
Consider the following type representing types in a programming language: type t = | Name of string | Record of (string \* t) list | Array of (t \* int) Is there a way to limit the type t in Array of (t \* int) to b… --- ## [Faking type families to encode extensible tagless-final interpreters](https://discuss.ocaml.org/t/faking-type-families-to-encode-extensible-tagless-final-interpreters/14647)
**Author:** [@Matthieu\_Lemerre](https://discuss.ocaml.org/u/Matthieu_Lemerre)\ **Replies:** 2\ **Last updated:** [May 16, 2024, 11:53am UTC](https://discuss.ocaml.org/t/faking-type-families-to-encode-extensible-tagless-final-interpreters/14647 "2024-05-16T11:53:26Z")
Hello, I am trying to define a language in the style of the tagless-final interpreters of Carett, Kiselyov and Shan (my goal is to perform tagless-final abstract interpretation, as described in a forthcoming PLDI paper)… --- ## [Limit the possible constructor in another type constuctor](https://discuss.ocaml.org/t/limit-the-possible-constructor-in-another-type-constuctor/14440)
**Author:** [@olleharstedt](https://discuss.ocaml.org/u/olleharstedt)\ **Replies:** 3\ **Last updated:** [April 5, 2024, 9:09pm UTC](https://discuss.ocaml.org/t/limit-the-possible-constructor-in-another-type-constuctor/14440 "2024-04-05T21:09:34Z")
Maybe I don’t understand GADT correctly, but I want to limit which constructors are available in a certain type lvalue can be a bunch of things, but for HashSet statement, I want to limit lvalue to be Variable of string… --- ## [Generalised abstract data types, phantom types and modules](https://discuss.ocaml.org/t/generalised-abstract-data-types-phantom-types-and-modules/14211)
**Author:** [@koizel](https://discuss.ocaml.org/u/koizel)\ **Replies:** 2\ **Last updated:** [February 28, 2024, 10:47am UTC](https://discuss.ocaml.org/t/generalised-abstract-data-types-phantom-types-and-modules/14211 "2024-02-28T10:47:03Z")
Consider the two following code snippets type atp type smt type \_ config = | ConfigSmt : smt config | ConfigAtp : atp config let digest : smt config -\> unit = fun cfg -\> match cfg with ConfigSmt -\> () and modul… --- ## [Explicitly polymorphic function inside a universally quantified record field (e.g., an effect handler)?](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889)
**Author:** [@Zeta](https://discuss.ocaml.org/u/Zeta)\ **Replies:** 6\ **Last updated:** [January 17, 2024, 2:58pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889 "2024-01-17T14:58:04Z")
How do I define an explicitly polymorphic function inside a universally quantified record field, e.g., inside an effect handler? Here is a MWE: open Effect open Effect.Deep type \_ Effect.t += Eff : ('a -\> 'a) t let r… --- ## [Patching a GADT-and-phantom-types-heavy-library … what did I do wrong?](https://discuss.ocaml.org/t/patching-a-gadt-and-phantom-types-heavy-library-what-did-i-do-wrong/13425)
**Author:** [@ELLIOTTCABLE](https://discuss.ocaml.org/u/ELLIOTTCABLE)\ **Replies:** 2\ **Last updated:** [November 15, 2023, 10:52am UTC](https://discuss.ocaml.org/t/patching-a-gadt-and-phantom-types-heavy-library-what-did-i-do-wrong/13425 "2023-11-15T10:52:39Z")
I’m trying to update a large, complex library that heavily uses GADTs and phantom types. Unfortunately, I seem to have ended up somewhat out of my depth — I just cannot get my patch to compile. Here’s a “minimal” reprod… --- ## [GADT and OR pattern matching](https://discuss.ocaml.org/t/gadt-and-or-pattern-matching/4154)
**Author:** [@cloudyhug](https://discuss.ocaml.org/u/cloudyhug)\ **Replies:** 4\ **Last updated:** [September 4, 2023, 8:47am UTC](https://discuss.ocaml.org/t/gadt-and-or-pattern-matching/4154 "2023-09-04T08:47:05Z")
Hi everyone. I have noticed a very strange behaviour for GADTs when using pattern matching. Consider the following type and function : type \_ t = | A : int t | B : int t | C : char t let f : type a. a t -\> (a -\> … --- ## [Exisential types and types variables equality](https://discuss.ocaml.org/t/exisential-types-and-types-variables-equality/12919)
**Author:** [@Gholad](https://discuss.ocaml.org/u/Gholad)\ **Replies:** 1\ **Last updated:** [August 29, 2023, 9:56am UTC](https://discuss.ocaml.org/t/exisential-types-and-types-variables-equality/12919 "2023-08-29T09:56:27Z")
I try to write an heterogenous formatter for learning purpose, and i’m stuck on a type variable equality issue i think, here the code : module IdList = struct type (\_, \_) t = | \[\] : (\_,Peano.zero) t | ( :: ) :… --- ## [Can't write a transition which can lead to two different states](https://discuss.ocaml.org/t/cant-write-a-transition-which-can-lead-to-two-different-states/12708)
**Author:** [@Gholad](https://discuss.ocaml.org/u/Gholad)\ **Replies:** 6\ **Last updated:** [July 28, 2023, 3:44pm UTC](https://discuss.ocaml.org/t/cant-write-a-transition-which-can-lead-to-two-different-states/12708 "2023-07-28T15:44:22Z")
Hi, I heard that, in OCaml, GADTs is the best way to write a statically typesafe explicit state machine, especially because it allows to write exhaustive pattern matching without referencing all the constructors of the … --- ## [Mapping GADT with Polymorphic Variant into a more restrictive form](https://discuss.ocaml.org/t/mapping-gadt-with-polymorphic-variant-into-a-more-restrictive-form/12214)
**Author:** [@Ben\_James](https://discuss.ocaml.org/u/Ben_James)\ **Replies:** 5\ **Last updated:** [May 24, 2023, 9:13pm UTC](https://discuss.ocaml.org/t/mapping-gadt-with-polymorphic-variant-into-a-more-restrictive-form/12214 "2023-05-24T21:13:44Z")
Hello! Suppose I have the following GADT in Ocaml: type \_ t = | A : f t | B : f t \* f t -\> f t | C : c t \* c t -\> f t | D : \[\< f | c\] t \* c t -\> c t | E : c t | T : string -\> \[\< f | c\] t where f and c are … --- ## [A bestiary of GADT examples?](https://discuss.ocaml.org/t/a-bestiary-of-gadt-examples/12143)
**Author:** [@Chet\_Murthy](https://discuss.ocaml.org/u/Chet_Murthy)\ **Replies:** 11\ **Last updated:** [May 18, 2023, 11:37am UTC](https://discuss.ocaml.org/t/a-bestiary-of-gadt-examples/12143 "2023-05-18T11:37:34Z")
Is there someplace a bestiary of GADT examples ? I’d like to find such a thing in order to more-fully understand the universe of possibilities for using GADTs in programming. I’ve never used 'em, and while, sure, readi… --- ## [ChatGPT explains GADTs](https://discuss.ocaml.org/t/chatgpt-explains-gadts/11759)
**Author:** [@Haudegen](https://discuss.ocaml.org/u/Haudegen)\ **Replies:** 4\ **Last updated:** [March 24, 2023, 2:37pm UTC](https://discuss.ocaml.org/t/chatgpt-explains-gadts/11759 "2023-03-24T14:37:12Z")
I asked ChatGPT: “Explain GADTs in OCaml” and it came up with the following answer: GADT stands for Generalized Algebraic Data Type. In OCaml, GADTs are a language extension that allows defining more precise types for … --- ## [Design suggestions for a functor with existential wrappers](https://discuss.ocaml.org/t/design-suggestions-for-a-functor-with-existential-wrappers/11401)
**Author:** [@Gopiandcode](https://discuss.ocaml.org/u/Gopiandcode)\ **Replies:** 7\ **Last updated:** [February 13, 2023, 6:06am UTC](https://discuss.ocaml.org/t/design-suggestions-for-a-functor-with-existential-wrappers/11401 "2023-02-13T06:06:40Z")
I’m designing an interface for a data structure that uses GADTs and I’ve run into a small blocker. My functor accepts module types of the following module type S = sig type t type 'a op (\*\* operations on the dat… --- ## [Question on continuations](https://discuss.ocaml.org/t/question-on-continuations/11320)
**Author:** [@ddickstein](https://discuss.ocaml.org/u/ddickstein)\ **Replies:** 3\ **Last updated:** [February 6, 2023, 10:46am UTC](https://discuss.ocaml.org/t/question-on-continuations/11320 "2023-02-06T10:46:56Z")
Is it possible to define printf in terms of sprintf without the use of ksprintf (or any of the other formatted output functions with continuations)? My actual use case involves a custom GADT, not format strings, but I t… --- ## [Explicitly name types in GADT patterns](https://discuss.ocaml.org/t/explicitly-name-types-in-gadt-patterns/11168)
**Author:** [@Lupjo](https://discuss.ocaml.org/u/Lupjo)\ **Replies:** 12\ **Last updated:** [January 13, 2023, 11:08pm UTC](https://discuss.ocaml.org/t/explicitly-name-types-in-gadt-patterns/11168 "2023-01-13T23:08:48Z")
Hi everyone, Section 7.6 of the manual gives a syntax to explicitly name existential types in GADTs, but it doesn’t say what to do when the type is not an existential type. Here’s a snippet that I would want to work. How… --- ## [Blog post: Testing in Seqes](https://discuss.ocaml.org/t/blog-post-testing-in-seqes/11115)
**Author:** [@raphael-proust](https://discuss.ocaml.org/u/raphael-proust)\ **Replies:** 0\ **Last updated:** [January 5, 2023, 8:02am UTC](https://discuss.ocaml.org/t/blog-post-testing-in-seqes/11115 "2023-01-05T08:02:23Z")
I have written a blog post about the test suite which covers this library. TL;DR: I use GADTs to describe the library API and generate QCheck tests. I manually used mutaml for mutation-testing on the test suite. http… [Next page](https://discuss.ocaml.org/tag/gadt/101.md?match_all_tags=true&page=1&tags%5B%5D=gadt)