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 useType : 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?