Playing a bit more with generics, I stumbled upon some fairly compact combinators that can derive n-ary conjunctions from a binary conjunction. Here is a self-explanatory F# example (disregard the ugliness involved in F#'s lack of higher kinds, Haskell or OCaml code would not need this):
In case you are wondering about the Coq file in the gist: a good objection to this approach is efficiency. Instances computed in this way are not efficient at all. Just think of all the allocated tuples! It turns out, we can remedy the situation with automated program transformation. In F# it would involve computing over quotations or similar quoted forms. It is hard to get started since little support for optimizing those is available out of the box. In Coq there is more batteries. As you can see in the gist, Coq seems to tackle the above example trivially with the "compute" tactic, and derive an instance equivalent to a hand-written one.
No comments:
Post a Comment