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

[Andreas Abel]

@Oscar:  Thanks for the long list of questions.  I take them as  
incentive to think about the Agda language design.

A newcomer does not have the "professional blindness" of an  
experienced user or developer, so his questions are a good stress test  
for the language design.  I want to pick up a few issues.

On Oct 12, 2010, at 11:14 PM, Oscar Finnsson wrote:
> 1. Is it possible to use "record syntax" (names parameters) for
> functions even when the arguments aren't implicit? I.e. can I
> construct named explicit arguments?
> I would like to be able do something like:
>> foo : (x : Nat) -> Nat
>> answer = foo { x = 42 }
>> answer2 = foo 42

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.

> 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:

1. Mark constructors (PiSigma prefixes them with ', Haskell has  
capital letters).

2. Mark bound variables (Twelf uses capitals to mark variables that  
should be bound).

I think I favor 2.  It might be worthwhile trying to require bound  
variables to be prefixed by ^ (like in old logic tradition), or have a  
declaration that provides a namespace for bound variables.

   variables x xs ys

   append (x :: xs) ys = ...

One could also explicitely list variables bound in a clause, but that  
could be tedious...

   append (x :: xs) ys = \ x xs ys -> x :: append xs ys

or

   append (x :: xs) ys = x xs ys |- x :: append xs ys

like in internal syntax.

> 16. Why is False defined as
>> data False : Set where
> while True is defined as
>> record True : Set where
> and why aren't both using the same sort of definition (data or  
> record)?

The question is why we need two syntactically so different  
declarations for such similar thinks as data and record.  If data is  
too ugly to define a record (lots of ->), one could think of   
modifying it something like:

   data Vec (A : Set) : Nat -> Set where
     vnil : Vec A zero
     vcons : Vec A (suc n)
       field
         {n : Nat}
         head : A
         tail : Vec A n

> 20. In vmap₃ (p 9) why isn't nil dotted, i.e. replace
>> vmap₃ zero f nil = nil
> with
>> vmap₃ zero f .nil = nil
> since the only valid value for the third argument is nil?

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.

> 21. What is the difference between parameters and indices of a
> datatype (except syntactically)? Is there something you can do with
> one that you cannot do with the other? When should I preferre one over
> the other?


What is a parameter and what is an index can be inferred automatically  
(see IDRIS).  Distinguishing them syntactically is heritage and could  
be given up, while maintaining the telescope syntax:

   data Vec (A : Set)(_ : Nat) : Set where

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/