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

[Andreas Abel]

On Oct 13, 2010, at 12:01 PM, Jean-Philippe Bernardy wrote:
>> What is a parameter and what is an index can be inferred  
>> automatically
>
> Would be a bit surprising: parameters are in scope of the
> constructors; indices are not.


Can be made work: Idris has:

   Vec : Set -> Nat -> Set
   vcons : A -> Vec A n -> Vec A (suc n)

where A and n are generalized over.


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/