11 ms·

GADTs for Dummies

60 points by gbrown_ 5y ago

whateveracct 5y ago
Once you understand their basics, GADTs are as easy to use as any other mainstream language feature. I wonder if any mainstream language will meaningfully have them soon. Not technically (many do) but meaningfully. Lightweight syntax and fully-powered pattern matching.
- anmolsahoo25 5y ago
  OCaml already does. Some good examples - JSON GADT : https://github.com/OCamlPro/ocplib-json-typed/blob/0d9e9cde74c7c50aa6d053990b46f5930c80de54/src/json_encoding.ml#L46 https://github.com/OCamlPro/ocplib-json-typed/blob/0d9e9cde7... Mirage/repr, uses GADT's for representing OCaml types as runtime values which are used for implementing dynamic polymorphism - https://github.com/mirage/repr/blob/main/src/repr/type.ml https://github.com/mirage/repr/blob/main/src/repr/type.ml
  - whateveracct 5y ago
    I count OCaml as "mainstream" as Haskell ;) it's one of the good ones
- nickmain 5y ago
  Haxe does. Not that Haxe is mainstream, but it does target mainstream languages.
- rtpg 5y ago
  Typescript, as a counterexample, doesn't need GADTs because it has first-class union support + nice type filtering. There's a bit of manual tagging that's needed but the ergonomics are both easy to understand and more flexible (not to mention supporting even other usage patterns). type Term = {kind: 'lit', value: number} | {kind: 'pair', left: Term, right: Term}; function pair(left: Term, right: Term): Term & {kind: 'pair'} { return {kind: 'pair', left, right}; } function lit(n: number): Term & {kind: 'lit'} { return {kind: 'lit', value: n}; } let t: Term = pair( pair(lit(1), lit(2)), lit(3) );
  - lmm 5y ago
    Your example doesn't show using a type parameter, which is what makes a GADT a GADT. As far as I can see your example is just an ADT.
    - def-lkb 5y ago
      Indeed. GADTs provide type equalities and existentials. This example involves neither, only sub-typing (which is quite strong and interesting in Typescript)
      - culturedsystems 5y ago
        Something pretty similar to the AST example in another thread can be implemented in Typescript using sub typing (as it happens, trying to do something like that is how I first found out about GADTs). Looking into existential types, I see that one of the things they can be used for is OOP style subtype polymorphism [1]. Are there things you can do with existential types that can't be done with subtyping? [1] https://wiki.haskell.org/Existential_type#Dynamic_dispatch_mechanism_of_OOP https://wiki.haskell.org/Existential_type#Dynamic_dispatch_m...
        lmm 5y ago
        An ADT is a "closed" type like an enum, which then enables other features that you can't implement for OO-style "open" subtyping (e.g. pattern matching). You can encode that in a traditional-OO language with the visitor pattern, but it's very cumbersome to work with in practice. The other subtle thing with GADTs is that the type information must flow back from the matched case to the type parameter: if you match an Ast<R> and get Mul, you know that R=Int. And that part is impossible to do fully in a language that doesn't have higher-kinded types, because you not only need to be able to know that you can pass an Int where an R was expected, but also that you can pass an Ast<Int> where an Ast<R> is expected, or return a List<Int> where a List<R> is expected, or....
        deleted 5y ago
        [deleted]
