Mantis Bug Tracker
Main | My View | View Issues | Change Log | Roadmap
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005866OCamlOCaml typingpublic2012-12-26 23:252013-02-26 06:17
Reportermbarbin 
Assigned Togarrigue 
PrioritynoneSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.00.1 
Target VersionFixed in Version 
Summary0005866: avoiding duplication of shared right hand production while pattern matching a gadt
Descriptiongiven 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>
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0008652)
garrigue (manager)
2012-12-27 03:51

 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.
(0008667)
sliquister (reporter)
2012-12-29 17:07

 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
(0008925)
pszilagyi (reporter)
2013-02-25 21:01

 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?
(0008926)
mbarbin (reporter)
2013-02-26 06:17
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

- Issue History
Date Modified Username Field Change
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

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker