On Sun, Jun 17, 2018 at 8:39 AM Viet Le <vietlq85@gmail.com> wrote:

The use there is pretty good. In GraphQL you have a query language in which fields are bound to functions with arguments. Andreas (the GraphQL author) takes the graphql schema and uses a GADT to derive the correct type for said function. In short: the function will have the correct type and schema changes will require updates on the necessary functions.

But you could argue this is still within the bounds of PL:

GraphQL is a language

Their spec doesn't show it, but it is best implemented as such: have a statics phase and a dynamics phase, type check vigorously in the statics phase. Most of what they call "validations" are just standard type checking hygiene.  

Also, the types are moded/polarized in that certain types flows from the client to the server (which means you shouldn't trust the client) and other types flows from the server to the client (which means you shouldn't trust the server).

I have a hunch that there is a small core language within GraphQL best realized as a lambda-calculus (with added primops corresponding to execution of user-defined code). But I have yet to try implementing that.

---------

A use I've seen Janes St. doing is to use a GADT as a witness for a given implementation. This allows the programmer to define a generic implementation of, say 'a array, and then later specialize the bool array variant into a bitset on words, or a more advanced data structure where the bitset is a tree of some kind. The GADT then "selects" for the given implementation in the code base.