Rust's Type System Is Turing-Complete: Type-Level Programming in Rust
sdleffler.github.io
sdleffler.github.io
I agree with the author that while this is interesting, for users it doesn't matter much. In particular, the folks (with respect) pontificating about whether this is a good or bad thing are quite exagerating its consequences. In practice, you can neither conveniently use this property for metaprogramming, nor will you ever get a nonterminal typechecking (not only is there a recursion limit, it is extremely unlikely you will write the kinds of impls that hit that limit except in extreme typelevel programming like documented here).
The most interesting thing is that the two examples we have now of turing completeness both use only features available in Haskell without making typechecking undecidable. The reason our system is Turing complete is that we allow certain impls that Haskell wouldn't, which are in practice very useful.
For example, we have an impl of "ToString for T where T: Display" (in Haskellese "instance Display a => ToString a"); that is, anything that can be pretty printed also has a to_string method. This would be disallowed without the -XUndecidableInstances flag in Haskell. However, if your type can't be pretty printed, you can separately add a ToString impl for it (even with undecidable instances, Haskell wouldn't consider this coherent because Haskell coherence ignores constraints).
If you're interested, the exact sorts of impls we allow that Haskell wouldn't are covered by what's called the "Paterson condition" in Haskell docs.
What happens in rust closures have a unique type[1]. So the recursive call in cps_factorial, instantiates a new cps_factorial which contains a new unique closure type which instantiates a new cps_factorial...
[1] This is done so that closure calls can be determined statically reducing run-time overhead and helps optimisation.
Most likely there is something obvious I'm missing as I don't know a lot about rust, but unless the compiler isn't doing what is essentially a type level equivalent of tail call elimination, which it almost certainly does, finding the type of that function should be trivial unless the return type can become recursive with unbounded depth.
It doesn't, why would it? That's a pretty niche thing to have.
> finding the type of that function should be trivial unless the return type can become recursive with unbounded depth.
The return type is recursive with unbounded depth. The typechecker doesn't know the value of `n`, so to it this returns an infinitely recursive type.
Closures are statically dispatched. If you want something like this to work, you should box them as a trait object so that they get dynamically dispatched.
(The problem is solved by using a trait object to dynamically dispatch the inner call. https://play.rust-lang.org/?gist=0d3c0a5f1291eb34ba61bd39449...)
Although I'm pretty sure you can overload the Fn* traits to implement currying in Rust. (Fn traits are unstable). Which is neat.
// Something like this:
impl<F, A, B, R> (FnOnce(A) -> Curry<F, A, B>) for F
where F: FnOnce(A, B) -> R,
{ ... }
// and
impl<F, A, B, R> (FnOnce(B) -> R) for Curry<F, A, B>
where F: FnOnce(A, B) -> R
https://downloads.haskell.org/~ghc/7.0.1/docs/html/users_gui...
Getting to grasp logic programming would improve your skills, even if you never use Prolog again.
Use SWI-Prolog, one of the best free implementations out there.
It is debatable if Datalog is enough or if cuts et al are worthwhile.
I seldom use an ORM, I rather leave the work for the database engine.
My knowledge of PL/SQL, Transact-SQL, PL/pgSQL is way better than trying to make an ORM perform better.
Something like Dapper.NET or jOOQ are good enough for the remaining part of the work.
So the argument is that it is a similar eye-opening transition from ignorance to awareness.
"Writing custom type systems for Python in Prolog"
Example https://unify.ly5.ch/ (Caveat: it's an old implementation)
The best days are when Niko posts about his work on Rust. Always interesting and they often exploit the power behind ideas like "It's basically Prolog" instead of apologizing for it. It's exciting and the kind of thinking that makes me remember why I fell in love with programming in the first place.
Accidentally Turing Complete type systems are usually not all that pleasant in practice. Examples: C++ Templates, and now it seems, Rust.
EDIT: Just because people may not know this: A relevant quote by Alan Perlis: "Beware of the Turing tar-pit in which everything is possible but nothing of interest is easy." This applies to type-level programming as it does any type of programming.
EDIT#2: Also, look into Shen for a principled way to do this type of thing.
If instead I add to the mix prolog, (or a prolog interpreter?) this will help a lot, or not worth the effort?
There is also a F# implementation, https://github.com/palladin/logic
This code, for example, will never stop compiling in gcc 4.4.1[0]:
template<int I>
struct Infinite
{
enum { value = (I & 0x1)? Infinite<I+1>::value : Infinite<I-1>::value };
};
int main ()
{
int i = Infinite<1>::value;
}
As programmers, we can indeed write infinite loops. Why is it "a bad idea" if the loop happens at compile time rather than runtime? Why should we reduce the expressiveness of our language to avoid this possibility?
What next? Will we start seeing meta-metalanguages because, hey, it makes compilation less error-prone (but adds something we'll call pre-compilation)?
What is your proposed alternative to the Paterson conditions (described in the top comment)?
Because you need at least one reliable tool to tell you when there's a problem, and if that tool isn't a compiler, what are you left with? When do you realize that a long compilation is actually in an infinite loop and not simply a long compilation? How do you debug the cause of an infinite compilation?
These questions may have answers, but current compilers aren't designed to address them.
Even without turing-complete type systems, you can still make compilation take effectively forever. It's been a while since I tested, but by my recollection, creating a fixed-length array of sufficiently large size in Rust would make compilation hang indefinitely (well, for much longer than I was ever willing to let it run). Of course this particular behavior may have been fixed (or maybe not; I'm not in a position to test right now), but I'm sure there's other ways to produce artificially long compilation times as well.
Sure boss, I'll fix it. Would have fixed it already, if only nontermination wasn't the most unhelpful kind of compiler error message, ever...
Actually, I'd rather want a system that was really designed around this -- well, OK, maybe not TC[1], but perhaps Pacman Completeness.
[1] Purely to avoid decidability problems.
In the worst case, they just require way too much thought on behalf of users reading and writing the code. Amount up expressiveness often leads to type errors that are not very easy to understand, or lead to type errors that occur under very strange conditions.
Yeah, that's my impression too. TC doesn't actually require all that much. (Of course, making it pleasant is a whole 'nother matter.)
Just because a language allows for doing cool stuff, kind of newspaper quiz, doesn't mean we should write code daily like that.
It is up to us to make the better judgement, according to the team skills and project complexity, about what should be used.
People do that in C++ because C++ lacks some features they want, and goes a long time between updates.
Rust has many built-in metaprogramming features already, and regularly adds more. And if you have something you want to do and can't currently, you can file an RFC.
That makes me much less worried about people (ab)using type-level programming to implement weirdness.
It seems best that errors are caught at compile time
Thus, even in languages where metaprogramming is a prominent feature(e.g. most Lisps) the culture tends to evolve towards writing in a plain style and sparingly using these abilities because they have so much footgun power.
Now, it's possible that Rust's method of extension doesn't have the same capability to cause harm as something like macros, and is more along the lines of generic types, which have a narrower scope and are more in line with everyday needs. But everyone who's seen it happen is justifiably wary about a proclamation of "this time is different".
The most important goal for any programming language is that it is useful, i.e. it can express common patterns without hacks or kludges. Languages that are not useful tend to be forgotten.
However, chasing the dual goals of usefulness and soundness inevitably leads to type-system bloat. If "nothing is allowed unless explicitly permitted" and "everything must be somehow allowed" then it the list of things that are explicitly permitted will end up being very, very long.
You talk about writing a custom compiler / type checker -- this is exactly what unit tests are. Are you against those as well? What's wrong with integrating certain sorts of test into the source itself?
You can get absolutely phenomenal performance, but any major template capability has a high risk of becoming a DSL with terrible debugging ability and slow comprehensibility.
Judicious use could be very nice though...
[1] http://cs.stackexchange.com/questions/19577/what-can-idris-n...
Also, your link indicates idris's type system is Turing complete.
Totality precludes Turing-completeness. Specifically, functions that don't terminate are by definition partial, and if you can't express functions that don't terminate then it isn't Turing-complete.
In any case, saying that Haskell 98 is the One True Haskell(TM) isn't accurate. Almost all code (beyond the LYAH level) written today uses a few Haskell 2010 extensions, mostly for ergonomics (things like OverloadedStrings are a good example of this), not to mention all the extensions that make mtl let you write "lift whatever" instead of "lift . lift . lift ..." and infer how "high" you want to go up the monad transformer stack.
In C++11 you can pre-instantiate common used templates (extern template)and hopefully C++20 will finally get modules.
Until then, those that are able to use just VS C++ 2015 and 2017, can make use of incremental linking and experimental modules, to ease the pain a bit.
Thanks for the obvious point that rust isn't agda. However, certainly you can agree that agdas type system is able to capture a strictly greater set of constraints than a typed language without a Turing complete type system
Same for Coq, and probably Idris.
[1]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...
Allocations can be removed just like in Rust thanks to uniqueness types:
http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
Also funny that you mention ergonomics, given that improving the current state is one of the main goals of 2017's roadmap.
Let's unpack that. You advocate using non-Turing complete languages for things that don't need it. Great. Something like DTrace does not need a Turing complete language and D isn't Turing complete. Awesome.
But then you say that if you're using a Turing complete language, what's wrong if the type system is Turing complete as well?
Well, does a Turing complete language, C or Rust, need or in any way benefit from a Turing complete type system? Does a low level systems language, C or Rust, need or benefit from a Turing complete language?
Other than an implementation pun, I don't see any point in this needless complexity. The point of a type system is safety. I don't see how a Turing complete type system gets you to heaven.
Unless I'm missing something, having Turing completeness in a type system doesn't mean it's less safe; it just means the type checker might not terminate. In which case, of course, the code will not compile and thus cannot do anything unsafe (of course the type checker itself might, say, allocate infinite memory and crash your machine... But that's a different story)
Do you believe in unit tests? Ultimately, this is using he taget language to type check itself. If you had a well integrated Turing complete type system (c++ does not), then you could start enforcing some of these at the compilation stage
Methinks you are defending pointless complexity. How did we ever write unit tests before this awesomeness was sprung upon us?
Hmm, I dunno about that. If you need to keep a collection of callbacks, that would most certainly be a collection of Fn/FnMut trait objects, that is this:
struct Thing {
callbacks: Vec<Box<FnMut(i32) -> i32>>
}
struct Thing<F> where F: FnMut(i32) -> i32 {
callbacks: Vec<F>
}
OP says "can also be used". It sure looks like the Fn trait is being used for dynamic dispatch in that example.
Metaprogramming is programming -- it's scripting the compiler, to produce code that is faster (at runtime) or catches more errors at compile time. But for some reason in C++, metaprogramming is written in a completely different language from everything else -- a functional language, but not a very good one. As a result, code that relies heavily on metaprogramming ends up inscrutable to most programmers.
Instead, we should embrace metaprogramming and allow it to be performed in a language that is similar to other code, so that we can understand it. Give the compiler an actual API and let me write code that calls that API at compile time.
(I don't know enough about Rust to know how well they've accomplished this.)
But Rust has a hygenic higher-level macro system that helps.
On top of that, Rust is getting procedural macros. Right now this is limited to `#[derive()]` macros, but we want it to cover all cases. This means that you can write a macro that runs arbitrary rust code at compile time.
(While it currently is limited to `#[derive()]` macros you can abuse the API to make it work for inline bang-macros as well)
There's also projects like ripgrep, alacritty, redoxOS, just off the top of my head. Dropbox and npm also come to mind.
You can also check out https://www.rust-lang.org/en-US/friends.html for a big list of companies that use Rust.
Edit: ah, further down in the article: "Smallfuck is a minimalist programming language which is known to be Turing-complete when memory restrictions are lifted."
How sad is it that a serious article for grownups has to put a disclaimer about a fucking word so that some flakes don't get offended? It's truly a sad state of affairs.
If you don't care about the disclaimer, it isn't for you, and you can ignore it freely.
You can complain that expiration dates on food should be removed, but using that to complain that people complain too easily is hypocritical.
It would only be imaginary/strawmen if the author (and us all) hadn't already seen the same complaining in hundreds of articles... As it is, it's merely pre-emptive...
"I'm all for cursing in private conversation with friends and such when it's appropriate - but why do people continue to think it's acceptable in public examples of work? Will this go on someone's resume like this? What will an employer think?"
https://news.ycombinator.com/item?id=12460640
"Reading through the comments I am glad I am not the only one who finds over the top profanity upsetting. Yes , the author is free to make his/her point any way they want to. and No, not everyone who thinks that this profanity is undue is a prude. and I dont think it is fair to make a culture or age characterization based on a user's response. Extreme or sometimes, any profanity changes the tone of the article. that alone is a good reason to avoid over the top proclamations. IMO the author comes across as loud and noisy , and not strong and forceful. Just like a stand up comedian, who says 'fuck' for every joke."
"potty mouth."
(and numerous other comments focusing on the use of "fuck" in the post)
https://news.ycombinator.com/item?id=5694173
"Was it really necessary to drop an F bomb to ask this question?"
Because it hit a nerve?
Anyway, as to the meta-point -- personally, I think it's fine to warn people of upcoming profanity, but it seems to fall kind of flat here. I mean, using the "fuck" in a warning about using the word "fuck" seems to sort of defeat the point of a warning. (Unless of course the writer is himself making a meta-point that I'm not seeing.)
People are different. A big part of the job of "not being an asshole" is recognizing this fact.
Given any two languages can do so then they are in fact, interchangeable.