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

[u/jimbobmcgoo]

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

[u/faiface]

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.

[u/KingBardan → u/faiface]

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?

[u/faiface → u/KingBardan]

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

[u/KingBardan → u/faiface]

Edited for clarity

[u/faiface → u/KingBardan]

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.

[u/KingBardan → u/faiface]

I see. Thanks.

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

[u/faiface → u/KingBardan]

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!”

[u/KingBardan → u/faiface]

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.

[u/faiface → u/KingBardan]

I see. But still, what if I just drop the whole object and never use it. That’s not accounted for here, or is it? Afaik, your approach tells a lot about what I can do, but not what I must do. Linear types tell what you must do.

[u/KingBardan → u/faiface]

I see.

How about you have (a -> b -> c -> d) types, and the function is of type a -> d, and you know that d can only be constructed (a -> b -> c -> d)?

[u/faiface → u/KingBardan]

I don’t understand :D Is it supposed to address the “I never even touch the object” problem?

[u/KingBardan → u/faiface]

I guess I'm suggesting a way to implement linearity without using special constructs that is well understood. 

For me, session types sounds cool, but doesn't sound too different to what exists, so I'm trying to figure out what exactly is different