Brian McKenna posted an interesting video and gist on implementing a type safe printf in Idris with dependent types.
This led me down a nice little rabbit hole wondering if something similar could be achieved with an F# type provider.
With a bit of help from Tomas the final solution turned out to be surprisingly nice, although not quite so clean as the Idris original.
Taking the format string and parsing it looks very similar to the Idris version, what with the common ML history of the two languages:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
|
This might not be the most efficient or flexible parsing method, but that's not really the point of the current exercise and it's very clear what it's doing.
Next, we want to create a quotation that represents a curried function based on our format type. This is where I needed Tomas' help - it turns out there isn't any easy way to do this with the <@@ ... @@>
syntax I've usually used to build quotations for type providers.
Tomas reminded me that the Microsoft.FSharp.Quotations
namespace gives direct access to the underlying classes that represent the expression tree of the quotation. This allows us to build an expression tree recusively; check out Tomas' explanation of the technique for more details of how it works.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 |
|
That's the hard stuff out of the way! Now we just have some type provider boiler plate. We're going to provide a type provider named TPrint
which takes a single parameter (our format string). Once the parameter is supplied, we provide a single static property which is an FSharpFunc type which matches the signature required by the format string.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 |
|
So, put it all together and you get a type provider which allows you to do this:
1 2 3 4 5 |
|
So; nothing there that the built in printf
doesn't already do for you. But, this does start opening up some options for providing much more idiomatic F# style APIs then I've really seen so far from Type Providers, which tend to provide very OO style interfaces. Should be some interesting ideas in there to explore!
Full code can be found at Github.