Distinguishing overloaded arrows about dynsem HOT 11 CLOSED

Example of problematic specification:

module test/coq-semantics/features/overloaded_arrows

signature


  sorts A B AorB

  constructors
    a : A
    b : B
    oa : A -> AorB {implicit}
    ob : B -> AorB {implicit}

  arrows
    AorB --> B
    A --> A

rules

  a() --> b
  where
    a() --> a;
    a --> b.

  a() --> a().

  b() --> b().

  //a() --> b().

Side note: implicit coercions and overloaded arrows interact somewhat confusingly in the example above in the sense that exchanging the order of the AorB --> B and A --> A arrows changes the semantics.

from dynsem.

As you also mention in your comment, the analysis that implements support for implicit reductions is (seemingly) nondeterministic. In the example you posted it should inform the user that there is an ambiguity and that an implicit reduction is not applicable. This issue is tracked at #35.

Now, about the actual issue. While desugaring these arrows to rename them is definitely possible, i don't think it is desirable, at least not as a compilation step in the regular pipeline towards interpreters. Renaming the arrows will probably cause confusion when running/tracing the interpreter as it won't be clear which arrow comes from where.

I presume you need this for code generation. Since your code generation strategies are run after the analysis information about applicable arrows is available. Given a sort ty and an arrow name a you can get a list of applicable arrow definitions:

arrow-def* := <lookup-applicable-arrow-def; filter(where(def-get-name; ?a))> ty

If you have a term construction for term with constructor c, arity i, an arrow name a you can get a list of applicable arrow definitions:

ConstructorType(_, ty) := <lookup-def(|Constructors())> (c, i);
arrow-def* := <lookup-applicable-arrow-def; filter(where(def-get-name; ?a))> ty

It is the expectation that if the semantics are valid there will be exactely one arrow definition in arrow-def*.

The lookup-applicable-arrow-def is currently defined in https://github.com/metaborg/dynsem/blob/master/dynsem/trans/backend/java-backend/analysis-extra.str#L112. If you would like to use this method we can promote this strategy to the regular analysis library (it doesn't require any extra passes).

If you want I can assist in writing a pre-process pass that renames the arrows to disambiguate.

from dynsem.

This issue is tracked at #35.

Thanks, hadn't noticed.

Renaming the arrows will probably cause confusion when running/tracing the interpreter as it won't be clear which arrow comes from where.

I take this point. A few follow-up questions/thoughts.

So the interpreter dispatches dynamically based on the constructor name? I suppose it's OK so long as it is disallowed to have different constructors with the same name, and so long as polymorphic sorts (lists, maps, pairs [at some point]) are explicitly cast.

Personally, I find the explicit casts annoying, and disallowing similarly named constructors for different sorts seems somewhat restrictive.

Maybe, instead of renaming, we could identify an arrow based on its name and sort? That would support my use case (Coq code generation). The interpreter could also use this information when giving error messages based on both the expected name, but also which sorts, so that it is easier for the semanticist/programmer to identify. Having the sort information recorded might also give a way to get rid of mandatory explicit casts when dispatching on polymorphic sorts?

I imagine we could simply augment the NamedDynamicEmitted constructor to incorporate sort information by adding Type below:

NamedDynamicEmitted : List(LabelComp) * IDNOHYPH * Type

(Assuming arrows are uniquely determined by their domain sort, which seems to be the case?)

(Maybe this is also what you're suggesting in #34 ?)

If you want I can assist in writing a pre-process pass that renames the arrows to disambiguate.

If you agree with my arguments above, and if you have time, you're more than welcome to do a pre-processing pass. :)

Otherwise, thanks to your pointers, I think it should be fairly straightforward for me to write up a transformation which augments the arrow descriptors to incorporate sort information to support my use case. I can integrate this into my Coq preprocessor. If you agree with my arguments above, maybe you/we could merge this pre-processing step it into the DynSem analysis/interpreter pipeline also at some point.

from dynsem.

For rules that reduce on constructors the interpreter dispatches on a 3-tuple: (constructor name, constructor arity, arrow name). As you pointed out the interpreter does not run sort-reducing rules - #34.

For polymorphic sorts (which are actually monomorphic per term) like lists the specification is statically disambiguated to insert the type of the list in the reduction use positions (in the LHS of premises that apply a list reduction). The availability of the type information as a type annotation (type cast) in rule application positions is optional but is handy for other transformations - especially the static
This transformation is not applied in the DynSem Core transformation.

At the definition site of rules on polymorphic sorts the type annotation is important in cases where an explicit pattern match is not present:

[] : List(Stmt) --> U().

[s | xs] : List(Stmt) --> U()
where
s --> _;
xs --> _.

Without the : List(Stmt) there's basically no information. In less extreme cases one could use type inference to determine the type of the list. The analysis doesn't do this, it does only very basic inference.

The plan is to apply the same for pairs and map reductions.

... disallowing similarly named constructors for different sorts seems somewhat restrictive.

Disallowing identically named constructors of different sorts was an intentional restriction. One of the reasons is performance.

The sort information is recorded for each arrow during analysis, every applied relation is checked against the recorded arrow signatures, it's just not written into the AST after analysis. Whether or not it is made explicit at arrow call site in the AST, that information has to be available at analysis time.

(Assuming arrows are uniquely determined by their domain sort, which seems to be the case?)

The arrows are indeed uniquely determined by their domain sort, but the at some points during the analysis a distinction is not made between arrows with the same name. Explication of semantic components is an example, where different arrows with the same name but different domain actually share semantic components.

from dynsem.

Ok. I will implement the transformation I sketched above in my Coq preprocessor. Thanks again for the pointers.

I don't see why performance would have to be affected by differently-sorted similarly-named constructors.

I also still think it could be useful to have the sort information available at run-time, at least for error reporting.

I would be happy to discuss these issues offline when you have time.

from dynsem.

Sure, let's discuss next week, that would be great.

I don't see why performance would have to be affected by differently-sorted similarly-named constructors.

Maybe that's indeed not an issue.

from dynsem.

I didn't mean to say that i won't add this explication pass in the compiler. I agree it can indeed be beneficial to implement #34. While it may alone introduce performance issues in the interpreter, relying on #34 will make rule dispatch very slow anyway. If you need to have this explication pass very soon implementing it yourself is the fastest path to getting it. We can backport it afterwards in the compiler front-end.

from dynsem.

Let's raise the priority of this issue, it looks like it's not a lot of effort to implement and it's something you need.

from dynsem.

Hi @casperbp. I pushed 9f73044 to master which adds an explication pass for arrow use sites. It's currently not hooked in the DynSem Core transformation because i haven't added concrete syntax for it, nor have i updated the analysis to support the distinguished arrows types.

from dynsem.

Works like a charm for my purposes -- thanks!

from dynsem.

Feature implemented, closing issue.

from dynsem.