might have to do with higher rank lifetimes but i mainly remember being confused by aaron and niko's conversation and the repeated invokation of the word 'skolemize'
Conversation
just wanted to jump in the thread to voice support for any Rust feature that uses the word “skolemize” in its docs
1
7
Quote Tweet
Replying to @Gankra_
I am literally too excited to properly read this
I just whispered "fuck yeah skolemized lifetimes" to myself
1
3
AFAIK, rough explanation is that skolemization is a way of normalizing complex types with 'foralls' in them so that you can check that they are the same. In Rust this is important for higher rank lifetimes. Comes from logic, after 'Thoralf Skolem': en.wikipedia.org/wiki/Skolem_no
1
5
Taking by the likes I got close? 😅
1
Yep! It basically treats "foralls" (i.e. generics) as if they were fresh concrete types that cannot be unified with any existing concrete types. That's how you make sure that your conclusions really do work *for all* concrete instantiations.
1
3
Ah neat TIL
1
Type theory has a steep learning curve, but it's pretty damn cool. Intimately linked with the foundations of mathematics! 🤩
1
3
Definitely a favorite of mine. I definitely should study more of it when I get the chance. I wish my CS program has done more of it.
1
1
Yeah, my CS program wasn't doing much theory at all, hence leading to me dropping out. I found “Type Theory and Formal Proof: An Introduction” to be useful from a more maths perspective, and TaPL and Software Foundations from Ben Pierce for implementation.