#agda2hs — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #agda2hs, aggregated by home.social.
-
I’m working on adding some support for Haskell exceptions to
agda2hs. I needed to do something so makethrownot break soundness so I added an (erased instance) argument of some postulated typeMayThrow exc, essentially making all exceptions be checked exceptions on the Agda side.I know there’s much nicer ways to exceptions in dependent type theory (i.e. exceptional type theory by PMP et al) but given that Agda doesn’t implement that, this seems like a decent first step. I’m curious to hear any comments you have!