I am looking for examples of business use cases for GADTs.
I understand that GADTs are a perfect match for small DSLs and their respective evaluators.
I know they can be used to encode run time type information (even thou this is much less clear to me).
But apart from this link (http://engineering.issuu.com/2015/09/17/gadt-practicalities.html) I have not found anything that describes GADTs in a more business like context.
So please share your application of GADTs in this context if you have (or links or whatever).
… at Jane Street we’ve found lots of examples where GADTs are important for performance, of all things. The theme in these examples is that GADTs enable you to tweak your memory representations in ways that would otherwise be painful or impossible to do safely in OCaml.
Sure, I know this blog as well.
My question thou is geared more towards conceptual aspects of using GADTs.
As Yaron says: "…GADT examples all seem to be about the kinds of things that compiler writers do, like embed domain-specific languages or build typed abstract-syntax trees. "
Sure he does explain that. However the example in that blog is a pretty technical one with the necessity to solve a deeply technical issue. I am somehow looking for more abstract / conceptual examples.
Its hard to explain but lets say I read the GOF (pattern) book and I read about the “Adapter” pattern then I would find examples to use that in a pretty technical context (for example TCP/IP => Token-ring conversion) but most likely also an example on how to adapt an SEC securities system to crypto currency system. And thats what I am looking for
Perhaps you should explain more about your goal. Are you trying to make a business case for using OCaml for a project, for example? If so, I wouldn’t discuss GADTs as that is getting too deep into the weeds I think.
I have no idea what you are looking for exactly, but maybe this might be of interest to you: https://www.michelson-lang.com/why-michelson.html The smart-contract language implemented in Tezos is using GADTs to let the OCaml typechecker do a lot of verification of the contracts before they are even executed.
What business aspects are you looking at? The main concept with GADTs is to encode more invariants into the types than with typical ADTs, so you can wrote both safer and faster code.
In general I’d say one use case of GADTs is when you already have a regular ADT (aka a sum type), but in a lot of places, when you pattern match on it, you rely on runtime invariants to ignore some cases (i.e you have a lot of match ... with ... | _ -> assert false ). Some times, in these cases, GADTs can help you encode the runtime invariants into the type and help you get rid of these annoying | _ -> assert false.
At Citrix one of our Architects , ping @jonludlam ;), had a PoC database implementation with any kind of safety guarantees, all based on GADTs. I really hope he will publish the exploration writeup at a certain point, it was very interesting and great fun!
