Conversation

I regularly have Rust envy, for all the reasons in this thread. Must steal more ideas.

Quote Tweet

· Jan 23, 2019

I've discovered some people aren't aware of why Rust is a really cool programming language. They think it's just a strongly typed compiled language of some sort, which is true, but it doesn't really explain why it is interesting. 1/

Show this thread

130

Brendan Zabarauskas

@brendanzab

Jan 24, 2019

Really would like to see multiplicities (like in Blodwen) and uniqueness typing (like in Clean) and regions (like in Rust) working together in a dependently typed setting. Then add in unboxed data types too. 😍

This Tweet was deleted by the Tweet author. Learn more

Brendan Zabarauskas

@brendanzab

Yeah, definitely wasn't suggesting that Idris/Blodwen needed to tackle all this stuff (if it does that would be cool though!)

4:29 AM · Jan 24, 2019Twitter Web Client

Replying to

and

AFAIK (I could be wrong), uniqueness typing and regions require effects style stuff, which is currently kinda hard in dependent types. So might be a while before we see them in dependently typed langs. I'm hopeful somebody will write a paper someday that I can steal from though!