Reasoning with Types in Rust | Hacker News Reader

Reasoning with Types in Rust

aaronweiss.us

162 pointsmiqkt22 comments

> A function of type fn<T>(T) -> T must:

> return its argument or

> panic or abort or

> never return

This confused me for a moment because I thought “why? it only says the return value must be the same type as the argument, not that it must have the same value”, but of course since the type can be anything there is no operation that is guaranteed to work that you can perform on the argument value. You can’t for example multiply by two because not all types will support multiplication by an integer.

The linked paper by Wadler (https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf) develops many more examples like this (e.g. "Figure 1: Examples of theorems from types").

Exactly. Welcome to the world of parametric polymorphism. Writing programs using those uninterpreted types are essentially proofs for logic by the Curry-Howard correspondence. It’s a fascinating topic.

Perhaps this is subverting the type-theoretic (in a CS sense) point being made, but in C++ you could quite reasonably write a function:

  template<typename T>
  T fn(T t){
      return t * 2;
  }

  fn(4.2); //fine
  fn("foo"); //fails

because the inability to multiply by 2 isn't a problem until an incompatible type parameter is instantiated. Is this not the case in rust?

Nope in Rust you can only do things with generic types that fit the constraints(called trait bounds in Rust) you've placed on them. So with no constraints you can only do things that every single type supports. In essence it's an implicit vs explicit trade off. C++ implicitly figures out the constraints on generic types whereas Rust requires you to be explicit about them.

Your example in Rust would be

    use std::ops::Mul;
    
    fn double<T: Mul<i32>>(a: T) -> T::Output {
        a * 2
    }
    
    fn main() {
        println!("{}", double(2));
    
        // Can't double &str because it doens't implement Mul<i32>
        // println!("{}", double("Hello"));
    }

https://play.rust-lang.org/?gist=ba8d6368a7fb997586b51580baa...

Also as the GP points out the above fact is crucial for the reasoning around to hold `fn<T>(T) -> T`. An example that breaks those rules is

    fn thing<T: Default>(a: T) -> T {
        T::default()
    }

That's because templates have no type-checking in C++.

Ideally, you wouldn't be able to do this with concepts, but I don't know whether that's true for the concepts that finally made it into the standard (i.e. I don't know if it would be an error to call a function or operator on an argument if that function isn't required in the concept specification.).

C++ templates have type checking after expansion, the type checking just isn’t modular.

I loved this post. It’s very readable and introduces some interesting concepts related to type safety and some potentially simple use case in the context of access to private data, guaranteed from a type pattern.

As was pointed out in the Reddit conversation about this [1], the parametricity (new word I learned while reading this last night), will be lost with specialization.

Personally I want specialization for all the joy it will bring, and I don’t see this as a huge loss, but I wonder what other people’s thoughts are on this?

[1] https://www.reddit.com/r/rust/comments/80eis2/reasoning_with...

To me, parametric polymorphism is much nicer for reasoning about a program locally / modularly. It's kind of like reasoning about a function with linear control flow vs reasoning about a function with lots of nested if/elses. You can do the reasoning once and be done with it.

I tried to make a general point along those lines in this blog post, thought I think it deserves more extensive examples. http://storm-country.com/blog/abstract-is-simple

The Secret example is basically just encapsulation. It reminds me of the HTML type used in Go's standard library to avoid XSS vulnerabilities in HTML templates due to lack of escaping. [1] Any string that's not cast using HTML() is considered unsafe and will automatically be escaped.

In practice, this is used to make security audits easier. It's not that you can't defeat the system, but security review only needs to look at all the places a string is cast to or from the HTML type and verify that they're in fact safe. This is considerably easier than it would be with bare strings, though better encapsulation would help. (In Go, this could be done with a struct that has a private field, but that's not what they did for some reason.)

This is an old trick, also used by GWT [2] and other languages. Language support for zero-overhead, encapsulated wrapper types makes this particularly convenient; otherwise you have to decide if the performance cost is worth it for a widely-used type.

[1] https://golang.org/pkg/html/template/#HTML [2] http://www.gwtproject.org/javadoc/latest/com/google/gwt/safe...

Along similar lines, a while back I took the time to migrate a bunch of Android code dealing with phone number strings in various levels of normalization into a handful of wrapper types that enforced it at the type level.

