[Agda] Pattern matching on irrelevant data

[Andreas Abel]

Irrelevant matching against data has been disabled by default now, for 
experimentation with it there is the option

   --experimental-irrelevance

On 04.10.11 10:35 AM, Nicolas Pouillard wrote:
> On Tue, Oct 4, 2011 at 10:20 AM, Andreas Abel<andreas.abel at ifi.lmu.de>  wrote:
>> On 03.10.11 10:51 PM, Dan Doel wrote:
> [...]
>> 3. As you pointed out with your refl-example, irrelevant matching against a
>> data type with just one constructor does yield new information in some
>> cases.  This indeed makes my enterprise questionable (the new stuff I pushed
>> yesterday).
>
> Let's throw in a naive question... Could we restrict the irrelevant
> pattern matching to the cases it does not
> add any information? Is it easy to implement? Does this retain some
> useful examples?

Good questions.

To answer the first, I think "terminating" linear pattern families are 
safe to match on irrelevantly.  That excludes the identity type and also 
the accessibility predicate.  This might already answer the second 
question; the interesting examples are gone then.

Terminating linear pattern families can in essence be replaced by 
recursively defined types, so I think they do not reveal information by 
matching on them.

An example that would remain are vectors:  As soon as their length is 
determined, you can match on their content, even if it is irrelevant.

Need to think of a use of this... ;-)

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/