7 ms·

Why OCaml GADTs matter for performance

120 points by michaelochurch 12y ago

AceJohnny2 12y ago
GADTs are http://en.wikipedia.org/wiki/Generalized_algebraic_data_type http://en.wikipedia.org/wiki/Generalized_algebraic_data_type
- marktangotango 12y ago
  Upvoting, so obnoxious of the author of the post to not define them.
  - deleted 12y ago
    [deleted]
  - adultSwim 12y ago
    I can't tell if you are serious or not. OP goes through them by example. Original type: type 'a t = | Array of 'a array | Bytes of bytes GADT'd (same functionality as before): type 'a t = | Array : 'a array -> 'a t | Bytes : bytes -> 'a t Now using power of GADT to add constraint: type 'a t = | Array : 'a array -> 'a t | Bytes : bytes -> char t Just jumping into it seems like a fine choice to make. Allows for a (narrow) introduction to GADTs without getting bogged down in their full complexity/limitations. Shows that it's useful before/without a theoretical discussion. Still, I wouldn't have minded a little discussion introducing GADTs.
    - AceJohnny2 12y ago
      In the original version of the article (when I wrote my comment), the author hadn't defined them.
kragen 12y ago
I'm still not quite sure what GADTs are (after skimming the WP article, reading this article, and skimming the code in it) but very surprisingly to me, it looks like OCaml's GADT implementation tackles a lot of the memory fragmentation problems that come with object-graph-heap memory-model languages like Lisp, Python, Java, previously OCaml, JavaScript, and so on, in exchange for a little more type declaration overhead. (Although, in my small experience, debugging OCaml type errors usually involves adding some redundant type declarations anyway.) This is really interesting and I hope I understand it someday soon!
- tel 12y ago
  Generalized Algebraic Data Types, GADTs, are algebraic data types which include both (a) existential types and (b) type equalities. The combination allows for a certain kind of interaction between the specific kind of value within a type and the type itself. For instance, we might have a little expression language using normal ADTs [0] type exp = | Int of int -- integer constants | Bool of bool -- bool constants | Add of exp * exp -- addition | Neg of exp -- negation | Ifte of exp * exp * exp -- if then else | Lte of exp * exp -- less than or equal to but there's no particular guarantee that a value of `exp` is well-typed. For instance, the following is a valid value of `exp` let x : exp = Add (Int 3, Bool true) GADTs allow us to fix this situation by reflecting the type of the expression value into the type of the expression. Here's some syntax type _ exp = | Int : int -> int exp | Bool : bool -> bool exp | Add : int exp * int exp -> int exp | Neg : int exp * int exp | Ifte : bool exp * 'a exp * 'a exp -> 'a exp | Lte : int exp * int exp -> bool exp The way to read this syntax is to see it as giving the "type" of each constructor. Not only do we now parameterize the `exp` type with an index type corresponding to the type of the value this expression denotes, we also create very non-trivial type equations like Ifte : bool exp -> 'a exp -> 'a exp -> 'a exp and Lte : int exp -> int exp -> bool exp The upshot is that while the type of an interpreter for the first exp would have to look like type value = VInt of int | VBool of bool val interpret : exp -> value option the type of the second `exp` is so constrained as to eliminate (a) the need for the separate `value` type and (b) the possibility of failure: val interpret : 'a exp -> 'a let interpret = function | Int i -> i | Bool b -> b | Add (i1, i2) -> interpret i1 + interpret i2 | Neg i -> - (interpret i) | Ifte (c, t, e) -> if interpret c then interpret t else interpret e | Lte (i1, i2) -> interpret i1 <= interpret i2 Such a construction is known to be type-error free because GADTs allow us to ensure that type constructors follow certain type equations and it's possible to write such a clean evaluator because GADTs keep around enough type information so that the compiler can "trust" them. Finally, the short answer of how they work is something like they interpret a constructor like Ifte : bool exp * 'a exp * 'a exp -> 'a exp as one with some existential types Ifte : ... | 'x exp * 'a exp * 'a exp 'a ex and some type equalities Ifte : 'x == int | ... then when typechecking it just has to collect all the unique new type variables and solve the system of equalities which arises. [0] Yeah, the author pooh poohs at examples like this, but I think they're really particularly clear.
mercurial 12y ago
It would have been interesting to get actual performance numbers with the article.
- throwaway000002 12y ago
  The specific performance aspect is, essentially, immaterial. The idea, in over-simple terms, is say you have Foo<T> but for say T=X there is a faster specialized way to implement Foo<X>, well you can do this in the type system of Ocaml via GADTs and still write generic type-safe code for Foo<T> and the compiler does the right thing when when it happens that T=X.(+) So you get to have your cake and eat it too. (+) without brittle, verbose, horrific re-factoring required to do similar things in simpler type systems.
  - kragen 12y ago
    Yes, having a faster specialized way to implement Foo<X> is great. But the reason it's great is "the specific performance aspect". If the cost of using the faster specialized way is, say, massive interpretive overhead, then it may not actually be faster, and then there's no reason to use it. GADTs actually seem to go in the other direction, though — they seem to enable the compiler to prove more at compile-time and thus generate code with less run-time tag checking. But some hard performance numbers would go a long way toward proving that.
    - mercurial 12y ago
      Especially since GADTs don't do too well with type inference. My take on "premature optimization is the root of all evil" is that I will take any "cheap" premature optimization which doesn't impact readability, but I'd like to be sure there is an actual performance improvement first.

