3 ms·

Once you get the hang of algebraic data types (ADTs), definitely check out generalized ADTs (GADTs). They reduce the amount of code required to express a soluti

Once you get the hang of algebraic data types (ADTs), definitely check out generalized ADTs (GADTs). They reduce the amount of code required to express a solution, make the type system do a ton of work for you to prevent bugs from compiling, and make it easier to embed domain-specific languages in your code. A lot of the GADT tutorials out there are a little abstract for my taste and I wish there were more examples with tangible applications, but this one is decent: http://joeyh.name/blog/entry/making_propellor_safer_with_GADTs_and_type_families/ http://joeyh.name/blog/entry/making_propellor_safer_with_GAD...

tom_mellior 9y ago
I also liked this one: https://blog.janestreet.com/why-gadts-matter-for-performance/ https://blog.janestreet.com/why-gadts-matter-for-performance...
Peaker 9y ago
Why do they reduce the amount of code? They add the ability for constructors to carry constraints, which aids expressivity in some cases. But the majority of GADT uses purely add safety. Can use ordinary ADT without a type-variable that is correlated with the data constructor, and crash at runtime if the constructors don't match.
- tom_mellior 9y ago
  > Why do they reduce the amount of code? [...] crash at runtime if the constructors don't match. You answered yourself: If you cannot have these runtime type mismatches, you don't need to write the corresponding bookkeeping and checking code.
  - Peaker 9y ago
    You don't have to write it - you just have to avoid -Wall :-)
- dpwm 9y ago
  I thought GADTs would be useless to me when I first heard the explanation of GADTs as imposing additional constraints on ADTs. Whilst technically true, it feels like it's missing the point. The real power of GADTs comes from the fact that you can use the type at compile time. This means that in OCaml I can do something like: type 'a t = | Int : int t | Float : float t let print : type a. a t -> (a -> string) = function | Int -> string_of_int | Float -> string_of_float I can the do (print Float) and receive string_of_float. I can do (print Int) and receive string_of_int. Both have drastically different types, but due to the constraints that the GADT imposes it is fully type safe and the type is known at compile time. Although this is a slightly contrived and useless example, there are scenarios where this can prove immensely useful that are not that far away and really aren't so useful when done with ADTs. Think serializing -- you would have to convert to the ADT first which isn't so useful. If you're interested in something useful, take a look at [0] (shameless plug), a very early alpha version of a similar idea allowing conversion from and to JSON. EDIT: this is not inlined as I recall. False memory. The reason it isn't is probably because you can use existential types in which case the type would not be known at compile time. [0] https://github.com/dpwm/typespec https://github.com/dpwm/typespec
Drup 9y ago
If you want to have fun, I also have a small tutorial on how to make a typesafe printf function with GADTs (and that technique is actually used in the OCaml stdlib!) https://drup.github.io/2016/08/02/difflists/ https://drup.github.io/2016/08/02/difflists/ I also have some slides (more entertaining and probably better introduction) here: https://www.irif.fr/~gradanne/papers/gadts.pdf https://www.irif.fr/~gradanne/papers/gadts.pdf

tom_mellior 9y ago

I also liked this one: https://blog.janestreet.com/why-gadts-matter-for-performance/ https://blog.janestreet.com/why-gadts-matter-for-performance...

Peaker 9y ago

Why do they reduce the amount of code? They add the ability for constructors to carry constraints, which aids expressivity in some cases. But the majority of GADT uses purely add safety. Can use ordinary ADT without a type-variable that is correlated with the data constructor, and crash at runtime if the constructors don't match.

tom_mellior 9y ago
> Why do they reduce the amount of code? [...] crash at runtime if the constructors don't match. You answered yourself: If you cannot have these runtime type mismatches, you don't need to write the corresponding bookkeeping and checking code.
- Peaker 9y ago
  You don't have to write it - you just have to avoid -Wall :-)
dpwm 9y ago
I thought GADTs would be useless to me when I first heard the explanation of GADTs as imposing additional constraints on ADTs. Whilst technically true, it feels like it's missing the point. The real power of GADTs comes from the fact that you can use the type at compile time. This means that in OCaml I can do something like: type 'a t = | Int : int t | Float : float t let print : type a. a t -> (a -> string) = function | Int -> string_of_int | Float -> string_of_float I can the do (print Float) and receive string_of_float. I can do (print Int) and receive string_of_int. Both have drastically different types, but due to the constraints that the GADT imposes it is fully type safe and the type is known at compile time. Although this is a slightly contrived and useless example, there are scenarios where this can prove immensely useful that are not that far away and really aren't so useful when done with ADTs. Think serializing -- you would have to convert to the ADT first which isn't so useful. If you're interested in something useful, take a look at [0] (shameless plug), a very early alpha version of a similar idea allowing conversion from and to JSON. EDIT: this is not inlined as I recall. False memory. The reason it isn't is probably because you can use existential types in which case the type would not be known at compile time. [0] https://github.com/dpwm/typespec https://github.com/dpwm/typespec

Drup 9y ago

If you want to have fun, I also have a small tutorial on how to make a typesafe printf function with GADTs (and that technique is actually used in the OCaml stdlib!) https://drup.github.io/2016/08/02/difflists/ https://drup.github.io/2016/08/02/difflists/ I also have some slides (more entertaining and probably better introduction) here: https://www.irif.fr/~gradanne/papers/gadts.pdf https://www.irif.fr/~gradanne/papers/gadts.pdf