Kind of going just straight to dependent types. Less for the proving, more for the meta-programming and first class type stuff. Who knows if it is going to work out though!
This Tweet was deleted by the Tweet author. Learn more
Conversation
This Tweet was deleted by the Tweet author. Learn more
Also, seems like systems level stuff will be more doeable thanks to the quantitative type theory work! (linear types and erasure). Do want more coeffects and also effects - sadly integrating those with DTs is still open research. :(
1
I want aaaallll the cake. So greedy :(
1
This Tweet was deleted by the Tweet author. Learn more
Have you thought about dependently typed row polymorphism? Feels like it might require variable capture as a coeffect (twitter.com/brendanzab/sta) and might be too brittle to be useful 🤔
Quote Tweet
Been thinking recently: Could variable captures be considered as coeffects?
(\x => \y => x) : a -> b -> a
(\x => \y =(x)=> x) : a -> b -> a
(\y => x) : error!
(\y =(x)=> x) : b -(a)-> b
Kind of reminds me of capture lists in C++ 
Show this thread