120 points by michaelochurch 12y ago

GADTs are http://en.wikipedia.org/wiki/Generalized_algebraic_data_type http://en.wikipedia.org/wiki/Generalized_algebraic_data_type

marktangotango 12y ago
Upvoting, so obnoxious of the author of the post to not define them.
- deleted 12y ago
  [deleted]
- adultSwim 12y ago
  I can't tell if you are serious or not. OP goes through them by example. Original type: type 'a t = | Array of 'a array | Bytes of bytes GADT'd (same functionality as before): type 'a t = | Array : 'a array -> 'a t | Bytes : bytes -> 'a t Now using power of GADT to add constraint: type 'a t = | Array : 'a array -> 'a t | Bytes : bytes -> char t Just jumping into it seems like a fine choice to make. Allows for a (narrow) introduction to GADTs without getting bogged down in their full complexity/limitations. Shows that it's useful before/without a theoretical discussion. Still, I wouldn't have minded a little discussion introducing GADTs.
  - AceJohnny2 12y ago
    In the original version of the article (when I wrote my comment), the author hadn't defined them.

kragen 12y ago

I'm still not quite sure what GADTs are (after skimming the WP article, reading this article, and skimming the code in it) but very surprisingly to me, it looks like OCaml's GADT implementation tackles a lot of the memory fragmentation problems that come with object-graph-heap memory-model languages like Lisp, Python, Java, previously OCaml, JavaScript, and so on, in exchange for a little more type declaration overhead. (Although, in my small experience, debugging OCaml type errors usually involves adding some redundant type declarations anyway.) This is really interesting and I hope I understand it someday soon!

tel 12y ago
Generalized Algebraic Data Types, GADTs, are algebraic data types which include both (a) existential types and (b) type equalities. The combination allows for a certain kind of interaction between the specific kind of value within a type and the type itself. For instance, we might have a little expression language using normal ADTs [0] type exp = | Int of int -- integer constants | Bool of bool -- bool constants | Add of exp * exp -- addition | Neg of exp -- negation | Ifte of exp * exp * exp -- if then else | Lte of exp * exp -- less than or equal to but there's no particular guarantee that a value of `exp` is well-typed. For instance, the following is a valid value of `exp` let x : exp = Add (Int 3, Bool true) GADTs allow us to fix this situation by reflecting the type of the expression value into the type of the expression. Here's some syntax type _ exp = | Int : int -> int exp | Bool : bool -> bool exp | Add : int exp * int exp -> int exp | Neg : int exp * int exp | Ifte : bool exp * 'a exp * 'a exp -> 'a exp | Lte : int exp * int exp -> bool exp The way to read this syntax is to see it as giving the "type" of each constructor. Not only do we now parameterize the `exp` type with an index type corresponding to the type of the value this expression denotes, we also create very non-trivial type equations like Ifte : bool exp -> 'a exp -> 'a exp -> 'a exp and Lte : int exp -> int exp -> bool exp The upshot is that while the type of an interpreter for the first exp would have to look like type value = VInt of int | VBool of bool val interpret : exp -> value option the type of the second `exp` is so constrained as to eliminate (a) the need for the separate `value` type and (b) the possibility of failure: val interpret : 'a exp -> 'a let interpret = function | Int i -> i | Bool b -> b | Add (i1, i2) -> interpret i1 + interpret i2 | Neg i -> - (interpret i) | Ifte (c, t, e) -> if interpret c then interpret t else interpret e | Lte (i1, i2) -> interpret i1 <= interpret i2 Such a construction is known to be type-error free because GADTs allow us to ensure that type constructors follow certain type equations and it's possible to write such a clean evaluator because GADTs keep around enough type information so that the compiler can "trust" them. Finally, the short answer of how they work is something like they interpret a constructor like Ifte : bool exp * 'a exp * 'a exp -> 'a exp as one with some existential types Ifte : ... | 'x exp * 'a exp * 'a exp 'a ex and some type equalities Ifte : 'x == int | ... then when typechecking it just has to collect all the unique new type variables and solve the system of equalities which arises. [0] Yeah, the author pooh poohs at examples like this, but I think they're really particularly clear.

mercurial 12y ago

It would have been interesting to get actual performance numbers with the article.

throwaway000002 12y ago
The specific performance aspect is, essentially, immaterial. The idea, in over-simple terms, is say you have Foo<T> but for say T=X there is a faster specialized way to implement Foo<X>, well you can do this in the type system of Ocaml via GADTs and still write generic type-safe code for Foo<T> and the compiler does the right thing when when it happens that T=X.(+) So you get to have your cake and eat it too. (+) without brittle, verbose, horrific re-factoring required to do similar things in simpler type systems.
- kragen 12y ago
  Yes, having a faster specialized way to implement Foo<X> is great. But the reason it's great is "the specific performance aspect". If the cost of using the faster specialized way is, say, massive interpretive overhead, then it may not actually be faster, and then there's no reason to use it. GADTs actually seem to go in the other direction, though — they seem to enable the compiler to prove more at compile-time and thus generate code with less run-time tag checking. But some hard performance numbers would go a long way toward proving that.
  - mercurial 12y ago
    Especially since GADTs don't do too well with type inference. My take on "premature optimization is the root of all evil" is that I will take any "cheap" premature optimization which doesn't impact readability, but I'd like to be sure there is an actual performance improvement first.