[Agda] An error function and totality

[Marko Dimjašević]

Dear Agda community,

I've been wondering if there is an Agda equivalent of the error
function in Haskell and Idris. In Haskell, it is this one:

https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:e
rror

In Idris, it is the Debug.Error.error function:

https://www.idris-lang.org/docs/1.2/base_doc/docs/Debug.Error.html

I find it interesting that Idris reports this function to be total,
although it throws an exception. I asked in the Idris mailing list how
come it is total [1], but I got no reply in two weeks.

Does Agda have an equivalent function? Does Agda find the function to
be total?


[1] https://groups.google.com/forum/#!topic/idris-lang/_CqBa0YZJSw

[Philip Wadler]

You can define such a function yourself.

postulate
impossible : ⊥

or even

postulate
error : ∀ {A} → String → A

I find this ability useful. However, an attempt to normalise a term that
depends on a postulate will yield a term in which the postulate appears
rather than raising an error. It would be helpful if Agda had an option to
raise an error in such circumstances, and to indicate in a file terms to be
normalised to confirm they don't depend on such postulates. Yours, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

Post by Marko Dimjašević
Dear Agda community,
I've been wondering if there is an Agda equivalent of the error
https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#v:e
rror
https://www.idris-lang.org/docs/1.2/base_doc/docs/Debug.Error.html
I find it interesting that Idris reports this function to be total,
although it throws an exception. I asked in the Idris mailing list how
come it is total [1], but I got no reply in two weeks.
Does Agda have an equivalent function? Does Agda find the function to
be total?
[1] https://groups.google.com/forum/#!topic/idris-lang/_CqBa0YZJSw
--
Regards,
https://dimjasevic.net/marko
PGP key ID: 056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Marko Dimjašević]

Dear Philip,

Post by Philip Wadler
I find this ability useful. However, an attempt to normalise a term
that depends on a postulate will yield a term in which the postulate
appears rather than raising an error. It would be helpful if Agda had
an option to raise an error in such circumstances, and to indicate in
a file terms to be normalised to confirm they don't depend on such
postulates.

Thank you for your reply. What you wrote sounds related to typed
holes. 

Is there a particular resource you would recommend for learning about
normalisation?


Kind regards,
Marko Dimjašević

[Philip Wadler]

Not really, it's not my area of expertise. Maybe someone else on the list
can help. Cheers, -- P

. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

Too brief? Here's why: http://www.emailcharter.org/

Post by Marko Dimjašević
Dear Philip,

Post by Philip Wadler
I find this ability useful. However, an attempt to normalise a term
that depends on a postulate will yield a term in which the postulate
appears rather than raising an error. It would be helpful if Agda had
an option to raise an error in such circumstances, and to indicate in
a file terms to be normalised to confirm they don't depend on such
postulates.

Thank you for your reply. What you wrote sounds related to typed
holes.
Is there a particular resource you would recommend for learning about
normalisation?
Kind regards,
Marko Dimjašević

[Nils Anders Danielsson]

Post by Marko Dimjašević
Does Agda have an equivalent function?

If you compile programs using the GHC backend, then postulates are
(currently) turned into uses of the error function.