3
$\begingroup$

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?

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.