Higher and Lower Types ("Omega Types")

[Gankra]

This proposal enables programmers to continuously navigate the performance-expressiveness curve by providing a mechanism for explicitly working with higher and lower types ("Omega Types").

This allows Rust programmers to take advantage of type-level monads (meganads), and negative-cost abstractions (NCAs).

Rendered

[Manishearth]

Given that this uses HTML, I wonder if we should have a jQuery based procedural macro system.

Or all the cool kids using React these days?

[mgattozzi]

Clearly we should be compiling not to machine code but to JS. It's what everyone is doing these days and we won't even need to worry about Omega Types let alone types at all!

[bstrie]

Oragami Typing

Nit: typo. I believe you meant Shin Megami Tensei, a series of Japanese role-playing videogames.

[comex]

Are you sure? I thought Persona was deprecated years ago.

[bungcip]

A new version of persona already released (persona 5). You can run it on deprecated platform like PS3 but compatible with new PS4 platform

[bstrie]

@bungcip There's a PS3, and it's already deprecated? I'll have to replace all my keyboards... :(

[mark-i-m]

And mice

[dherman]

@Manishearth React? Get with the times, everyone's moved on to preact vue.js next.js reimplementing a web browser in canvas.

Anyway, IIUC this type system can only be modeled with the lambda-hypercube, so it requires A-frame to visualize.

[crlf0710]

When this type-system landed, then people from the community will come up with some AJAX-like approach for builtin RPC support. And by wrapping such RPC-calls to servo into a crate, we can have great GUI systems for Rust right away. Hooray!

[Manishearth]

It occurs to me that this RFC is incredibly one dimensional. I mean that quite literally, it only considers one dimension, the dimension of Rust IRs, which is "up"/"down" in this RFC.

It is based off a one dimensional pipeline:

Text -> AST -> HIR -> MIR -> LLVM-IR -> LLVM-MIR -> ASM -> Machine Code.

However, this isn't the only such pipeline in existence. Consider:

GCC:
Text -> AST -> GENERIC -> GIMPLE -> RTL -> ASM -> Machine code

Swift:
Text -> AST -> SIL -> LLVM-IR -> ASM -> Machine Code.

LaTeX:
Text -> AST -> Text -> AST -> Divine Beauty

Lisp:
AST -> AST -> AST -> AST -> AST -> AST

IRs are a diverse space, and it would be good for us to tap into this.

I propose that we consider the notion of scuttling, where we not only can raise and lower types at will, but have them scuttle sideways much like our beloved Ferris. This way, we can have our types move to, say, SIL, instead, giving us the amazing benefits of our output only working on OSX. This would end the language debate once and for all. Rust becomes the best language, because it is all languages, so anything they can do, Rust can do better.

Scuttled types also let us mix paradigms at will. People have always complained that traditional OOP patterns do not work in Rust due to it's preference of composition over inheritance. No longer! Your program can get the wonderful performance benefits of a GC, while still being able to benefit from the safety of raw pointers. Your program can have the functional purity of C, as well as the amazing mutation powers conferred by Haskell's monads.

I understand that scuttled types do expand the scope of this RFC a lot. I think that while we should not expand the scope of this RFC too much, we must consider future proofing it so that adding scuttled types will still be possible as a non breaking change in the future.

I also understand that my proposal is only two dimensional. A three dimensional proposal is possible by allowing brief forays into completely different fields; for example you may scuttle a type into pureed tomatoes. Further dimensions sadly require introducing Calabi-Yau manifolds into Rust, which I think will have to be tabled until Rust 2.0.

[withoutboats]

👎 no good where is the emoji? I would think someone with your Swift experience would know emoji are really important to making a proposal good. Do more emoji.

[ivandardi]

@withoutboats Emojis are currently reserved as keywords. They'll eventually be used for more ergonomic functionality to appease the newer people coming into Rust. For example 💩will be an alias to the unsafe keyword, 🤔will be the new Lifetime trait, because current lifetimes aren't expressive enough, 🔥will be an alias to the panic!() macro, etc.

[Manishearth]

@ivandardi

🍻   🤣   ↩️🎁(&🤳)   ➡️   ☕ {
    ❓   ✍️   🗃️(📂)   🤷‍♀️    🌟🤳 {
        📂
    } ❗ {
        😱!("Called ❔::↩️🎁() on a 🚫 value")
    }
}

[lifthrasiir]

sup and sub (and in fact, almost all HTML tags) are normal identifiers, no? This will require contextual parser that is cumbersome to implement, albeit it wouldn't be ambiguous (Vec<sup> not followed by ident is a type by its own).