It didn't take long, identified several flaws in the process, and the instant feedback on misuse alone probably saved more time than it took to do the migration. And being able to implicitly get rid of the duplicate normalization we were doing probably ended up saving more CPU than we lost due to the increased indirection when doing this in Java. (phone number (re)normalization is really expensive, even compared to 1000s of other normal string operations).

I'm totally sold on wrapper types for this kind of thing.

You can write parametrically polymorphic code in pretty much any language that has a concept of polymorphism [1]. It's not difficult to avoid doing the things that violate it. The problem arises in that if your language doesn't guarantee it, you don't know what third-party code will do. Go by no means guarantees parametric polymorphism, for instance, and technically a wizard armed with "reflect" can do anything they want, but in practice you can get a lot of mileage out of it even if it isn't guaranteed.

I write a lot of networking code and one of the patterns I use a lot is to get a socket from something (connecting, accepting, whatever), do any socket-specific configuration I may need to do on the socket immediately, and then pass it to a function to do the real work that takes an io.Reader or io.Writer or whatever minimal interface it is I actually need. This has two major benefits: First, it makes it clear that the "real" code is only going to do certain things, and second, it makes the "real" code much easier to test because it's tedious and difficult to mock a real socket, but quite easy to pass something an io.Reader and ensure it does the right thing.

It's certainly not a new trick and it can be applied in a lot of existing languages, but as programming ideas go, it's still a relatively new concept to the programming gestalt community [2]. I expect to see this idea coming up more and more over the next 20 years; I wouldn't be surprised that on the cutting edge programming language side, it becomes as expected to have some form of enforced parametricity in your new shiny language as it is to have closures.

[1]: For the purposes of this discussion, dynamic languages have only one type, "Variant", and thus don't really qualify as polymorphic in this manner, despite their apparent extreme polymorphism.

[2]: Yes, it's a couple of decades old, but measured in person-years of understanding it is minuscule compared to the community as a whole.

I said it was basically the same thing, but a big difference is that we aren't using polymorphism, just encapsulation.

You don't need reflection to break parametricity. All you need is instanceof (in Java) or a type switch (in Go), and this is very common style since sum types don't exist and that's how we pattern-match. (Along with the visitor pattern.)

Parametricity seems to be when a language doesn't have these things; if you want to pattern-match on types, there needs to be a sum type or an operation that returns one.

It's not clear that programmers used to an object-oriented style will go along with the idea that downcasts are bad and should be forbidden. Is it worth removing a useful escape hatch (particularly in framework-heavy code) to gain an esoteric form of type-based reasoning?

But if you try Rust, you're fighting the borrow checker anyway, so perhaps this additional inflexibility isn't that noticable?

"You don't need reflection to break parametricity."

Correct; I cited reflect just because it lets you do anything; i.e., you can get a type you don't understand at all, and reflect can go groveling through the type to see if it can find an embedded type it does understand, or even directly muck about with unrelated struct values, or any other crazy thing. Type switching requires you to be able to name the types you're going to examine in advance; with reflect you can even do horrible things to types that didn't exist when you wrote the code.

But then, the answer is mostly not to do that. Go isn't academically pure, but neither is it full of people writing crazy code like that. And so, technically, you can't use this reasoning in Go... but even so, enough of it is there that I get some mileage out of it. I find my expertise in Haskell transfers in Go in some bizarre and unexpected ways, because while Go doesn't have much, Haskell taught me a lot about exploiting what is there to the maximum I can. Even though by Haskell standards haughty sniff Go is barely even a programming language (well I never!).

Site isn't very usable on mobile.

It works in my mobile !!

Agree, Brave on Android is unusable

Check out Firefox mobile's Reader mode

Does your mobile browser support CSS Grid? If it does and there's still an issue, I'd love to fix it.

Grid doesn't have great support on mobile yet.

I'm sure you want to stick with it, and aren't really interested in something else, but Grid only started getting solid support across all the main mobile browsers in January. Lots of mobile devices are stuck on older versions, because of vendors not releasing updates.

It's been supported on iOS for just about a full year now according to caniuse. Unfortunately, they seem to lack meaningful historical info about Android, but assuming some kind of feature parity between Chrome versions on mobile and desktop, should've been about the same time.

I will definitely stick with grid, but it does suck that people have mobile devices that still haven't gotten these updates after a year. :\

Excellent fucking article.

Reply on news.ycombinator.com