Pre-Pre-RFC: Dependable types in rust

[oddcoder]

Hello everyone, This post is reviving the an old (RFC issue)[Add dependent types · Issue #2709 · rust-lang/rfcs · GitHub].

I scouted this forum and bunch of random places over the internet for progress on dependable types for rust and this is a discussion of my findings.

The goal of this post is to come up with a plan for RFC for adding dependable types to rust.

Motivation

First why would we need dependable types. Dependable types is a very powerful tool, but for rust I can imagine two mainline use-cases 1- Proof carrying code in rust: this sounds a bit too specific but that may make rust lucrative for writing cryptographic primitives and code where the correctness (beyond basic memory safety) is important. 2- Type inference in procedural macros for free: I am not 100% sure that this use-case works. but intuitively I would think that since it is possible to pass types as arguments in dependable type system, this should somehow allow rust to model its own type system in runtime, and that may be used in procedural macros (That might as well be 100% wrong, I cannot fully imagine yet how would that work).

It would be possible to combine both use-cases DSL in rust that evaluate at compile time with stricter typing rules thus allow people to write rust code with more guarantees without having to deal with dependent types themselves.

** Which type system **

One of the main questions here is which type system to use, I am aware of 3 languages with dependable types, Coq, Agda and twelf. Both Coq and Agda are built on different views of Matrin Löf type theory, and twelf is built on Edinburgh Logical Framework. The advantage of having similar construct in rust is that the core type system would be extremely small, and provable to be correct which is a good thing. The disadvantage is that much of rust's features (pretty much everything) will have to be modeled on top of those extremely small type system, that would be extremely horrible in terms of performance since it is mostly functional programming model, besides that is counter productive since lots (if not most) of the stdlib would need rewriting(unless I am missing something).

The other extreme would incrementally add ideas from dependable types to rust. The problem is that we will not know for sure if our additions are sound or not, and until we know, the dependable types extension might not be really suitable for proof carrying code.

A compromise solution would be starting from something like rustbelt/oxide or patina (whichever easier to work with / close to completion) and model the (yet to be designed) dependable type extension there and then we know high confidence that it work, but I am not sure if any of the 3 projects completely model the rust language.

I am looking for your input on the matters, If I am lucky and can come up with a clear objective, I might be able work on that project for some time.

[djc]

My input: your post provides an abstract motivation, but none of the other parts of what an RFC usually provides. For your proposal to be taken seriously, it needs to at least talk through some examples of how adding dependent types would improve Rust. Some consideration of the drawbacks probably would also be necessary. As it is now, it’s pretty unclear what you’re actually proposing.

(I’m not familiar with the theory of dependent types, but it would also help if you explain why you’re using divergent terminology here of “dependable” vs “dependent”, which seems more commonly used.)

[canndrew]

Even though my dream language is some kind of dependently typed Rust, adding dependent types to Rust as-is is not something that I think can or should happen. Dependent types are a massive paradigm shift and integrating them properly would require a major overhaul of the language. There are design patterns baked into Rust that you just wouldn't use if dependent types were available. One example is the fact that the == operator returns a bool rather than something proof-relevant. Or even the fact that Rust has a primitive bool type at all given that in dependently-typed setting it's almost never what you want because dependent types and erasure give you zero-cost abstractions for expressing what was true/false and making use of that information at the type level. Pretty much every other aspect of the language and standard library would need to change too though to take account of type dependency.

If you really want a dependently-typed Rust then you'd need to start by designing a Rust 2.0 which is dependently-typed from the ground up. Hopefully someone out there is already working on that.

[oddcoder]

Thanks for your input, Unfortunately I don't have a clear design yet, I know one drawback which would be that one might need SMT solvers which would require hell lot of convincing for why should rustc be shipped with that .

It will take some time before I can have a preliminary design, that would be especially hard because the easy solution as described by @ canndrew would require intrusive modifications to the standard library, and i am trying to figure away to get away with extending the language rather than having to rewrite stdlib before making the extension useful.

[voidc]

Have you read the Pi Type Trilogy RFCs? They propose an extension of Rust's type system to make it dependently typed. Although they weren't accepted in the end, they inspired the design of const generics.

[oddcoder]

Some how I missed that but thanks for pointing it out!