Type system for Query DSL with only simple GADTs: what typing judgments are needed?

Question

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#.

The Meat of It

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. 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#).
• The rest of an actual lambda calculus; I am only interested in defining types in this DSL (for now).
• I'm thinking that what I've got here is less than the full power of GADTs even in Haskell.

What I do need is:

• Sound type judgments, e.g. no Type : Type junk. This has been a stumblingblock in researching this; most intros to dependent types use Type : Type for ease (which I can understand in a tutorial) and I haven't found stuff to introduce just GADTs.
• At-least-somewhat-generalized algebraic data types.

I believe I am capable of translating whatever the rules are from the syntax of natural deduction into sound Idris code.

tl;dr

What type judgments are needed for a small type system that has only simple GADTs and primitive types?

Answer 1

Lennart Augustsson and Kent Petersson 1994 present syntax and type rules for a small functional language which is basically just lambda calculus with GADTs. They have two kinds of judgments, one to indicate that "the expression e has type T in the type environment $\Gamma$" and the other to indicate that "the declaration d generates the type environment $\Gamma$". Using the second they have rules for type declarations and declaration sequencing, i.e. rules giving the ability to define types. Using the first they define typing rules for expressions: variables, constructors, pattern matching, and application.

Note: The paper is marked as DRAFT and does not seem to be as rigorous as some, but nevertheless has much valuable material.