[Agda] Changing import lists turns constructors into variables

[Nils Anders Danielsson]

On 2009-02-25 21:03, Edward Kmett wrote:

> if a₁ changes from constructor to value in module A then your code
> continues to typecheck

At one point shadowing of locally bound variables was disallowed in
Agda. I don't know why this is no longer the case; shadowing can make
code harder to understand. Ulf, what was the reason for this change?

> If you then construct a value using a₁ then you've used the pattern!
>  
> foo a₁ = a₁

In the case of a type with only one constructor this either works as
intended or fails to type check. For a type with several constructors
the (modified) coverage checker would complain if foo had several
clauses.

> On the other hand, we can observe that
>  
> foo (bar baz)
>  
> can always identify the fact that bar is used as a constructor.

Yes, this problem only applies to nullary constructors (counting only
explicit arguments).

> foo zero = ...
> matches zero as a variable
>  
> foo (zero) = ...
> matches zero as a constructor

By using this trick we can avoid reserving another word or character
(and the discussion of which one to choose). My preferred solution is
still to modify the coverage checker, though.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.