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
avoiding duplication of shared right hand production while pattern matching a gadt #5866
Comments
Comment author: @garrigue While I admit that this expressiveness could be useful, it is not so easy to implement. |
Comment author: @sliquister Would it not be simpler and sufficient to give a way of pattern matching on gadt constructors without adding any of the type constraints that it introduces now? For instance:
|
Comment author: pszilagyi I think it would be contrary to the spirit of OCaml, but what are the feelings towards a syntactic sugar in the opposite direction, where the clauses are duplicated syntactically for each case, such that they can be instantiated differently for each case? |
Comment author: mbarbin One upside that one could think about pszilagyi's proposal is that it could post-pone the problem for the user point of view. The source could actually be written as the developper wished it to be, giving some time to the compiler to do later (or not) some more trickier things |
Comment author: roshanjames I have a lot of code that deals with GADTs. FWIW, I find the inability to not share right hand side of pattern clauses to cause a lot of repetitive code in my programs. I like sliquister's proposal and it would be good to treat the [a] as a skolem variable in the branches that conflate the type. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 5866
Reporter: mbarbin
Assigned to: @garrigue
Status: acknowledged (set by @garrigue on 2012-12-27T02:51:23Z)
Resolution: open
Severity: feature
Version: 4.00.1
Category: typing
Monitored by: @hcarty
Bug description
given a gadt:
type _ t =
| A : int t
| B : string t
| C : float t
one cannot write the following:
let is_A : type a. a t -> bool = function
| A -> true
| B
| C -> false
Error: This pattern matches values of type string t
but a pattern was expected which matches values of type a t
However, we could imagine a special behavior of the type checker to enforce not specializing the type of [a] in the case of a shared right production, and avoid duplicating the code of the production.
I believe that this proposal is sound, since it could be taken as just syntax sugar for the following workaround (even if the actual change would probably not involve any rewriting of the source code)
let produce : type a. a t -> production = fun t ->
let f () = <common_case> in
match t with
| A -> <special_case>
| B -> f ()
| C -> f ()
In the body of f when it is typed checked, [t] has type [exists a. a t], which would be the type of t in the shared production.
let produce : type a. a t -> production = function
| A -> <special_case>
| B
| C -> <common_case>
The text was updated successfully, but these errors were encountered: