4

All tutorials on GADTs that I've seen (in Haskell, Coq and Idris) use one same exapmle of a well-typed interpreter to show how GADTs can be useful, where you use the type index to encode the type of the term in the object language.

What are some other examples and general rules for when we should think of GADT as a solution?

Improve this question
2

1 Answer 1

Reset to default
-5

Link dump for the OCaml side of things:

Some concrete use cases:

Improve this answer
3
  • 5
    Link dumps don't make good answers because links eventually die. Can you bring some of the relevant content from these links into your answer?
    – MetaFight
    Commented Feb 27, 2017 at 16:12
  • 1
    No I can't. OP expects a set of concrete use cases, So I provide concrete use cases as links to the actual libraries. Not a simplified toy explanation that would fit here. This is an extremely common question that comes back frequently. I don't see the value of not pointing to external significant sources.
    – Drup
    Commented Feb 27, 2017 at 19:42
  • 1
    @Drup It's against the conventions of this site. Note that the question itself is off-topic here and shouldn't be answered at all.
    – Andres F.
    Commented Feb 27, 2017 at 21:35

Not the answer you're looking for? Browse other questions tagged or ask your own question.