[Agda] --no-pattern-matching

[Conor McBride]

On 17 Jan 2014, at 23:37, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> --no-pattern-matching is an extreme form of chastity, but it should not hard to implement it.

Indeed. It's not even that hard to implement things which look like
pattern matching, but aren't. In fact, I recommend it.

Agda remains fundamentally troubled by its failure to separate its
surface programming language from its (somewhat nebulous) kernel.
It's in good company, of course, but I really think it's worth trying
to nail down what is the type theory and what is elaboration.

All the best

Conor


>  If I understood correctly, you want Agda to slap your fingers if you wrote a constructor pattern anywhere.
> 
> The most principled way to implement this I can think of is to disallow any kind of splitting in the checking of function left hand sides.
> 
> Cheers,
> Andreas
> 
> On 17.01.2014 15:28, Matteo Acerbi wrote:
>> every now and then I would like to forbid
>> myself to use pattern matching at all, at least from inside a single
>> file.
>> 
>> I would like to have the possibility to get back to that file and make
>> sure that I never used pattern matching in that code just by looking
>> at the OPTIONS header.
>> 
>> I think I would find a --no-pattern-matching option, which simply
>> applied this restriction, but still allowed for importing modules
>> whatever their options are, very convenient.
>> 
>> For now I am just curious as to whether others are interested: would
>> anyone else like such a --no-pattern-matching option?
> 
> -- 
> 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