Type Theory for the Working Rustacean - Dan Pittman
ฝัง
- เผยแพร่เมื่อ 7 ม.ค. 2020
- Rust really hits a sweet spot with respect to programming languages on account of a) its usefulness when working at a low level, coupled with b) its style of type system. Because of a), Rust can be - and is - used in places which tend to safety-critical: cyber-physical systems, autonomous vehicle infrastructure, robotics, etc. When building systems for these safety-critical environments, one also often formally proves properties about their software. That’s where b) comes in.
Rust’s type system is borne from the same ilk as those used in proof assistants like Agda, Coq, or Lean. Because of this, we can use Rust’s type system in similar ways we’d use a proof assistant to produce safer and more correct programs. This is envisioned by reducing the language of these disparate systems into the lingua franca of type theory.
This talk will explore using (and abusing) Rust’s type system to mimic the proofs one writes about their Rust programs while also enumerating how this mimicry is derived from common ground in the worlds of types or categories. - วิทยาศาสตร์และเทคโนโลยี
I wouldn't exactly consider myself a rustaceon, but I found this to be a nice talk
I love thinking about this kind of stuff. Anything within discrete mathematics max me feel smart (once I understand it). Feels good!
Wow, I'm glad I watched this talk, it's super interesting and makes me want to learn more about the whole thing.
Short and accurate. Thanks
Hadn't seed that thing about dependent types moving up one universe level, very cool
In _raku_ (`raku_lang`) the type hierarchy starts with "Mu" - which puts "the developer" in the realm of logical philosophy and Buddhist metaphysics right from the get go.
mind blown
One issue with this approach is compile-time increase. Imagine running IsLessOrEqualTo calculation for Vec with size i32::max_value() or such. It'd never finish...
my thoughts exactly. This function exists for every size of vec.
That's why the typenum crate encodes the numbers in the typesystem in binary instead of unary.
Compile time is free compared to debugging time. That's something the industry is slowly learning.
But yes, if the language was actually designed around dependent types, patterns like these could be optimised just like anything else :)
@@JETBLAST88 Compile is certainly not free. It makes automated tests costs much higher. Also low debug time is achievable with good architecture + good test policy.
Checking lens in properly implemented type systems with dependent types is done by reduction not literally counting
thanks for the great video. is the code for the implementation of IsLessOrEqualTo public?
This is the slides/code/video from the author.
AHHHH that's why a Rust enum is a SUM-type; A FruitSnack so to speak; A variable can have enum-value 1 OR enum-value 2 OR ...; e.g. The Option enum can be either Some(x) or None.
omg let him hit the spacebar!!
wow mathematicians couldn’t be bothered to type out Natural and succeed or increment but would/expect me to say ‘suck suck naturals’ with a straight face
actually a brilliant talk. thanks for making this understandable for those of us who aren’t type theorists!! i’ve always been really bothered by how i have to check the lengths of vectors and such at runtime, learnt something really cool from this talk, and i’m gonna try and apply this idea in my code later. i still stand by my point that mathematicians should get over themselves and stop with the silly symbol business already. computers have been around for decades. just learn to type faster ffs. it’s 2023 and it’s ur fault if you type so slowly that you still have to Nat this and suc that.
What's the difference with const generics?
If I'm not wrong, const generics are juste a specialization of this concept, for some specific use cases.
@@shikablyat97You're right. Const generics remove the need for "counting up/down" in the type checker and allow you to simply subtract numbers which is much quicker. There's still lots of features that could be added though and I just want to press a fast forward button to get them - const generics just made it to stable, 4 years later.
I just wish slice::Windows could produce `Item`s of known length so that they could be unpacked. This would seem to be a solution. But there has got to be a limit somewhere; I think the typescript type system has been shown to be Turing complete. Maybe rust can beat it by being the first to run Doom on a type system.
Google it, Rust's is too.
singular they kindof kills the barbers paradox
I've had the same error with copy_from_slice, and it's bad, because it's basically memory corruption, something Rust is supposed to guarantee against.
Interesting. It appears as though, mathematically speaking, we are essentially running into Godel's "Incompleteness Theorems" in this endeavor.
That whole "formal mathematics is essentially an impossibility because every paradigm/theory will require certain assumptions which themselves are impossible to prove, and further each and every system of number theory must by its nature omit or 'falsify' certain mathematical truths" thing.
Thus no paradigm of thought regarding number can be "complete." - A paradigm by its very nature is an analytical beast, and analysis being primarily a destructive process (as opposed to synthesis) must omit "things" in its quest towards a satisfying conclusion.
The problem being that all the "omitted things" also contain "mathematical truths," making every theory fundamentally incomplete, unable to express all mathematical truths, and requiring for their validation some other theory which itself is incomplete, ad infinitum.
However, two individuals or components agreeing to operate within a certain paradigm can obviously communicate and "make sense" of each other just fine, thus "dependent types."
_succ_
That's not dependent types, but rather an overengineered, hardcoded, typed nightmare bullshit. Imagine trying to use this in a production code. Actual dependent types don't depend on types (pun not intended) and can be inferred automatically by proof checker from context.
The talk was clearly framed as bending the rust type system, this is just a demo and not meant for prod
Dependent types cannot always be inferred by the proof assistant unfortunately. I think dependent types are better understood as a kind of macro, since (almost) all of the type information is completely deleted at compile time.