Currently reading up on Idris. Dependent types are really cool! Imagine you take an vec of len 2, and a vec of len 3. In Idris the type system is able to express that the return type is a vector that has the length of the two combined! Super interesting https://en.wikipedia.org/wiki/Idris_(programming_language) …
-
Show this thread
-
Apparently it's possible to "prove invariants" aka prove your code once you have dependent types. The syntax in the examples is super foreign to me, and I don't completely understand how this works. But it mostly sounds like the compiler can catch more bugs, which is great!
1 reply 0 retweets 1 likeShow this thread -
This Tweet is unavailable.
-
Replying to @monkeygroover @yoshuawuyts
Oh, interesting. I've been doing that in Rust for a while now (well, session types) and I'm looking forward to reading Idris' approach
1 reply 0 retweets 1 like -
Replying to @killercup @monkeygroover
Some more resources on dependent types if you're interested: - https://pca.st/5inL - https://www.youtube.com/watch?v=wNa3MMbhwS4 … I'm still trying to make exact sense of this too, haha.
1 reply 0 retweets 1 like -
I'm thinking the right mental model for this is: "what if a type was a primitive". E.g. you can pass a type into a function, and make it produce a new type. Aka "type functions". (Okay, that's as far as I've made sense of it).
1 reply 0 retweets 0 likes -
This may not make sense yet but.. a type function is any type that is generic (e.g. Vec is a type function). Dependent types is when you have type functions that can take *values* - the types depend on the values
1 reply 0 retweets 3 likes -
Replying to @withoutboats @yoshuawuyts and
For example, a Vec<T, Len> is a function of (type, integer) -> type
1 reply 0 retweets 3 likes -
Wait, wait — so am I understanding you correctly then Rust already has this right? I somehow thought it would depend on adding higher kinded types first somehow, haha.
2 replies 0 retweets 0 likes -
Rust has type functions but not yet ones that can have values as inputs. You can write Foo<i32, String> but not Foo<5, String>
1 reply 0 retweets 2 likes
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.