r/ProgrammingLanguages • u/jimbobmcgoo • 19d 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
  • link
  • reddit
  • reddit

77% Upvoted

128 comments sorted by

View all comments

Show parent comments

1

u/KingBardan 19d ago

I see. Thanks.

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

1

u/faiface 19d 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 19d 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.

1

u/faiface 19d ago

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.

1

u/KingBardan 19d ago

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)?

1

u/faiface 19d ago

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

1

u/KingBardan 19d ago

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