Types and Safety

[e-dant]

Linear and affine types solve parts of the resource safety problem.

Dependent types solve parts of the type safety problem.

Programming has a bit of an issue with “big fancy words.” I don’t mean for this to come off as a “look at this fancy thing.”

Affine types, a big part of Rust’s type system, help real programmers write correct programs daily.

Linear types solve a trade off with affine types: that the value, or resource, might not be used.

Dependent types help prove that the programs we write work correctly on more kinds of input by allowing more logic in the type system.

Has thought been put into adopting or enabling one or more of these approaches in the type system?

[geoffromer]

Carbon will support move-only types, which will allow an approximation of linear/affine typing much like in C++ and Rust. We have occasionally looked at dependent typing in various contexts, but so far we've avoided it. "More logic in the type system" is a double-edged sword, because it makes it harder (or even impossible) to decide when two types are equal.

[e-dant]

I think equivalence proofs would be a part of a dependent type system. The language from "A Little Typer" doesn't allow recursion.

IOW It's a constrained logic.

Anyway, I'm happy to hear that move-only types will be supported.

It would be wonderful to have a type system that allowed the programmer to implement move-only types themselves -- and maybe other things, too!

Consider a move-only type that requires some other operation (a "destructor" for example) to be called when it's being moved-from. Specifying that behavior would either require a specific change from the language for that purpose, or a more generic type system.

Food for thought.

Side note, are move-only types actually Kinds?

[e-dant]

(There are more answers to that example problem than I could count. What I meant was that one solution is leaving a spot open in the type system for "types that transfer ownership but call some particular function before they do" with the benefit that runtime-errors are turned into compile-time error messages.)

[Kubiyak]

I didn't realize this discussion existed earlier and its related to a q I posted.
Is it possible to restrict taking references/pointers to specially designated types? For example as an API designer I don't want end users taking references or pointers to handle types (smart pointers) returned by the API.

I will be very interested in Carbon if there is such a feature.

One of the main issues in C++ is that even a well designed API can become a failure due to misuse. The realities of the corporate landscape is that mistakes = outages = lost revenue. In that landscape it doesnt matter whether an API caused a fault or if its misuse caused a fault. It's the same thing.

I am looking for features which can bound pointer/reference/lifetime errors. If Carbon has those I will be very interested. And if it does have such features PLEASE make those the first slide in any presentation on Carbon.

Thanks and good luck.

[geoffromer]

See my response here