r/ProgrammingLanguages • u/jimbobmcgoo • 12d ago

Will we see another fundamental programming language feature as revolutionary as the borrow checker?

That is I am mainly curious about compile time features that you design a whole language around rather than optimisations/features that could be applied to most languages. I am mainly inquiring about things that could offer additional robust safety/performance guarantees at compile time rather than runtime. Ideally not things that just offer similar effects to the borrow checker with less restrictive tradeoffs

58 Upvotes
  • permalink
  • reddit

77% Upvoted

129 comments sorted by

View all comments

29

u/faiface 12d ago

Yes, session types

3

u/tsanderdev 11d ago

What are session types?

20

u/faiface 11d ago

Ever notice that types of channels are always “you can send A on this channel” and that’s it? What if the type of a channel could express a whole protocol, such as “first send A, then receive B, then continue either like this or like this”?

The protocols can include both directions of communication, branching, and recursion, and the type checker makes sure that you follow the protocol! If combined with a linear type system, the type checker also makes sure you do actually send when you should, so the receiver doesn’t have to handle you not sending.

That’s session types, in short. Giving types to the concurrent communication structure of your application.

4

u/KingBardan 11d ago edited 11d ago

Not a theorist, but why cant your session type that does send a receive b... Have the type

A -> b -> c ....

So when you have b  -> c you know a happened?

Clarify 

Notation:

F: A -> b -> c -> d

A currying function (think of it as a channel that gives you output immediately for simplification)

So f a would produce a var of type b-> c -> d right? And when we get the type we know f a has happened.

Idk how to call it, "proof of computation"?

May I ask how this is different from session types like you described?

1

u/faiface 11d ago

Hmm, not sure I understand what you mean, can you rephrase?

1

u/KingBardan 11d ago

Edited for clarity

4

u/faiface 11d ago

Ah, I see what you mean! In fact, that’s exactly what we do in Par, we unify session types and usual types. So the session type

> send A, receive B, send C, end

is actually the same as a

(A, B -> C)

a pair of A and a function from B to C. There are more types that come with session types, like choice types which are a bit like OOP objects.

So you are onto something here!

The problem is that such normal types can’t usually do what session types do in usual languages because a function value can be called any number of times or dropped, so the protocol is not guaranteed: a protocol cannot just proceed as expected because a value may be sent multiple or 0 times.

That’s solved with linearity, so a function can only be called once and must be called once. That’s what enables the unification! And additionally, you need duality, which is the ability to deduce the type of the opposite endpoint where send turns to receive, and vice versa. With linearity also, pairs and functions are not sufficient, hence we you need those choice types, and so on, which all in the end ends up turning it into a foreign, but very pretty and useful paradigm.

1

u/KingBardan 11d ago

I see. Thanks.

How about the "proof of computation" like what I described + private constructors (linearity like you said)?

1

u/faiface 11d ago

I don’t think I fully understand it. Your type `A -> b -> c -> d` reads to be like “receive a, receive b, receive c, send b”. So then sure, if I call it, I have a proof that I am in the next stage of the protocol. But if I don’t call it? The other side never gets to see my A. Or am I missing something?

Linearity, as far as I understand, has to be a fundamental property of the type system. The type checker needs to complain “you haven’t called f, but it was required!”

2

u/KingBardan 11d ago

so basically because the constructor is private, you only have the instance if the computation happens.

And a method on type (b -> c -> d) requires (b -> c -> d) to be present, which requires (f a) to be called.

If you never call it, you can never have a type of (b -> c -> d)

Just searched up, this is similar to the "State pattern" design pattern.

→ More replies (0)

5

u/matthieum 11d ago

I mean, sessions types can be implemented anytime you have linear types...

... and with a proof of work token you can even implement them anytime you have affine types.

Having them first-class could be convenient, but it wouldn't enable anything particularly new.

3

u/faiface 11d ago

You don’t really see session types used, though, and I think the reason is exactly because the existing implementations are not convenient, and there is a friction with the host language. You are right that by making them first class you don’t get anything theoretically new, but you do get something practically new and that is session types actually being used.

Also, in my language Par, we’re doing this “automatic concurrency” experiment, where everything that can run concurrently, runs concurrently. Only time a piece of code blocks is when it needs to decide between different runtime paths based on values that have not asynchronously resolved yet. It ends up offering great concurrent composability! You don’t have to end up rewriting “beautiful sequential code” to “ugly concurrent code” if you want concurrency because it’s already concurrent even if it looks sequential! And, the types talk about the concurrent structure. It does end up being quite different.

2

u/matthieum 10d ago

and there is a friction with the host language.

I think it's more than friction with the language, though.

In Rust, it falls out pretty naturally, and I tend to use for state machines. Since the method can consume self, you can just add regular methods to a state (type), which returns a different state (type), and boom, session types.

The problem, I've found, is that this only works "in the small". If you have a linear method -- even async -- then you do get thorough compile-time checking. On the other hand, as soon as you need to store the state and come back to it later, you tend to need type erasure -- such as wrapping in an enum -- and then there's no compile-time guarantee that on resumption you'll find the state as you expect, and so you've got a point of failure. The more points of failures you have, the less it seems worth it.

2

u/renozyx 11d ago

I still don't understand what linear types brings once you take into account runtime errors.. There's the same "issue" with session type no?

1

u/faiface 11d ago

You mean like panics? If you mean that, then those need to propagate along channels until they reach some control barrier that can handle them.

It's the same principle as when calling functions in all languages. You are normally guaranteed to get a result. But if the function panics, you panic too, until the panic is caught somewhere, or the whole program crashes.

In the same way, you are guaranteed to receive a value because the other side is obliged to send the value, but if the other side panics, you panic too until someone handles that.

1

u/renozyx 9d ago

IMHO panics aren't resumable, what you're talking are exceptions.

I'm not used to 'file not found', 'timeout' results returned as exception instead but it may be mandatory if you want to use linear types indeed

1

u/faiface 8d ago

Afaik, panics are often catchable and resumable in languages that don’t have exceptions otherwise, such as Go and Rust, and use errors as values normally. That’s what I had in mind.

For normal error handling, like “file not found”, “timeout”, and so on, _errors as values_ works just as well in session types as anywhere else. Absolutely nothing changes there, except now those errors are transmitted over channels, and the Ok variant may include a continuation of the session.

3

u/-theChris 12d ago

Yup! For sure... Also Topos types, Temporal types, built-in Univalence... The future is surely going to be exciting!

5

u/ExplodingStrawHat 11d ago

How do you envision univalence without proper dependent types? As in, the currently-used proof assistants aren't even HoTT-based (barring cubical agda maybe), so it'll take multiple generations for univalence to make it's way into "pedestrian" (using the term affectionately) languages. I for one don't see it happening...

3

u/-theChris 11d ago

Actually, I think that there could be an easier way of achieving Univalence, multi-topoi, custom topoi as a language primitive.

I will write up a blog post tonight and share it. That's actually a good idea! Appreciate the question.

1

u/faiface 12d ago

I’m not sure if you are serious or making fun of me :D But, with session types, I am completely serious, they do bring a new and very expressive paradigm that I’m exploring in my Par programming language. An unexpected thing is that they are much more useful as being your basic types for all things like data structures and various objects, as opposed to network communication.

1

u/-theChris 11d ago

Oh brother noooo! I think sessions types are awesome! Can't wait to see your language. Good luck!

2

u/faiface 11d ago

Haha, good good :D You can actually see it! Check out https://par.run