We can instead adopt a syntax that is common enough in the running plain text and several lightweight markup languages (e.g. Pandoc's implementation of Markdown):

i32
Vec<i32>
Vec^i32^
Vec~i32~
Vec^Vec~i32~^

In the expression position, a path including lower or higher type components will be then expressed as Vec::^i32^ etc, highly regular and unambiguous. And it's even more easier to grasp without editor support! (Of course, we can have a side-by-side view like VSCode...)

[jFransham]

This proposal is all about giving users choice, so I think we should allow both syntaxes. So, all of these will be valid:

Vec<sup>i32</sup>
Vec^i32^
Vec^i32</sup>

For compatibility with HTML, we should also allow Vec<sup>i32, parsed in the obvious way.

[killercup]

Many academics professionals prefer not to use angular braces. Thus, I propose we use LaTeX professional syntax instead:

Vec^{i32}
Vec_{i32}
Vec^{HashSet_{i32}}

[jFransham]

This would break backwards-compatibility. I currently rely on the combined gravitational potential of the types in my program to seed a random number generator, which I use to generate a keypair and decrypt the source code of a second program, which is then run through a custom interpreter (I could have used the regular Rust compiler after decrypting, but I wanted to disable type-checking). This proposal would break my workflow.

[ticki]

This feels a lot like a parody extension of my pi type RFC. Perhaps we should join them as an possible extension???

[killercup]

Wow, this is… sloppy and unprofessional :O I mean, in 2017 everyone should know that we need a formal grammar definition for every language change! Please add a section with an XSD for those new tags!

[ticki]

I take offense at the plagiarism. Nobody except me can write a so shitty rfc.

At least give me credits.

[Ixrec]

This is also a major problem for macros 2.0. We need the ability to change a type's gravitational constant at compile-time based on database schemas stored on network file systems if we ever want DieselRocket to be usable on stable. Today it has to rely entirely on Newtonian mechanics to work around hygeine bugs, even though those were proven unsound centuries ago.

[killercup]

@Ixrec, diesel 0.13-beta.37 now has a reverse-polarity feature which you can use to reverse the polarity of Neutron<Flow> in Rocket applications, so that compile-time macros get executed at run time and vice versa. Do you think this could help in such a case?

[aidanhs]

negative-cost abstractions (NCAs)

I just want to go on a tangent to discuss this point a bit. A less formal way of phrasing it is "abstractions that permit optimizations". And we all know that the most optimized code is nonexistent code. Research languages like C have shown us how effective the undefined behaviour 'abstraction' is at validly removing vast swathes of code in a predictable manner to the user, but unfortunately this hasn't really caught on (as C is considered too academic).

I think there's a great opportunity to bring this intuitive behaviour to the masses with a follow-up RFC to extend the NCAs introduced here with undefined behaviour integrated deeply into the language, possibly based on a borrow checker that removes bad code rather than rejecting it [0]. Surely nobody will be able to deny Rust is the fastest language when 90% of main functions can be optimized to just ret! This also fits neatly into the 2017 roadmap goal of "lowering the learning curve" by eliminating the common source of complaints that it's too hard to satisfy the borrow checker at compile time. Nobody likes a failed compile!

[0] Aside from undefined behaviour in C, readers may be more likely to have encountered this behaviour in vigil, a widely used language in safety-critical systems where the removal happens at runtime in order to converge to a perfectly functional application.

[ccmtaylor]

Lgtm, . We can always iterate on syntax and semantics in future major releases of the language, so i wouldn't waste to much time on getting it perfect.

[shepmaster]

Jumping on the syntax bandwagon, I feel that a more intuitive syntax would be to reuse what we already have. This also avoids having to introduce new parser complexity.

i32
Vec<i32>
Vec..i32
Vec...i32
Vec..Vec...i32..... 

The RFC should be accepted as-is. We can hash out insignificant details that people won't have strong opinions about (like ... vs ..=) when deciding to stabilize the feature.

[mark-i-m]

@gankro This is a great RFC! Thanks for all your efforts!

Rust currently lives in an awkward middle-ground: it's currently incredibly inexpressive, making it undesirable for the mainstream programming community which is used to languages like Idris. At the same time, Rust is also incredibly inefficient, making it undesirable for hardcore systems programmers who are used to the blazing performance of Haskell.

I am very confused.

I was under the impression that Rust beat Idris and Haskell on both fronts. But then again, I haven't ever used Idris and I am a novice Haskell programmer.

Under this system, types may be made higher and lower, using the theory of Omega Types. The syntax for this, is simple and natural: types may be raised with the HTML ^{tag, and lowered with the HTML _tag.}

Typing all of those angle brackets sounds like a pain. Maybe we could allow people to ellide hitting the shift key (on keyboards where shift is need to get >):

i32                             // A regular type (coexistential type)
Vec<i32>                        // A generic type (Van Emde Boas type)
Vec,sup.i32,/sup.               // A higher type (Omega type)
Vec,sub.i32,/sub.               // A lower type (Co-Omega type)
Vec,sup.Vec,sub.i32,/sub.,/sup. // A lower higher type (Re-Omega type)

In fact, most Rust programmers could trivially design this system given only the description of it as "a minimal system for forming an oragami crane in the type system".

Including this link might be helpful for beginners, though: https://courses.csail.mit.edu/6.849/fall10/lectures/

How will this proposal interact with ongoing efforts to support SIMD address spaces?

We don't need SIMD anymore. With this proposal, we can right extremely efficient code for dataflow machines.

[mark-i-m]

@Manishearth You should get a Turing award for this.

[Manishearth]

I would prefer a Turing-complete award

[bstrie]

@Manishearth Excuse me, but don't you think you're giving yourself a bit too much credit here? That program is literally copy-pasted from the first page of the Swift tutorial, and it's self-evident that Swift is Turing-complete; otherwise Apple wouldn't have invented it to replace Python 3.

[ticki]

@bstrie can swift run python 2 though

I think not

busted

fucking liar

[withoutboats]

Thanks for the thoughtful RFC @gankro. I don't think anyone has ever written an RFC which so clearly laid out the design space, or as articulately justified the specifics of the proposal in terms of the trade offs involved. Its an immaculately crafted example that all RFC authors should aspire to.

That said, I've decided to unilaterally close this RFC without even giving it an FCP. First, as useful as omega types would be, they just don't fit into the roadmap for 2017. Second, as I'm sure you're already aware, omega types are only a sound typing construct on the first day of April, 364 days of the year they are a totally nonsensical idea made up as a joke. Since its already April 2nd in most of the world, to most users this proposal is quite confusing.

Thanks again for the RFC; I'm looking forward to more great proposals from you now that you're working on Rust again. :-)