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

[Andreas Abel]

On Oct 13, 2010, at 1:42 PM, Ulf Norell wrote:

>
> On Wed, Oct 13, 2010 at 11:01 AM, Andreas Abel <andreas.abel at ifi.lmu.de 
> > wrote:
>
> 2. Why is
> isTrue : Bool -> Set
> isTrue true = True
> isTrue false = False
> valid but not the reverse, i.e.
> isBool : Set -> Bool
> isBool True = true
> isBool False = false
> isn't?
>
> This is a real design problem of Agda:  What parts of a pattern are  
> variables bound by the pattern is too context sensitive.
>
> It needs to be clear from apparition alone which are the  
> constructors and which are the variables.  Haskell solves this by  
> putting constructors into a different class of identifiers.  We need  
> a some way to distinguish variables from constructors in patterns,  
> and there are >=3 choices:
>
> Variables and constructors are distinguished by colour.

Well, yes, *after* type checking.

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.

Cheers,
Andreas

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/