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

[Jesper Cockx]

@Jon: The main point is indeed to have decidable typechecking, not
normalization per se. Thanks for clarifying.

@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.

-- Jesper

On Wed, May 1, 2019 at 5:17 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> That is not really an argument.
>
> Clearly there are many situations where we would like to reduce a term
> which will only terminate in a consistent context. E.g. we can reduce terms
> which are only guarded by a proof of well-foundedness. Another situation is
> wether you can reduce a coercion which relies on an equality proof. The
> latter could lead to a failure of type-soundness but does it matter when we
> execute symbolically (i.e. not at run-time).
>
> I don't say that the answer is always that we shouldn't care, but I was
> asking for better arguments why we should.
>
> Thorsten
>
> On 01/05/2019, 15:35, "Agda on behalf of Jon Sterling" <
> agda-bounces at lists.chalmers.se on behalf of jon at jonmsterling.com> wrote:
>
>     To respond to Thorsten's comments a bit further down the thread, I
> tried really hard to make proof assistants without a complete decision
> procedure for typing practical, and I determined that it is not likely to
> work out. Decidable type checking is good.
>
>
>
>
>
>
> 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.
>
>
>
>
> _______________________________________________
> 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/20190501/3f071015/attachment.html>