[Agda] Changing import lists turns constructors into variables

[Edward Kmett]

  There is one additional option, which I was able to employ in a toy
compiler of mine that had a similar issue.

1.) means you always have to keep these issues in mind, and you are always
at risk of the scenario I paint down in 4 below.

2.) I was supporting full unicode operators just like you and so the
localization nightmare of requiring only upper case characters to lead
constructors was unpalatable and there is a general paucity of easy to type
symbols anyways, that ruled out 2 for me. An optional decorator might not be
a bad idea if no other system presents itself.

3.) Three is ugly because hiding constructors is a handy for letting you
ensure unstated properties by closing off a portion of the world. maybe less
of an issue in agda i'll admit. But I do like being able to enforce the
opaqueness of types while still letting the defining module 'cheat' a
little.

4.) Pattern usage warnings isn't bad. However, it doesn't solve all of your
problems. if a₁ changes from constructor to value in module A then your code
continues to typecheck, If you then construct a value using a₁ then you've
used the pattern!

foo a₁ = a₁

On the other hand, we can observe that

foo (bar baz)

can always identify the fact that bar is used as a constructor. In fact,
anything that is applied in the pattern can't be a variable. It is either a
constructor or the notion being defined.

 You can then either require pattern matches that use nullary constructors
to include parentheses to disambiguate or simply say that when you don't
have them, then the behavior falls back to scenario 4.

Then,

foo zero = ...
matches zero as a variable

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

 I'm not necessarily advocating this approach, but it is an alternative to
the & that sucks less. ;)

-Edward Kmett


On Wed, Feb 25, 2009 at 2:32 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk>wrote:

> Hi,
>
> Consider the following module:
>
> module M where
> open import A -- Brings A, a₁ and a₂ into scope.
> open import B -- Brings B, b₁ and b₂ into scope.
>
> f : A → B
> f a₁ = b₁
> f a₂ = b₂
>
> Assume now that someone adds a definition B to module A. This makes the
> type signature of g ambiguous. One can fix this by changing the import
> statements in M. By just adding minimal import lists one can be lead to
> believe that the following fix is correct:
>
> module M′ where
> open import A using (A)
> open import B using (B; b₁; b₂)
>
> f : A → B
> f a₁ = b₁
> f a₂ = b₂
>
> However, while the code in M′ type checks, it is not equivalent to the
> one in M, because a₁ and a₂ are now treated as variables (the
> constructors are not in scope).
>
> When Ulf and I discussed the lexical syntax of Agda the possibility of
> this problem was raised, but we never did anything about it. However, I
> was recently bitten by this problem. What should we do about it? Some
> ideas:
>
> 1) Leave things as they are. We can devise conventions to avoid this
>  problem. Maybe it is enough to be aware of it.
>
> 2) Make variables and constructors lexically distinguishable. In Haskell
>  constructors start with an upper-case letter. We can mark variable
>  patterns using some reserved character or word:
>
>   id : {A : Set} → A → A
>   id &x = x
>
> 3) Always bring constructors into scope together with the corresponding
>  data type.
>
> 4) Thorsten noted that this particular instance of the problem could
>  have been avoided if Agda had warned about unreachable patterns.
>
> I'm leaning towards 4). Hopefully it is easy to change the coverage
> checker so that it complains if only a proper subset of the clauses is
> needed to reach full coverage. Ulf?
>
> --
> /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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090225/9413a4fb/attachment.html