Skip to content

Conversation

@jespercockx
Copy link
Member

This PR implements basic support for Haskell exceptions in agda2hs, with a twist that these exceptions are checked by requiring an argument of type MayThrow e in scope where e is an exception type. This is necessary to have a throw function that does not break soundness of Agda. As usual in agda2hs, the proofs of MayThrow type are marked as erased.

This also has a nice side effect of fixing #428 by requiring an argument of type MayThrow AssertionFailed in the type of assert.

I took the liberty of also including bindings to functions from System.Environment (fixing #433) so that I could replicate the example from Parse, Don't Validate by Alexis King. It turns out that in agda2hs, it is fine to validate rather than parse, as long as you make the validation function return evidence of the validated property.

@jespercockx
Copy link
Member Author

jespercockx commented Nov 20, 2025

Note that this does not include the following:

  • The SomeException type and toException method (which would require proper support for existential types)
  • The fromException method (which would additionally require support for Typeable, see Add support for TypeRep and Typeable #441).
  • Exception contexts (which would require me to understand what they are about)
  • Asynchronous exceptions (which would require support for threading)
  • Handlers (which is again an existential type)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Add support for functions from System.Environment Add support for Exception typeclass and throw/catch functions

2 participants