Type system for Query DSL with only simple GADTs: what typing judgments are needed?
Background
I have several F# codebases with reasonably high level of complexity of code. In order to convince myself that the code is solid I do whatever I can to write as much of it as possible type-driven and pure (up to what I am able to determine is pure without much help from the compiler) and unit test it like crazy (thanks, FsCheck & Expecto). The style that has got me the furthest within the infuriating constrains of F# is to use a command/query DSL. The queries take a shape like:
type Query<'a> =
| GetMyFoo of (Foo -> 'a)
| GetMyBarById of Guid*(Bar -> 'a)
| GetMeNBazs of int*(list<Baz> -> 'a)
and so on. Inevitable I want a functor instance. The queries grow large and the functor instance is very rote, making me long for deriving a la Haskell. More than that though, It doesn't feel like we have separation of concerns here, since we are mingling in the handler of the query results everywhere. I would really like to be able to represent a query not as a functor at all, but simply as a GADT, and have one canonical functor instance for a query paired with a handler (Idris syntax):
record HandledQry (q : Type -> Type) (a : Type) where
constructor HandleQry
qry : q i
handle : i -> a
whose functor instance I do not mind writing once. Or perhaps I would use a freer monad since the ideas from that paper resonate very much with this. The exact approach, whether to use HandledQry or a freer monad etc. is not the concern of this question; nor how to encode it into F#.
<PERSON>
I have an idea for how to encode simple GADTs in F#. However it does involve some localized exploitation of weaknesses in F#'s type system and some boilerplate code. 603
Given that unsoundness is an excellent way to give rise to bugs, I am not interested in handrolling this F# code: I would like to generate it from a small, specialized DSL, which supports nothing but a subset of GADTs, something like this (contrived syntax similar to Idris):
%given_type Foo
%given_type Guid
%given_type Bar
%given_type (List Baz)
data Query : Type -> Type where
| GetMyFoo : Query Foo
| GetMyBarById : Guid -> Query Bar
| GetMeNBazs : int -> Query (List Baz)
The idea is this. Existing F# types could be declared for use in the DSL as primitives, while being opaque to the DSL's compiler (it knows Foo : Type, and that is all). The DSL's compiler could make sure that the GADT it has been given is sound, and then generate F# code to use it, encapsulating the abuses of F#'s type system. However it is critical to me that the logic of the compiler be sound and based on type theory. To this end, I have been studying up on type theory. I am making progress, but it is a long road, and what we have here in my proposed DSL seems to be an odd mix of relatively few features, and yet those from a somewhat more advanced type system, with more basic features missing. I am not trying to build a full functional language right now and so what I am doing is a bit esoteric and unique.
It seems to me that we do not need:
* The lambda abstraction. The data constructors' type could be a function type, but functions, with bound parameters and bodies, never occur in any of the code I have as inputs or outputs of the queries so I am not interested in supporting them right now.
* (Full-on) dependent types. I have no idea how to encode a fuller version of dependent types into F#, nor do I have a need for them now (though as I understand it GADTs are a weak species of existential types).
* Product types (at least for starters). If the query takes multiple inputs, I can just use a curried function and translate it to e.g. int*string when I compile it to F#.
* Recursive or inductive types. Query should never have to reference itself and the other types are opaque.
* Parametric polymorphism. The cases of the query can always specific a concrete type for my purposes (and according to what I know how to encode in F#). 603