coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Greg Morrisett <greg AT eecs.harvard.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Why no unfolding on left in match?
- Date: Wed, 8 Oct 2014 15:14:34 -0400
This is an instance of a more general problem with datatypes/inductive
definitions that arises in the ML/Haskell/Coq/etc. community: pattern
matching does not promote abstraction.
I’ve always wanted to have more control over this in the form of
an abstract pattern declaration (with attendant proofs that the
patterns are exhaustive and non-overlapping.)
-Greg
On Oct 8, 2014, at 2:26 PM, Kevin Sullivan
<sullivan.kevinj AT gmail.com>
wrote:
> Yeah. Simple unfolding of symbolic names in patterns would be nice, though,
> for the reasons I mentioned. On the other hand, I guess it'd arguably be a
> hack that breaks design symmetry. Maybe it'd cause other problems, too.
> Thanks, --k
>
> On Wed, Oct 8, 2014 at 2:07 PM, Adam Chlipala
> <adamc AT csail.mit.edu>
> wrote:
> Just like in ML and Haskell, those positions don't make sense with
> arbitrary expressions. You need patterns there, and it would add
> nontrivial complexity to the Gallina design to introduce more first-class
> treatment of patterns. [Definition] introduces new expression constructs.
>
>
> On 10/08/2014 02:05 PM, Kevin Sullivan wrote:
>> I'm wondering what's the technical reason that Coq doesn't unfold
>> expressions in pattern position?
>>
>> (* THIS WORKS *)
>>
>> Definition bar (n:nat): nat := match n with 1 => 1 | _ => 0 end.
>>
>> (* THIS DOESN'T *)
>>
>> Definition foo: nat := 1.
>> Definition bar (n:nat): nat := match n with foo => 1 | _ => 0 end.
>>
>> (*
>> The only difference is the use of a symbol rather than a "manifest
>> constant" in the second case.
>> When using nats to represent objects of another kind, I'd prefer to match
>> on symbolic names rather than on their concrete representations as nats --
>> for abstraction, information hiding, readability. Of course
>> the question generalizes beyond nats.
>> *)
>>
>> Kevin
>
>
- [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Enrico Tassi, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Abhishek Anand, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
Archive powered by MHonArc 2.6.18.