This is my first post in a series intended to draw programmers from outside the functional programming sphere into dependent typing, by showing off ways that dependent typing can be used to build ergonomic and misuse-resistant APIs in ways that would typically require macros in languages with less powerful type systems.
My target audience is still a bit vauge for this series, currently I’m targeting systems programmers that have decent experience with strongly typed languages, rust comes to mind since I’ve worked extensively in it personally, and has maybe tried haskell and gotten burnt by it.
Feedback is appreciated, I’m interested in hearing about how I can make posts like this more approachable to people with other backgrounds, and I’m also very interested in seeing examples of macros people would like to see disappear into the type system.
How strong is the compile time / run time phase separation in Idris?
Could this technique work with format strings that are chosen at run time, with the type system ensuring that the strings are compatible? (Assuming format strings come from a limited set that is fixed at compile time.)
For Idris 2, that’s a tricky one to answer extensively, I’ve got a whole several posts planned out explaining that. One of 2’s unique features among dependently typed languages, even counting Idris 1, is it’s integration of linear types, which are very similar to the affine types of rust’s ownership, but used for a totally different purpose of controlling the spill over between compile time and run time. Idris 2 has a rather expressive sub language, so to speak, for explicitly encoding the relationship between compile time and runtime.
For the second question, that wouldn’t be difficult, and I’ll probably getting around to covering something like that sooner or later, but basically you just need to write a function that “decides” (produces a proof of equality or a proof of inequality at runtime) whether or not the type signatures produced by two format strings are equal, and then you can pretty easily write up a procedure that reuses printfFmt to make a function that checks two format strings for compatibility at runtime, and then uses the types from the first to accept arguments for the latter. I may actually end up writing that as an addenda to this post.
I realized that the specific case you were asking about (where the format strings come from a limited set that is fixed at compile time) is actually basically trivial, so I’ve gone ahead and written a little addendum to the post showing that off.
I still think I’ll write another addenda later on that covers the case where the format string is generated at runtime and checked, at runtime, against a template format string for type compatibility, but that’s going to require some slight refactoring to make the implementation short enough to be suitable for tacking onto this blog post.
I like the sound of this, but note that it is disapproved here to have one’s own work be 25% or more of one’s submissions. Try to submit some other things that you find interesting before the next part of this series.
This is a common misconception of the rule. You can’t ignore the purpose of the rule and skip straight to the rule of thumb.
The purpose of the rule is:
Self-promotion: It’s great to have authors participate in the community, but not to exploit it as a write-only tool for product announcements or driving traffic to their work.
Writing high-quality educational content like this isn’t automatically “self-promotion” just because it was submitted by the author. It also doesn’t automatically become self-promotion based on ratios. Self-promotion is a type of spam, where spam is defined as frequent low-quality/unwanted content. The rule of thumb is just a way to detect the symptoms of self-promotion but cannot diagnose it alone.
Huh. For what it’s worth, I commented as I did because I figured someone would say it was against the self-promotion rule and I preferred to have the message delivered in what I thought would be a supportive, constructive way by a fellow admirer of dependent typing (me) rather than maybe in a more discouraging way by someone who disdains dependent typing.
FWIW, C++ now has a type-safe printf replacement, std::format. It’s done using variadic templates. I implemented my own simplified equivalent last year, which was a fun exercise because I’m not a real template expert! Fortunately concepts and consteval functions made it a lot easier.
C++ templates are in a really wild category here, I personally very much consider them macros, but, there’s actually an argument to be made for considering the C++ template language to be dependently typed, if you consider compile time it’s “runtime”, but that’s a whole can of worms of its own.
I understand that C++ templates are very messy from a PLT perspective, but it would be inaccurate to consider them macros, they’re too deeply integrated with the “object language” to meaningfully be called macros. As an ex-C++ programmer with a lot of functional programming experience afterwards, I think most PLT folks are making a big mistake by not looking closer at what C++ templates got right among all the things that it obviously got wrong.
Maybe this is a bit of a gap in our definitions of “macros”, but I personally don’t think there is such a thing as being too deeply integrated with the “object” language for something to be meaningfully considered macros. Lots of modern macro systems end up deeply entangled in with the host language, in the quest for hygiene, and I also consider idris’s elaborator reflection to be macros, and it’s what the C++ template language wishes it could be in terms of integration with the host language.
I would say the way I implemented it is more on the dependent-typing side, to the extent that I understand the term. While parsing the format() call,
each arg’s type is mapped to an enumerated constant, which goes into a compile-time array that’s passed to the internal format() function
each arg is wrapped in a function that converts it to a type that can be passed through C varargs, e.g. the function for std::string calls c_str() to convert it to a C string pointer.
C++ now has a type-safe printf replacement, std::format.
I’m not sure it’s even “now” anymore. std::format has been provided in the standard library since C++20, and fmt::format has provided compile-time argument checking back to C++14, an eleven-year old language !
“Since C++20” doesn’t mean “since 2020” unfortunately. As of a year ago std::format was still giving me trouble in Clang/libc++ (not the latest one but whichever one Xcode ships.)
And adoption is slow in C++. It seems a lot of projects still haven’t moved past C++11 features [citation needed].
I mean, on macOS you can disregard the vendor’ old clang and use for instance a homebrew-shipped clang which will be up-to-date. I always find it weird to judge a language by how it’s shipped by Apple / Microsoft / Ubuntu… - by that measure Idris does not exist as a PL.
Likewise, people who aren’t using c++20 are likely not going to jump ship to Idris mainly because the kind of magical features a dependent-typed language brings is usually what they don’t want.
I doubt it’s the majority though, every c++ poll from a few years ago already showed c++11 already being quite towards the end of the bell curve of standard adoption: https://www.jetbrains.com/lp/devecosystem-2023/cpp/
I’m sure there are some corners that haven’t gotten past C++11, but I don’t think it’s particularly common. Even in old industry code bases upgrading to newer standards is rarely an issue unless some weird platform/toolchain needs to be supported. (Maybe some highly regulated industries too, where upgrading compilers is a lot of paperwork? I don’t touch that too much)
At work our move to C++20 was complicated by the need to support some older versions of CentOS. I don’t remember the details, but our Linux guy was cursing about it. Something about not supporting GCC 12, or glibc/libcpp being too old?
That’s strange too, CentOS is actually very nice for recent compiler support. You can use gcc-toolset-12 on CentOS 7 (released 11 years ago) and gcc-toolset-14, the latest, on CentOS 8.
This is my first post in a series intended to draw programmers from outside the functional programming sphere into dependent typing, by showing off ways that dependent typing can be used to build ergonomic and misuse-resistant APIs in ways that would typically require macros in languages with less powerful type systems.
My target audience is still a bit vauge for this series, currently I’m targeting systems programmers that have decent experience with strongly typed languages, rust comes to mind since I’ve worked extensively in it personally, and has maybe tried haskell and gotten burnt by it.
Feedback is appreciated, I’m interested in hearing about how I can make posts like this more approachable to people with other backgrounds, and I’m also very interested in seeing examples of macros people would like to see disappear into the type system.
How strong is the compile time / run time phase separation in Idris?
Could this technique work with format strings that are chosen at run time, with the type system ensuring that the strings are compatible? (Assuming format strings come from a limited set that is fixed at compile time.)
For Idris 2, that’s a tricky one to answer extensively, I’ve got a whole several posts planned out explaining that. One of 2’s unique features among dependently typed languages, even counting Idris 1, is it’s integration of linear types, which are very similar to the affine types of rust’s ownership, but used for a totally different purpose of controlling the spill over between compile time and run time. Idris 2 has a rather expressive sub language, so to speak, for explicitly encoding the relationship between compile time and runtime.
For the second question, that wouldn’t be difficult, and I’ll probably getting around to covering something like that sooner or later, but basically you just need to write a function that “decides” (produces a proof of equality or a proof of inequality at runtime) whether or not the type signatures produced by two format strings are equal, and then you can pretty easily write up a procedure that reuses
printfFmtto make a function that checks two format strings for compatibility at runtime, and then uses the types from the first to accept arguments for the latter. I may actually end up writing that as an addenda to this post.That linear type machinery sounds interesting! I’ll look out for your future articles, thanks!
I realized that the specific case you were asking about (where the format strings come from a limited set that is fixed at compile time) is actually basically trivial, so I’ve gone ahead and written a little addendum to the post showing that off.
I still think I’ll write another addenda later on that covers the case where the format string is generated at runtime and checked, at runtime, against a template format string for type compatibility, but that’s going to require some slight refactoring to make the implementation short enough to be suitable for tacking onto this blog post.
I like the sound of this, but note that it is disapproved here to have one’s own work be 25% or more of one’s submissions. Try to submit some other things that you find interesting before the next part of this series.
This is their first ever submission. You can’t extrapolate a trend of only posting their own things from a single submission.
This is a common misconception of the rule. You can’t ignore the purpose of the rule and skip straight to the rule of thumb.
The purpose of the rule is:
Writing high-quality educational content like this isn’t automatically “self-promotion” just because it was submitted by the author. It also doesn’t automatically become self-promotion based on ratios. Self-promotion is a type of spam, where spam is defined as frequent low-quality/unwanted content. The rule of thumb is just a way to detect the symptoms of self-promotion but cannot diagnose it alone.
Huh. For what it’s worth, I commented as I did because I figured someone would say it was against the self-promotion rule and I preferred to have the message delivered in what I thought would be a supportive, constructive way by a fellow admirer of dependent typing (me) rather than maybe in a more discouraging way by someone who disdains dependent typing.
FWIW, C++ now has a type-safe printf replacement, std::format. It’s done using variadic templates. I implemented my own simplified equivalent last year, which was a fun exercise because I’m not a real template expert! Fortunately concepts and consteval functions made it a lot easier.
C++ templates are in a really wild category here, I personally very much consider them macros, but, there’s actually an argument to be made for considering the C++ template language to be dependently typed, if you consider compile time it’s “runtime”, but that’s a whole can of worms of its own.
I understand that C++ templates are very messy from a PLT perspective, but it would be inaccurate to consider them macros, they’re too deeply integrated with the “object language” to meaningfully be called macros. As an ex-C++ programmer with a lot of functional programming experience afterwards, I think most PLT folks are making a big mistake by not looking closer at what C++ templates got right among all the things that it obviously got wrong.
Maybe this is a bit of a gap in our definitions of “macros”, but I personally don’t think there is such a thing as being too deeply integrated with the “object” language for something to be meaningfully considered macros. Lots of modern macro systems end up deeply entangled in with the host language, in the quest for hygiene, and I also consider idris’s elaborator reflection to be macros, and it’s what the C++ template language wishes it could be in terms of integration with the host language.
I would say the way I implemented it is more on the dependent-typing side, to the extent that I understand the term. While parsing the format() call,
I’m not sure it’s even “now” anymore. std::format has been provided in the standard library since C++20, and fmt::format has provided compile-time argument checking back to C++14, an eleven-year old language !
“Since C++20” doesn’t mean “since 2020” unfortunately. As of a year ago std::format was still giving me trouble in Clang/libc++ (not the latest one but whichever one Xcode ships.)
And adoption is slow in C++. It seems a lot of projects still haven’t moved past C++11 features [citation needed].
I mean, on macOS you can disregard the vendor’ old clang and use for instance a homebrew-shipped clang which will be up-to-date. I always find it weird to judge a language by how it’s shipped by Apple / Microsoft / Ubuntu… - by that measure Idris does not exist as a PL. Likewise, people who aren’t using c++20 are likely not going to jump ship to Idris mainly because the kind of magical features a dependent-typed language brings is usually what they don’t want.
I doubt it’s the majority though, every c++ poll from a few years ago already showed c++11 already being quite towards the end of the bell curve of standard adoption: https://www.jetbrains.com/lp/devecosystem-2023/cpp/
I’ve been reluctant to install a newer Clang, tbh. Will it have the same Apple-specific bits as the one in Xcode, and compatible libc++ headers?
I had issues with it a decade ago but since then I’ve seen a few software successfully shipped on macOS with a custom-compiled clang.
I’m sure there are some corners that haven’t gotten past C++11, but I don’t think it’s particularly common. Even in old industry code bases upgrading to newer standards is rarely an issue unless some weird platform/toolchain needs to be supported. (Maybe some highly regulated industries too, where upgrading compilers is a lot of paperwork? I don’t touch that too much)
At work our move to C++20 was complicated by the need to support some older versions of CentOS. I don’t remember the details, but our Linux guy was cursing about it. Something about not supporting GCC 12, or glibc/libcpp being too old?
That’s strange too, CentOS is actually very nice for recent compiler support. You can use gcc-toolset-12 on CentOS 7 (released 11 years ago) and gcc-toolset-14, the latest, on CentOS 8.
It might be CentOS 6 we still have to support?
It has been EOL for 5 years already, thus, my condolences !