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
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