bradrn 5y ago
I like using GADTs in Haskell. However, I find the explanation in the article nearly impossible to understand. This annoys me, so I will attempt to give my own explanation of what GADTs are. (Because everyone else explains it incorrectly and my explanation is of course the best, right? /s) So, a bit of Haskell first, starting with algebraic data types. (Skip this if you already know about ADTs.) If you want to define a data type in most languages, there are basically two things you can do. Either you can define a record, with multiple values wrapped up as a single type: data MyRecord = ConstructorName Int String Bool Or, you can define an enumeration, where a type has a limited set of allowed values: data TrafficLight = Red | Amber | Green Haskell calls the former ‘product types’ and the latter ‘sum types’. The thing is, there’s nothing stopping you from combining the two: making an enumeration where each value of the enumeration is a record. This is called an algebraic data type (because it combines sums and products, geddit?) For instance, this lets me make an AST for a simple language: data AST = Integer Int | Boolean Bool | Addition AST AST | Multiplication AST AST | Equals AST AST | Not AST So now I can make values like `Not (Equals (Integer 1) (Integer 2)) :: AST`. (In Haskell, read ‘::’ as ‘has-type’.) Often, you want to make data types polymorphic over the record field type. For instance, I might have a type expressing either an integer or an error: data IntErr = Error String | IntResult Int And I might have expressing either a string or an error: data StrErr = Error String | StrResult Int And eventually I might get tired of writing out all these types. In that case I can add a type variable representing any type: data WithError a = Error String | Result a So now I can have `Result 3 :: WithError Int`, `Result True :: WithError Bool`, and so on. (This is basically the same as generics or templates in languages which have them.) The thing is, no-one says a type parameter needs to correspond to anything concrete. There’s nothing in Haskell which stops me from doing this: data Weird a b = IgnoreTheType Int This is a bit weird. If you have a value of type `Weird String Bool`, say, that value won’t actually have a string or a boolean within it. And `IgnoreTheType 1 :: Weird String Bool`, `IgnoreTheType 2 :: Weird Char Float`, `IgnoreTheType 3 :: Weird Bool Double` are all values of different types. You can basically change the type at will without affecting the value. Variables such as `a` and `b` are called ‘phantom type variables’. Now let’s back up a bit and have another look at that `AST` data type I defined earlier. It’s not particularly satisfying: you can easily create meaningless terms like `Addition (Boolean True) (Not (Integer 3))`. As Haskellers, we want to avoid this as much as possible. So let’s add a phantom type parameter to express the type returned by each `AST` constructor: data AST r = Integer Int | Boolean Bool | Addition (AST Int) (AST Int) | Multiplication (AST Int) (AST Int) | Equals (AST r) (AST r) | Not (AST Bool) This says that multiplication, for instance, must take two `AST`s returning an `Int`, as encoded in the type parameter. But wait — how do we restrict the type parameter? We need to be able to say that something constructed with `Multiplication` must have type `AST Int`, but something constructed with `Not` must have type `AST Bool`. As it happens, vanilla Haskell has no way of doing this. There is no way of explicitly controlling the value of `r` based on which constructor is used. You might have guessed by now that this is exactly what generalised algebraic data types let us do. And indeed, `AST` can be easily implemented as a GADT: data AST r where Integer :: Int -> AST Int Boolean :: Bool -> AST Bool Addition :: AST Int -> AST Int -> AST Int Multiplication :: AST Int -> AST Int Equals :: AST r -> AST r -> AST Bool Not :: AST Bool -> AST Bool And now, if we try to construct an incorrect AST, the compiler will give us back an error, because the types don’t match: > Addition (Boolean True) (Not (Integer 3)) <interactive>:11:11: error: * Couldn't match type `Bool' with `Int' Expected type: AST Int Actual type: AST Bool * In the first argument of `Addition', namely `(Boolean True)' In the expression: Addition (Boolean True) (Not (Integer 3)) In an equation for `it': it = Addition (Boolean True) (Not (Integer 3)) <interactive>:11:26: error: * Couldn't match type `Bool' with `Int' Expected type: AST Int Actual type: AST Bool * In the second argument of `Addition', namely `(Not (Integer 3))' In the expression: Addition (Boolean True) (Not (Integer 3)) In an equation for `it': it = Addition (Boolean True) (Not (Integer 3)) <interactive>:11:31: error: * Couldn't match type `Int' with `Bool' Expected type: AST Bool Actual type: AST Int * In the first argument of `Not', namely `(Integer 3)' In the second argument of `Addition', namely `(Not (Integer 3))' In the expression: Addition (Boolean True) (Not (Integer 3))
siraben 5y ago
I like that GADTs are a good example of "lightweight dependent types". You don't need to use full-blown dependent types to achieve the following: - type-safe AST representations of a language - type-safe encoding of lambda calculus and an eval function that will only accept _closed terms_ (i.e. no free variables!) In Coq, everything is defined in the GADT style and with dependent types you have an explosion of possibilities: - length-indexed vectors - dependently-typed red-black trees - inductive proofs! just to name a few.
- AnthonBerg 5y ago
  Useful take, thanks! I assume it varies, but I find Idris' dependent type system to be easier to reason about and understand than non-dependent ones I've worked with (say, OCaml and Haskell). Even if Idris can be judged as strictly more powerful in that regard. There's a sense of a closed loop of consistency and a smaller, tighter set of thought patterns that apply both on this side and the other side – whatever those sides may be, say, values vs. types, compilation vs. runtime, AST vs. raw syntax, parsing vs. printing… It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :)
  - siraben 5y ago
    Yes! I love the consistency of dependent types. You don't need separate declarations for type aliases or a dozen language extensions to do some type-level evaluation, it's quite uniform. > It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :) Indeed, I feel like we are just getting started finding the right "design patterns" for working with dependently typed programs. It's sort of a Wild West of styles in the Coq world currently, IMO, which is great when something is well designed but terrible when using a theorem demands you prove some clearly obvious precondition (e.g. Riemann integration in the stdlib is a pain to work with).
    - AnthonBerg 5y ago
