Language Design considerations [Re: [Agda] Newbie questions after reading Dependently Typed Programming in Agda]

[Nils Anders Danielsson]

On 2010-10-13 10:01, Andreas Abel wrote:
> Here professional blindness hits me, I cannot see much use for named
> non-hidden arguments, except maybe:
> - code documentation by reduncancy
> - refactoring: switching the hiding of an argument without changing the
> code much.

- Code documentation by descriptive names. Compare

     power m n

   and

     power (exponent = m) (base = n).

> This is a real design problem of Agda: What parts of a pattern are
> variables bound by the pattern is too context sensitive.

We have discussed a related issue (which actually led to bugs, not just
type errors) before:

   Changing import lists turns constructors into variables
   http://thread.gmane.org/gmane.comp.lang.agda/720

I think the solution we adopted has worked out rather well.

In another message you wrote the following:

> Apparently it is a problem. A error message like
>
> cannot match against True, because it is not a constructor
>
> would have made things pretty clear for the newcomer, but not the
> mysterious message about an unreachable clause.

If Agda disallowed shadowing in patterns, then we could actually give
that error message.

> field
>   {n : Nat}
>   head : A
>   tail : Vec A n

Minor point: The code above is syntactically incorrect. The following
code works (in a record declaration):

   field
     {n}  : Nat
     head : A
     tail : Vec A n

> Dot patterns are better suited for internal syntax then surface syntax.
> The surface syntax can do without the dots (see IDRIS). However, dot
> inference needs some research first.

Epigram 1 and AgdaLight also supported some notion of "dot inference".
If I remember things correctly there was some major problem with this
inference in AgdaLight, though.

However, if you're so keen to distinguish between constructors and bound
variables syntactically, why don't you want to distinguish between dot
patterns and "real" patterns in a similar way?

--
/NAD