2:30 Wrong historical & conceptual information. Russell's Type Theory wasn't constructivist in any meaningful sense. It only aimed at incorporating Poincaré's "vicious circle principle" to avoid the contradictions of naïve set theory. Type theory didn't become properly construvist until Per Martin-Löf reconstructed it on an explicitly intuitionistic principles following an astute analysis of Brouwer's original program of intuitionsim.
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.
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...
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.
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.
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.
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."
@@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.
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.
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.
![BOWKYLION - วิงวอน (ex-change) [Official MV]](http://i.ytimg.com/vi/cLdnZWDaO-w/mqdefault.jpg)
I love thinking about this kind of stuff. Anything within discrete mathematics max me feel smart (once I understand it). Feels good!
I wouldn't exactly consider myself a rustaceon, but I found this to be a nice talk
6:57 ah but now we can, as generic constants have since landed in stable rust🎉
2:30 Wrong historical & conceptual information. Russell's Type Theory wasn't constructivist in any meaningful sense. It only aimed at incorporating Poincaré's "vicious circle principle" to avoid the contradictions of naïve set theory. Type theory didn't become properly construvist until Per Martin-Löf reconstructed it on an explicitly intuitionistic principles following an astute analysis of Brouwer's original program of intuitionsim.
Wow, I'm glad I watched this talk, it's super interesting and makes me want to learn more about the whole thing.
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.
Hadn't seed that thing about dependent types moving up one universe level, very cool
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
mind blown
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.
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.
Short and accurate. Thanks
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."
thanks for the great video. is the code for the implementation of IsLessOrEqualTo public?
This is the slides/code/video from the author.
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.
singular they kindof kills the barbers paradox
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.
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.
_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.
chill out wtf