[Agda] An error function and totality

[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/


On Mon, 19 Nov 2018 at 06:31, Marko Dimjašević <marko at dimjasevic.net> wrote:

> 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
>
>
> --
> Regards,
> Marko Dimjašević <marko at dimjasevic.net>
> https://dimjasevic.net/marko
> PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
> Learn email self-defense! https://emailselfdefense.fsf.org
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181119/fd430947/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181119/fd430947/attachment.ksh>