Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use all constructors listed in a pattern matching to resolve ambiguity #6784

Closed
vicuna opened this issue Feb 17, 2015 · 4 comments
Closed

Use all constructors listed in a pattern matching to resolve ambiguity #6784

vicuna opened this issue Feb 17, 2015 · 4 comments

Comments

@vicuna
Copy link

vicuna commented Feb 17, 2015

Original bug ID: 6784
Reporter: @alainfrisch
Status: acknowledged (set by @damiendoligez on 2015-02-18T22:54:20Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Child of: #5759 #7409
Monitored by: @diml @yallop @hcarty

Bug description

In a record pattern or expression, when no type information is available, the type-checker looks at all listed labels to find the record type. It would be useful to apply a similar strategy for pattern matching on sum types.

Typically, with a declaration such as:

type kind1 =
| Var of string
| Foo of kind1 * kind2

and kind2 =
| Var of string
| Bar of kind1 option * kind2 option

one would be able to write directly:

let rec eval1 = function
| Var _ -> ...
| Foo _ -> ...

and eval2 = function
| Var _ -> ...
| Bar _ -> ...

This would make the code more robust w.r.t. changing the ordering between the declarations for kind1 and kind2 and also w.r.t. changing the ordering of pattern matching clauses. Moreover, it's not syntactically convenient to provide a type annotation on the input type for eval1 or eval2 ("let rec eval1 : t -> _ = function ...").

A first step would be to apply the strategy only when the constructors appear at top-level (type-based lookup would then often do the job for sub-terms, except for parametrized sum types). This should be simple to implement and explain. We could go further and do the same e.g. under tuples.

@vicuna
Copy link
Author

vicuna commented Feb 17, 2015

Comment author: @gasche

I'm in favor of this change that we discussed in #5759, but Jacques was opposed to it at the time ( #5759#c8457 ), because it's hard to propagate type information in patterns. I agree we could at least handle the head constructor of patterns.

@vicuna
Copy link
Author

vicuna commented Feb 17, 2015

Comment author: @alainfrisch

I don't really see that as a form of propagation, just as a change to the lookup strategy to be used for constructors in absence of type information. It's true that (i) the proposed solution, even for head constructors, is not completely local; (ii) it's not very satisfactory to do that only head constructors; (iii) doing it in general would be more complex (although supporting constructors under tuples -- at least when no GADT is involved -- should not be much more difficult and cover most cases); (iv) one might wonder why we should do it for patterns only and not for expressions (and indeed, it should be doable for some expressions as well).

@trefis
Copy link
Contributor

trefis commented Oct 21, 2019

I just stumbled upon this, and it did not get me all excited.
To be able to do this we need to identify "semantic columns" (for lack of a better term), which there's no easy way of doing right now. So this would indeed be restricted to the first column.

Perhaps a "concurrent" inference engine would unblock that restriction (I sort of doubt it), but even so, I don't believe there's any real need for this.

@alainfrisch @gasche : can we close this?

@damiendoligez
Copy link
Member

Given the lack of enthusiasm, I'm closing this feature wish.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants