3 ms·
Yes, Idris. Dependent types in an effect system allow you to prove that deadlock cannot occur, such that a potential deadlock in user code is a compile time err
by scatters 5y ago
Yes, Idris. Dependent types in an effect system allow you to prove that deadlock cannot occur, such that a potential deadlock in user code is a compile time error. Edwin Brady has been working on this for decades[1], and Idris 2[2] has finally made it a reality[3].
1. https://www.type-driven.org.uk/edwinb/papers/fi-cbc.pdf https://www.type-driven.org.uk/edwinb/papers/fi-cbc.pdf (free; 2009)
2. https://livebook.manning.com/book/type-driven-development-with-idris/chapter-15/ https://livebook.manning.com/book/type-driven-development-wi... (registration wall; 2017)
3. https://research-repository.st-andrews.ac.uk/handle/10023/23560 https://research-repository.st-andrews.ac.uk/handle/10023/23... (free; 2021)