Improve range info in pattern synonyms

[UlfNorell]

From pumpkingod@gmail.com on October 19, 2011 04:19:34

Have people considered adding pattern/constructor synonyms to Agda? It'd make working with custom universes of types a lot more pleasant. It seems like you could just do a simple syntactic substitution, after checking that the pattern definition contains only nested constructors (or other pattern synonyms).

Original issue: http://code.google.com/p/agda/issues/detail?id=495

[UlfNorell]

From ulf.nor...@gmail.com on October 19, 2011 00:57:01

Yes, it's something I'd really like to have. There are some design choices and I'm currently in favour of a simple syntactic approach, like what's in SHE.

Status: Accepted
Owner: ulf.nor...@gmail.com
Labels: Type-Enhancement Priority-Medium Pattern-Matching

[UlfNorell]

From stevan.a...@gmail.com on March 08, 2012 08:56:21

Adam Gundry and I managed to hack up something that seems to work. Comments appreciated.

Attachment: PatternSynonyms.patch

[UlfNorell]

From andreas....@gmail.com on March 08, 2012 10:06:23

This seems to be analogous to what I have added to MiniAgda (same syntax). I guess you expand all pattern synonyms during type checking? Is there a "back-folding" for printing?

[UlfNorell]

From nils.anders.danielsson on March 08, 2012 10:22:34

We discussed pattern synonyms at the last AIM. Andreas argued for the approach he uses in MiniAgda, I argued for identifying certain simple functions as constructor-like and allowing them in patterns. We didn't reach a consensus. The MiniAgda approach is a bit hacky (what is the semantics of a pattern synonym?), whereas the constructor-like function approach seemed quite costly compared to the perceived benefits. We started discussing Epigram 1-style "<=" and "view" instead. :)

[UlfNorell]

From andreas....@gmail.com on March 08, 2012 10:31:10

The semantics is "a linear macro which expands to a pattern expression". When it comes to dot patterns, it is not so clear how to do them. I shall be interested to study your solution...

[UlfNorell]

From adamgundry on March 09, 2012 01:14:51

Our implementation treats pattern synonyms purely as syntax, as in SHE and MiniAgda (I think). They are scope-checked and stored as abstract syntax in the TCM, then substituted out during the concrete to abstract step (for patterns) or when type-checking (for expressions). We don't currently fold them when printing; I guess this would be possible but needs some thought.

We handle dot patterns by substitution just like everything else, though some of the more arcane parts of the expression language are not supported (notably extended lambdas). I guess writing a dot pattern containing an extended lambda in a pattern synonym would be very unusual.

Identifying constructor-like functions seems like it would require writing out more type signatures. One advantage of the syntactic approach is that it copes nicely with overloaded constructors: the overloading does not need to be resolved in the definition of the pattern synonym, only in its expansion. Such synonyms cannot be given a single type! On the other hand, the constructor-like functions approach might give an explanation for what pattern synonyms in parameterised modules should mean, which our implementation doesn't support.

[UlfNorell]

From adamgundry on March 09, 2012 02:40:33

Just because we could: it was easier to modify the second pass of Concrete to Abstract on patterns (which is there to handle dot patterns) so that it expands synonyms than to figure out how patterns are type-checked! There's no real reason we couldn't do it at type-checking time though.

[UlfNorell]

From adamgundry on March 09, 2012 02:44:41

(The above was in reply to Andreas' question in comment 7, which seems to have disappeared. It asked why we expand LHS pattern synonyms in Concrete to Abstract rather than during type-checking, as with pattern synonyms in expressions.)

[UlfNorell]

From nils.anders.danielsson on March 09, 2012 02:50:14

Ordinary constructors can be overloaded, but if you don't know what a certain constructor refers to, then you can jump to its definition. Have you thought about how similar functionality can be implemented for syntactic pattern synonyms? (With constructor-like functions this should be easy.)

[UlfNorell]

From andreas....@gmail.com on March 09, 2012 03:09:25

I found a problem with the error location. See attached file. Here the relevant lines:

pattern vz = zero , refl

idVar : (Gamma : Context)(C : Ty)(x : Var Gamma C) -> Var Gamma C -- CORRECT: idVar (A ∷ Gamma) C (zero , proof) = zero , proof idVar (A ∷ Gamma) C vz = vz

The pattern vz does not match. The error report point not to vz in the faulty clause, but to the definition of pattern vz.

This behavior can be fixed if you take care of propagating the Range properly. When you expand the pattern synonym, then paste the region of the current location over the region of the expanded pattern.

Attachment: PatternSynonymsErrorLocation.agda

[UlfNorell]

From andreas....@gmail.com on March 09, 2012 03:13:53

Another issue. Parsing the lhs of a pattern synoym definition does not honor infix operators. E.g. I cannot write

infix 5 ∷

pattern x ∷ xs = cons , x , xs

but I have to write

pattern ∷ x xs = cons , x , xs

Is there a principle problem with parsing operators on the lhs or did you just not consider it for now?

In general, I want to upload your patch, but maybe you fix these issues first.

Owner: andreas....@gmail.com

[UlfNorell]

From adamgundry on March 09, 2012 05:49:32

Regarding overloading: it's not clear how to handle overloaded pattern synonym names in our implementation, as they are substituted out before there is enough information to resolve the overloading. Such overloading is simply rejected at present. On the other hand, uses of overloaded constructors in the pattern synonym definiens are permitted, as the overloading can be resolved after substituting out the pattern synonym.

Andreas, thanks for pointing out the issues with our patch. We are working on improving the handling of range information. You're also right that we require definitions to be in prefix form at the moment. A potential problem with allowing definitions like

pattern x ∷ xs = cons , x , xs

is that if the user omits the fixity declaration, this would be parsed as defining the (nonsensical) pattern synonym x with two arguments (∷ and xs). On the other hand, it does look neater than the prefix version. What does MiniAgda do here?

[UlfNorell]

From adamgundry on March 09, 2012 07:15:09

Here's a re-rolled patch that fixes the range issue (plus a bug we found with importing modules). Note that it should be applied to a clean HEAD, without the previous patch, because a recent change to HEAD caused a conflict and this seemed the easiest way to avoid it.

Attachment: PatternSynonyms20120309.patch

[UlfNorell]

From andreas....@gmail.com on March 09, 2012 07:43:27

MiniAgda has no operators. I have not really spent effort on syntax there...

I have committed the patch now. Note that I amended it a bit to remove a conflict with my latest pushes. So Adam, you will also have to obliterate your own patch and pull from the trunk.

The issue with infix operators is optional, but I think it would be nice to have.

If the user omits fixity declarations and underscores, he gets lots of mysterious error messages already (I am getting them all the time. ;-))

[UlfNorell]

From ulf.nor...@gmail.com on March 12, 2012 00:02:51

Good job on pattern synonyms!

A note on infix declarations: the way it works for normal definitions is that infix functions need a type signature, so that you know exactly what name is being defined. I suppose you could look at the declared infix operators and see if any of them match, but that feels a little bit ad hoc. I'm not too concerned with having to write it out in prefix form in the definition. This is already the case for datatypes and records.

[UlfNorell]

From nils.anders.danielsson on March 13, 2012 02:57:08

On the other hand, uses of overloaded constructors in the pattern synonym definiens are permitted, as the overloading can be resolved after substituting out the pattern synonym.

Maybe you misinterpreted my question. Let me be more precise:

data C₁ : Set where c : C₁

data C₂ : Set where c : C₂

data D (A : Set) : Set where d : A → D A

pattern p = d c

foo : D C₁ foo = d c

bar : D C₁ bar = p

If, in the RHS of foo, I jump to the definition of c, then I get to know how Agda disambiguated the constructor. However, if, in the RHS of bar, I jump to the definition of p, then I end up at the constructor d [*]. How can I find out how Agda disambiguated the constructor, without doing the disambiguation manually?

[*] I would have expected to end up at the definition of p. Bug?

[UlfNorell]

From stevan.a...@gmail.com on March 13, 2012 08:13:12

Yeah, the range information still needs some tweaking. Some other things we noticed which would be nice to fix:

* When declaring pattern synonyms it would be nice to have more syntax 
  highlighting; for example in: /pattern s x = suc x/, both /s/ and /suc/ should be
  highlighted as if constructors.

* When pattern synonyms are used on the lhs of a definition the whole pattern is
  highlighted as if it was a constructor, i.e. in /apa (s x)/, /s x/ is green,
  would be nice if only /s/ was green and /x/ was black.

[UlfNorell]

From nils.anders.danielsson on March 13, 2012 08:36:53

Yeah, the range information still needs some tweaking.

How could you solve my problem by tweaking range info? (The problem, not the bug.)

for example in: /pattern s x = suc x/, both /s/ and /suc/ should be highlighted as if constructors.

What if _x is a constructor? Or are operators disallowed also in the RHS?

[UlfNorell]

From andreas....@gmail.com on April 03, 2012 08:03:46

Is anything happening here? We have pattern synonyms, but the range information is not perfect. Passing on ownership of this issue to Adam...

Summary: Improve range info in pattern synonyms
Owner: adamgundry

[UlfNorell]

From stevan.a...@gmail.com on May 29, 2012 08:27:14

Nisse: We are afraid you have to do disambiguation manually.

We fixed the bug for the example you gave in the attached patch, but it mucks about with nameBindingSite which doesn't seem ideal and it only works for use of pattern synonyms on RHS of a defintion, i.e. something like:

baz : D C₁ → D C₂ baz p = p

Where you goto definiton on the LHS p still doesn't work for reasons not clear to us (we do exactly the same thing as we did in the RHS case).

Attachment: pattern-syn-goto-rhs.patch

[UlfNorell]

From nils.anders.danielsson on October 15, 2012 12:44:34

Should this patch be pushed? Your description makes me hesitate.

[UlfNorell]

From stevan.a...@gmail.com on October 18, 2012 03:10:11

Perhaps not. As pointed out; it doesn't seem like the ideal solution and it only fixes the problem partially.

But it was the only solution we could think of at that point in time and, at least I, haven't grown wiser since. Perhaps somebody with a better understanding of the internals can make the judgement if nameBindingSite needs to be tampered with, or if there is a better solution?

[UlfNorell]

From andreas....@gmail.com on October 19, 2012 01:04:45

Labels: -Pattern-Matching PatternMatching

[UlfNorell]

From andreas....@gmail.com on November 17, 2012 03:24:14

Labels: -PatternMatching PatternSynonyms