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

avoiding duplication of shared right hand production while pattern matching a gadt #5866

Closed
vicuna opened this issue Dec 26, 2012 · 7 comments

Comments

@vicuna
Copy link

vicuna commented Dec 26, 2012

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>

@vicuna
Copy link
Author

vicuna commented Dec 27, 2012

Comment author: @garrigue

While I admit that this expressiveness could be useful, it is not so easy to implement.
Basically, you would have to type the patterns separately, and in the general case the right hand side should be type several times too.
Things get even worse if you want to handle non-toplevel or-patterns.
So don't hold your breath for this one.

@vicuna
Copy link
Author

vicuna commented Dec 29, 2012

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:

let f (non_specializable_type a) (x : a t) =
  match x with
  | A -> (* a is still abstract *) true
  | B | C ->
    (* a is still abtract, B as type [a t] and C has type [a t] so they are
       unifiable and the pattern is well typed *)
    false

@vicuna
Copy link
Author

vicuna commented Feb 25, 2013

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?

@vicuna
Copy link
Author

vicuna commented Feb 26, 2013

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

@vicuna
Copy link
Author

vicuna commented Apr 30, 2014

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.

@github-actions
Copy link

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.

@github-actions github-actions bot added the Stale label May 15, 2020
@yallop
Copy link
Member

yallop commented May 15, 2020

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

This code is accepted in OCaml 4.08 onwards, thanks (I think) to @trefis's #2110.

@yallop yallop closed this as completed May 15, 2020
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