fho 5y ago
Somewhat related: What has blown my mind at some point is that with dependent types you can actually check your algorithms for correctness. --- Example: http://goto.ucsd.edu:8090/index.html#?demo=Order.hs http://goto.ucsd.edu:8090/index.html#?demo=Order.hs Press Check -> The button should turn green and say "Safe" Now mess up the algorithm, e.g. change the `>=` in line 174 to `<=` in effect changing the sorting order. Press Check again -> The button should turn red and the line you changed should be highlighted telling you that at this point you violated the ordering constraint that put in place by the `IncrList a` type. --- To be fair, I don't think too many programming work is low-level algorithmic programming where this would be applicable. I see the benefits in having type level size constraints on arrays or having a "Safe / Unsafe" constraint on input from users that can only be changed by running through verification functions.
- bidirectional 5y ago
  These are refinement types, rather than dependent types. The main distinction as I understand it being that refinement types allow you to state assertions at a meta-level which are submitted to an SMT solver which may or may not prove them correct, dependent types on the other hand allow expression of arbitrary constraints within the types themselves, along with arbitrary proofs satisfying these types.
  - fho 5y ago
    Yeah ... I am no expert there. I would guess there is some overlap between refinement and dependent types, thou.
gawi 5y ago
Understanding how GADT works only comes next to understanding how leveraging the typing system during design can be beneficial. The motivation to go through this tutorial stems from the desire to let the typing system strengthen the programs and API. I'm coming from the Java world and I've spent some time learning Haskell for my own culture. At the time, I was trying to use Java generics to encode some restrictions in my design. It was interesting but alas a bit limited by the Java generics implementation and the results were most of the time hard to use or understand. I'd like to see more articles on how GADT (or any other mechanism) can improve a concret design, with real-life examples. Starting with a native design leveraging only a few tricks from the typing system up to a final version where constraints are properly encoded.

60 points by gbrown_ 5y ago

Once you understand their basics, GADTs are as easy to use as any other mainstream language feature. I wonder if any mainstream language will meaningfully have them soon. Not technically (many do) but meaningfully. Lightweight syntax and fully-powered pattern matching.

anmolsahoo25 5y ago
OCaml already does. Some good examples - JSON GADT : https://github.com/OCamlPro/ocplib-json-typed/blob/0d9e9cde74c7c50aa6d053990b46f5930c80de54/src/json_encoding.ml#L46 https://github.com/OCamlPro/ocplib-json-typed/blob/0d9e9cde7... Mirage/repr, uses GADT's for representing OCaml types as runtime values which are used for implementing dynamic polymorphism - https://github.com/mirage/repr/blob/main/src/repr/type.ml https://github.com/mirage/repr/blob/main/src/repr/type.ml
- whateveracct 5y ago
  I count OCaml as "mainstream" as Haskell ;) it's one of the good ones
nickmain 5y ago
Haxe does. Not that Haxe is mainstream, but it does target mainstream languages.
rtpg 5y ago
Typescript, as a counterexample, doesn't need GADTs because it has first-class union support + nice type filtering. There's a bit of manual tagging that's needed but the ergonomics are both easy to understand and more flexible (not to mention supporting even other usage patterns). type Term = {kind: 'lit', value: number} | {kind: 'pair', left: Term, right: Term}; function pair(left: Term, right: Term): Term & {kind: 'pair'} { return {kind: 'pair', left, right}; } function lit(n: number): Term & {kind: 'lit'} { return {kind: 'lit', value: n}; } let t: Term = pair( pair(lit(1), lit(2)), lit(3) );
- lmm 5y ago
  Your example doesn't show using a type parameter, which is what makes a GADT a GADT. As far as I can see your example is just an ADT.
  - def-lkb 5y ago
    Indeed. GADTs provide type equalities and existentials. This example involves neither, only sub-typing (which is quite strong and interesting in Typescript)
    - culturedsystems 5y ago
      Something pretty similar to the AST example in another thread can be implemented in Typescript using sub typing (as it happens, trying to do something like that is how I first found out about GADTs). Looking into existential types, I see that one of the things they can be used for is OOP style subtype polymorphism [1]. Are there things you can do with existential types that can't be done with subtyping? [1] https://wiki.haskell.org/Existential_type#Dynamic_dispatch_mechanism_of_OOP https://wiki.haskell.org/Existential_type#Dynamic_dispatch_m...
      - lmm 5y ago
        An ADT is a "closed" type like an enum, which then enables other features that you can't implement for OO-style "open" subtyping (e.g. pattern matching). You can encode that in a traditional-OO language with the visitor pattern, but it's very cumbersome to work with in practice. The other subtle thing with GADTs is that the type information must flow back from the matched case to the type parameter: if you match an Ast<R> and get Mul, you know that R=Int. And that part is impossible to do fully in a language that doesn't have higher-kinded types, because you not only need to be able to know that you can pass an Int where an R was expected, but also that you can pass an Ast<Int> where an Ast<R> is expected, or return a List<Int> where a List<R> is expected, or....
      - deleted 5y ago
        [deleted]

