Towards generic programming in F#: thoughts on generalizing the earlier combinators over records and unions...
I wrote earlier a little post on combinators over records and unions. This approach in F# is still very attractive to me for defining various converters and serializers because it (1) uses no reflection and thus works in JavaScript via WebSharper out of the box; (2) gives the programmer full control to drop out of combinators anywhere where specific (more optimal, or custom) behavior is needed; (3) leans toward generic programming which has the potential to reduce code.
However, the approach, as presented, was overly specific, so point (3) remains on the TODO list. Code savings are only possible if you have N definitions that prove that datatypes are generic, and M definitions that prove that traits are generic, and from these you are able to derive every trait for every datatype. That is, the manual approach takes M * N definitions, and the GP approach takes M + N definitions. To make it possible, I need to find a way to generalize the combinators presented earlier.
If you look at Oleg's site, there is a nice article on first-class OCaml modules in relation to Generic Programming (GP). Of course, F# is incapable of any such thing. So GP proper seems out of reach.
One idea I had was to try modelling GP proper in Coq and extract to F#, but I did not get very far yet.
Another idea was to restrict the shape of the generic trait - this is obviously weaker than full-blown GP, but can still be useful. So instead of `g a` with abstracting over `g`, we fix `g` to be of a certain shape. For serializers we want this shape to have both positive and negative occurrence of `a`.
I got some success prototyping this in Haskell - the idea is to model in a purely functional setting (with monads) to make sure there model holds up, and then port back to F# functions, where, say, `a -> b` is understood as `a -> IO b`, and is itself a monad if we fix `a`: `type M x = a -> IO x`.
Here is the gist of it. I have a hunch that `Monad` is too strong when modeling the "reader" part and there should be a way to get by with `Applicative` only.
No comments:
Post a Comment