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

[Ulf Norell]

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. I can't remember
what the default colours are but if you think the difference is too subtle
you can always change your preferences to make it more obvious.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101013/b661deb1/attachment.html