bradrn 5y ago

I like using GADTs in Haskell. However, I find the explanation in the article nearly impossible to understand. This annoys me, so I will attempt to give my own explanation of what GADTs are. (Because everyone else explains it incorrectly and my explanation is of course the best, right? /s) So, a bit of Haskell first, starting with algebraic data types. (Skip this if you already know about ADTs.) If you want to define a data type in most languages, there are basically two things you can do. Either you can define a record, with multiple values wrapped up as a single type: data MyRecord = ConstructorName Int String Bool Or, you can define an enumeration, where a type has a limited set of allowed values: data TrafficLight = Red | Amber | Green Haskell calls the former ‘product types’ and the latter ‘sum types’. The thing is, there’s nothing stopping you from combining the two: making an enumeration where each value of the enumeration is a record. This is called an algebraic data type (because it combines sums and products, geddit?) For instance, this lets me make an AST for a simple language: data AST = Integer Int | Boolean Bool | Addition AST AST | Multiplication AST AST | Equals AST AST | Not AST So now I can make values like `Not (Equals (Integer 1) (Integer 2)) :: AST`. (In Haskell, read ‘::’ as ‘has-type’.) Often, you want to make data types polymorphic over the record field type. For instance, I might have a type expressing either an integer or an error: data IntErr = Error String | IntResult Int And I might have expressing either a string or an error: data StrErr = Error String | StrResult Int And eventually I might get tired of writing out all these types. In that case I can add a type variable representing any type: data WithError a = Error String | Result a So now I can have `Result 3 :: WithError Int`, `Result True :: WithError Bool`, and so on. (This is basically the same as generics or templates in languages which have them.) The thing is, no-one says a type parameter needs to correspond to anything concrete. There’s nothing in Haskell which stops me from doing this: data Weird a b = IgnoreTheType Int This is a bit weird. If you have a value of type `Weird String Bool`, say, that value won’t actually have a string or a boolean within it. And `IgnoreTheType 1 :: Weird String Bool`, `IgnoreTheType 2 :: Weird Char Float`, `IgnoreTheType 3 :: Weird Bool Double` are all values of different types. You can basically change the type at will without affecting the value. Variables such as `a` and `b` are called ‘phantom type variables’. Now let’s back up a bit and have another look at that `AST` data type I defined earlier. It’s not particularly satisfying: you can easily create meaningless terms like `Addition (Boolean True) (Not (Integer 3))`. As Haskellers, we want to avoid this as much as possible. So let’s add a phantom type parameter to express the type returned by each `AST` constructor: data AST r = Integer Int | Boolean Bool | Addition (AST Int) (AST Int) | Multiplication (AST Int) (AST Int) | Equals (AST r) (AST r) | Not (AST Bool) This says that multiplication, for instance, must take two `AST`s returning an `Int`, as encoded in the type parameter. But wait — how do we restrict the type parameter? We need to be able to say that something constructed with `Multiplication` must have type `AST Int`, but something constructed with `Not` must have type `AST Bool`. As it happens, vanilla Haskell has no way of doing this. There is no way of explicitly controlling the value of `r` based on which constructor is used. You might have guessed by now that this is exactly what generalised algebraic data types let us do. And indeed, `AST` can be easily implemented as a GADT: data AST r where Integer :: Int -> AST Int Boolean :: Bool -> AST Bool Addition :: AST Int -> AST Int -> AST Int Multiplication :: AST Int -> AST Int Equals :: AST r -> AST r -> AST Bool Not :: AST Bool -> AST Bool And now, if we try to construct an incorrect AST, the compiler will give us back an error, because the types don’t match: > Addition (Boolean True) (Not (Integer 3)) <interactive>:11:11: error: * Couldn't match type `Bool' with `Int' Expected type: AST Int Actual type: AST Bool * In the first argument of `Addition', namely `(Boolean True)' In the expression: Addition (Boolean True) (Not (Integer 3)) In an equation for `it': it = Addition (Boolean True) (Not (Integer 3)) <interactive>:11:26: error: * Couldn't match type `Bool' with `Int' Expected type: AST Int Actual type: AST Bool * In the second argument of `Addition', namely `(Not (Integer 3))' In the expression: Addition (Boolean True) (Not (Integer 3)) In an equation for `it': it = Addition (Boolean True) (Not (Integer 3)) <interactive>:11:31: error: * Couldn't match type `Int' with `Bool' Expected type: AST Bool Actual type: AST Int * In the first argument of `Not', namely `(Integer 3)' In the second argument of `Addition', namely `(Not (Integer 3))' In the expression: Addition (Boolean True) (Not (Integer 3))

