Encode state transitions in types using linear types | Hacker News Reader

Encode state transitions in types using linear types

tweag.io

97 pointsyorwba35 comments

I really like the name "Linear Types" better than RAII. C++ ctor/dtor pairs are a sort of primitive linear type system that forces exactly one (implicit) use for each instance created.

Linear types nicely generalizes this so that we don't need RAII wrappers or whatever. Just produce values and pass them around, eventually to be consumed. It feels like this is a powerful language idea.

Rust uses a similar (but significantly weaker) system called "affine types" underlying its borrow checker.

> but significantly weaker

Just curious, could you expand on this? What makes it weaker? Is it that affine types allow either consuming or not consuming a type?

Exactly what you said -- it's not possible to make something that must be used exactly once. See https://gankro.github.io/blah/linear-rust/ for a deeper explanation.

You can't make a type that must be used exactly once, but you can often express that requirement in some other way. One technique is to require that some top-level function returns a value of the terminal type; then you can't accidentally abandon a computation part-way through. Here's a silly example:

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

That little DSL lets you make multi-layer burgers, but only where bacon and patties alternate, and there is a bun on the top.

Nit: Rust's affine type system is orthogonal to its borrow checker, rather than underlying it (though they're both crucial to Rust's system of memory safety, of course).

Would it be correct to say that the affine type system underlies the ownership paradigm?

Absolutely, I was just trying to avoid using "ownership" in my previous comment because it's more of an abstract concept than the type system and the borrow checker (which have concrete phases in the compiler, typeck and borrowck (though typeck also does more than just enforce linearity (er, affininity?))).

It's definitely not orthogonal. Mutable borrows require affine types.

Maybe not completely orthogonal, but I was thinking specifically of how treatment of immutable borrows show how one could partially tack on borrowing semantics to a non-linear/affine language for at least a modicum of use-after-free protection, and also it's a common misconception that linearity ("ownership") and the borrow checker are synonymous rather than distinct-though-intertwined concepts.

> how one could partially tack on borrowing semantics to a non-linear/affine language

How might that look if you tried to do this in, say a (not compatible with C) C-like language? I thought the ownership system (affine types) was required for the borrow checker to work.

> I really like the name "Linear Types" better than RAII.

They're not the same thing.

> C++ ctor/dtor pairs are a sort of primitive linear type system that forces exactly one (implicit) use for each instance created.

ctor/dtor are closer to what Rust provides which is an affine type system. Linear types must be used exactly once, affine types can be used at most once. You can initialise a C++ object and never use it, that would not be allowed in a linear type system.

I completely agree they're not the same things, but you can sort of see the "linear type" notion of "one and only one use" in RAII. Every construction has exactly one use (destruction.) it's fairly easy to see that RAII is a very limited version of a linear type system.

In an affine type system, every variable is used at most once. But C++ instantiations for RAII are not destructed more than once. Each instantiation has exactly one destruction.

> Every construction has exactly one use (destruction.) it's fairly easy to see that RAII is a very limited version of a linear type system.

Aside from actually having it integrated to the type system, Rust does exactly that. RAII is not linear.

> But C++ instantiations for RAII are not destructed more than once.

That's also what happens in Rust, it's not a linear type system.

> easy to see that RAII is a very limited version of a linear type system.

You might be interested in [0].

Affine logic rejects only the contraction rule [1]; unlike linear systems still has weakening [2].

[0]: https://en.wikipedia.org/wiki/Substructural_type_system

[1]: https://en.wikipedia.org/wiki/Idempotency_of_entailment

[2]: https://en.wikipedia.org/wiki/Monotonicity_of_entailment

I thought the "use" was the destruction or movement of the value, in which case an object is used exactly once.

You may never use a C++ object, but it will be destroyed (under normal circumstances).

> I thought the "use" was the destruction or movement of the value

Implicit behaviour is not use.

> You may never use a C++ object, but it will be destroyed (under normal circumstances).

And that is different from Rust how? https://gankro.github.io/blah/linear-rust/#must-be-used-at-l...

I don't know Haskell but this looks like Phantom Types in Scala.

Can anyone who knows both languages enlighten us ?

More on Scala Phantom types here https://gigiigig.github.io/tlp-step-by-step/phantom-types.ht...

    data State = Unbound | Bound | Listening | …
    data Socket (s :: State)

(s :: State) is a phantom type, yes.

I don't know Scala, but Phantom Types look like they only encode the state at the type level, but don't prevent you from copying e.g. the closed door before opening it, which would be undesirable if the state transition corresponds to a side effect.

Linear types can guarantee that the object participating in a state transition is not reused, which prevents accidentally referring to invalidated data.

This, exactly.

You can use phantom types to mark the difference between bound and unbound sockets, but you need the linear type system to prevent the unbound value from being used again.

Yes, those are phantom types. Many languages allow phantom types --- basically any language that has type parameters. So Haskell as we've seen, Scala as you point out, ML, Rust, etc.

That's not the interesting part, though. It's the linear types that are giving the guarantees here, and linear type systems are rare.

The short version, as I understand it, is this will enable the GHC Haskell compiler to validate state machines at compile time. Which is pretty awesome.

A tiny bit of model checking never hurt I guess.

Discussion of the previous post in the series: https://news.ycombinator.com/item?id=13866787

A linear type system isn't strictly necessary for this pattern; this is a common trick in Rust, which only has affine types: http://insanitybit.github.io/2016/05/30/beyond-memory-safety... . Indeed, it's lovely for validating state machines at compile time.

Rust can’t guarantee that a value is consumed exactly once.

This example creates a monad parametized over how many times a return value must be consumed. It has two settings: 1 (exactly once), and ω, which I’m prettying sure is the Greek abbreviation of “whatever” (zero or more times).

> Rust can’t guarantee that a value is consumed exactly once.

As far as I can tell this isn't relevant to the pattern being discussed though. All that matters is that a type can be consumed at most once, which is a capability provided by both linear and affine types. If you're worried about guaranteeing that the state machine ends gracefully (in this case, the socket being closed), then that's the role that destructors play. Indeed, the fact that destructors exist is what initially gives the impression of Rust having a linear type system; the only time that Rust doesn't guarantee exactly-once behavior (degenerating to at-most-once) is when the destructor leaks, which is pretty hard to do by accident (e.g. creating cyclical references in Rust is non-trivial).

For this specific state machine case though, an affine type system means you can't statically ensure the machine reaches a terminal state.

It seems as though one could have the transition to the terminal state return a unique type, and then execute the entire state machine inside a function whose return type is the return type of the terminal transition, yes?

Sure but now you can't really drive the state machine can you? The state machine has to drive you and provide callbacks for state transitions, something like that.

edit: ah I see you'd extract the entire manipulation in a function which would return a terminal type or union thereof, yeah that'd work I guess.

> ω, which I’m prettying sure is the Greek abbreviation of “whatever” (zero or more times).

Or it is the classical notation for the ordinal associated with the set of integers ℕ, aka any number of times.

the last element, as in the alpha omega perhaps.

I guess that’s also possible. I prefer my own explanation though, but then again I’m no mathematician.

Yup.

On the other hand, as an expansion of that pattern linear type system allows ensuring (statically) the state machine reaches a terminal state. With an affine type system you could just drop the computation halfway.

Reply on news.ycombinator.com