News for hackers. Stuff that matters.
Re:Kind: A Modern Proof Language by LangMakers on Wednesday August 11, 2021 @04:13PM (#28147130)
You're forced to be in the Either monad to use your `abort` though, which kinda beats the point (you could just use the Maybe monad...). It is refreshing to be able to just throw an abort literally anywhere in your code, and get rid of a `Maybe` without changing the structure of your code, resting assured that the `none` case is dealt with properly.
Re:Kind: A Modern Proof Language by lmm on Thursday August 12, 2021 @12:08AM (#28151783)
Isn't that the whole point of MTL-style typeclasses? You use e.g. throwError and can be confident that it'll be plumbed appropriately for whichever context you're currently in. Maybe shouldn't be a special case.