siraben 5y ago

I like that GADTs are a good example of "lightweight dependent types". You don't need to use full-blown dependent types to achieve the following: - type-safe AST representations of a language - type-safe encoding of lambda calculus and an eval function that will only accept _closed terms_ (i.e. no free variables!) In Coq, everything is defined in the GADT style and with dependent types you have an explosion of possibilities: - length-indexed vectors - dependently-typed red-black trees - inductive proofs! just to name a few.

AnthonBerg 5y ago
Useful take, thanks! I assume it varies, but I find Idris' dependent type system to be easier to reason about and understand than non-dependent ones I've worked with (say, OCaml and Haskell). Even if Idris can be judged as strictly more powerful in that regard. There's a sense of a closed loop of consistency and a smaller, tighter set of thought patterns that apply both on this side and the other side – whatever those sides may be, say, values vs. types, compilation vs. runtime, AST vs. raw syntax, parsing vs. printing… It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :)
- siraben 5y ago
  Yes! I love the consistency of dependent types. You don't need separate declarations for type aliases or a dozen language extensions to do some type-level evaluation, it's quite uniform. > It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :) Indeed, I feel like we are just getting started finding the right "design patterns" for working with dependently typed programs. It's sort of a Wild West of styles in the Coq world currently, IMO, which is great when something is well designed but terrible when using a theorem demands you prove some clearly obvious precondition (e.g. Riemann integration in the stdlib is a pain to work with).
  - AnthonBerg 5y ago

fho 5y ago

Somewhat related: What has blown my mind at some point is that with dependent types you can actually check your algorithms for correctness. --- Example: http://goto.ucsd.edu:8090/index.html#?demo=Order.hs http://goto.ucsd.edu:8090/index.html#?demo=Order.hs Press Check -> The button should turn green and say "Safe" Now mess up the algorithm, e.g. change the `>=` in line 174 to `<=` in effect changing the sorting order. Press Check again -> The button should turn red and the line you changed should be highlighted telling you that at this point you violated the ordering constraint that put in place by the `IncrList a` type. --- To be fair, I don't think too many programming work is low-level algorithmic programming where this would be applicable. I see the benefits in having type level size constraints on arrays or having a "Safe / Unsafe" constraint on input from users that can only be changed by running through verification functions.

bidirectional 5y ago
These are refinement types, rather than dependent types. The main distinction as I understand it being that refinement types allow you to state assertions at a meta-level which are submitted to an SMT solver which may or may not prove them correct, dependent types on the other hand allow expression of arbitrary constraints within the types themselves, along with arbitrary proofs satisfying these types.
- fho 5y ago
  Yeah ... I am no expert there. I would guess there is some overlap between refinement and dependent types, thou.

gawi 5y ago

Understanding how GADT works only comes next to understanding how leveraging the typing system during design can be beneficial. The motivation to go through this tutorial stems from the desire to let the typing system strengthen the programs and API. I'm coming from the Java world and I've spent some time learning Haskell for my own culture. At the time, I was trying to use Java generics to encode some restrictions in my design. It was interesting but alas a bit limited by the Java generics implementation and the results were most of the time hard to use or understand. I'd like to see more articles on how GADT (or any other mechanism) can improve a concret design, with real-life examples. Starting with a native design leveraging only a few tricks from the typing system up to a final version where constraints are properly encoded.