Final code (if you want to skip the video): https://gist.github.com/puffnfresh/11202637
Stories with similar links:
- Idris: Type safe printf via puffnfresh 9 years ago | 14 points | 6 comments
Final code (if you want to skip the video): https://gist.github.com/puffnfresh/11202637
Got this link from an article posted on this website. Sorry if you already seen that, but I think this is a great showcase for dependent types.
Hi thanks but I’ve already seen it :)
Ocaml does this with GADTs, AFAIK.
Nice, I really need to look at Ocaml: Haskell GADTs cannot express that. (Plus: I am french, looks like I should at least acknowledge INRIA’s great work, I miss patriotism here :) )
Out of curiosity, what would be the Ocaml type signature for the interpFormat function?
I’m not sure exactly, but here is a slidedeck on how Printf works in Ocaml once it was moved to GADTs:
https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-gadts.pdf
EDIT: Sorry that’s not a slide deck it’s a short paper. And I think the Ocaml versions still requires the compiler to do some preprocessing, but now it turns it into what you would have to write by hand for the GADTs to work rather than doing all of the formatting type check logic in the compiler.
Thanks for the link.
The actual source code seems to be here: https://github.com/ocaml/ocaml/blob/trunk/stdlib/camlinternalFormat.ml#L57
Once again, I am a rookie using OCAML (I just used back when I was a student to be honest). I spent 20 minutes on it and still don’t fully understand this code. In conjunction with the paper you sent, this looks like more like a macro system looping-back to the type system right? I think the same kind of trick is used by the Haskell singletons library (for nick, here’s the associated papers :) ).
In this Idris example, the “computations on the type level” is performed out of the box without the need of any workaround. That’s the part I found very neat, looks like way more usable than what I saw so far.
But again, I’m not an expert on dependent types and never used them in the real world. Maybe @puffnfresh could confirm or infirm that.
Yeah, that’s completely right. Idris doesn’t have anything in the compiler about printf, you can do meta programming because you can write types depending on values.
The point of the video is not to extend Idris with a type-safe printf, the point is that you don’t have to extend Idris.
Thanks. I liked the paper form better since it had a detailed description of the problem, a few solutions with pro’s/con’s, and then the final one. Might come in handy when bootstrapping systems considering different ways to handle functions like printf.
[Comment from banned user removed]
[Comment removed by author]