[Agda] Pattern matching on irrelevant data

[Thorsten Altenkirch]

Maybe this is a good general approach for this sort of potentially dangerous changes.

At least you say explicitely that you are doing something dangerous.

Cheers,
Thorsten

On 4 Oct 2011, at 13:06, Andreas Abel wrote:

> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda