|Anonymous | Login | Signup for a new account||2017-05-25 22:07 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0005866||OCaml||typing||public||2012-12-26 23:25||2014-04-30 18:30|
|Target Version||Fixed in Version|
|Summary||0005866: avoiding duplication of shared right hand production while pattern matching a gadt|
|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
| 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>
| C -> <common_case>
|Tags||No tags attached.|
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.
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?
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 *)
|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?|
edited on: 2013-02-26 06:17
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
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.
|2012-12-26 23:25||mbarbin||New Issue|
|2012-12-27 03:51||garrigue||Note Added: 0008652|
|2012-12-27 03:51||garrigue||Assigned To||=> garrigue|
|2012-12-27 03:51||garrigue||Status||new => acknowledged|
|2012-12-29 17:07||sliquister||Note Added: 0008667|
|2013-02-25 21:01||pszilagyi||Note Added: 0008925|
|2013-02-26 06:17||mbarbin||Note Added: 0008926|
|2013-02-26 06:17||mbarbin||Note Edited: 0008926||View Revisions|
|2014-04-30 18:30||roshanjames||Note Added: 0011338|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|Copyright © 2000 - 2011 MantisBT Group|