[Agda] Pattern matching on irrelevant types with only one constructor?

[Thorsten Altenkirch]

Exactly. It is not a cost but it means that a certain definitional equality doesn’t hold which makes it harder to check your programs. I would be much more flexible with “judgemental equality” anyway, maybe following the lines of Andromeda. The user should be able to define her own eqaulity as long as it is sound (ie.e it has to produce a proof of equality).

From: Jesper Cockx <Jesper at sikanda.be>
Date: Wednesday, 1 May 2019 at 16:22
To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>
Cc: Jon Sterling <jon at jonmsterling.com>, "agda at lists.chalmers.se" <agda at lists.chalmers.se>
Subject: Re: [Agda] Pattern matching on irrelevant types with only one constructor?

@Thorsten: But we *can* reduce the term when we give it the actual termination proof, the point here is only that the termination proof is not irrelevant for checking conversion. When compiling the code to Haskell, Agda even detects that Acc does not contain any interesting information and erases the termination proofs, so there's no run-time cost, only a compile-time one.





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190501/e9c16e42/attachment.html>