Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006137OCamlOCaml typingpublic2013-08-22 22:572014-07-16 08:56
Reporterjpdeplaix 
Assigned Togarrigue 
PrioritynormalSeverityfeatureReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.01.0+beta/+rc 
Target VersionFixed in Version 
Summary0006137: Allowing soften locally abstract types
DescriptionI would like to be able to create function like the following:

  let f : type 'a. ([< `A | `B ] as 'a) t -> unit = function A -> () | B -> ()

where the type t is a GADT like:

  type _ t = A : [`A] t | B : [`B] t | C : [`C] t

The function match only on two of the tree constructors of the type t.

To do so, I'm requiring features like allowing 'a instead of a full name in locally abstract types to have a restricted polymorphism ([< `A | `B ]) instead of a full polymorphism ('a) in the final signature.
Additional InformationI don't really need this, but it's an experimentation and I think it would be great to have it.

Also, I don't know if it's possible theoretically. If not, I'm interesting in papers on the subject.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0010229)
lpw25 (developer)
2013-08-23 00:42
edited on: 2013-08-23 00:47

It would definitely be nice to have a syntax for adding constraints
directly to locally abstract types:

  let f (type a = [< `A | B]) (x: a t) = ...

or

  let f (type a constraint a = [< `A | B]) (x: a t) = ...

This would also make it possible to use types like:

  type 'a t =
    A : [`A] t
  | B : [`B] t
  constraint 'a = [< `A | `B]

(0010230)
lpw25 (developer)
2013-08-23 01:02

Note that for this to work with polymorphic variants, we would probably need to support refining constraints on polymorphic variant types. This means supporting functions like the following, which add a constraint to a locally abstract type and then refine that constraint to a smaller type:

  # type _ t = X : [< `A | `B] t | Y : [ `C ] t;;
  type _ t = X : [< `A | `B ] t | Y : [ `C ] t

  # type _ s = I : [ `A ] s | J : [ `B ] s | K : [ `C ] s;;
  type _ s = I : [ `A ] s | J : [ `B ] s | K : [ `C ] s

  # let f (type a) : a t * a s -> a = function
      X, I -> `A
    | X, J -> `B
    | Y, K -> `C;;
        Characters 55-57:
        X, I -> `A
                ^^
  Error: This expression has type [> `A ]
         but an expression was expected of type a
         Types for tag `A are incompatible
(0010231)
garrigue (manager)
2013-08-23 01:31

This is a well-known limitation of locally abstract types.
In theory there is no problem (implementation may still be tricky), but the current syntax for locally abstract types makes it hard.
The syntax type 'a... you propose is indeed one I thought about, but this would mean introducing yet another new syntax for types.
The problem with (type a = [< `A|`B]), or rather (type a = private [< `A|`B]) is that is does not allow mutual recursion between private types.
Let's say that all this is under consideration, but with no easy solution in view...
(0010232)
lpw25 (developer)
2013-08-23 01:41

> The problem with (type a = [< `A|`B]), or rather (type a = private [< `A|`B]) > is that is does not allow mutual recursion between private types.

We could allow mutually recursive types like:

  let f (type a = private [> `B of b] and b = private [> `A of a]) ...
(0010233)
garrigue (manager)
2013-08-23 01:55

Sure, I considered that too, but this gets really heavy.
  let f : type a = private [> `B of b] and b = private [> `A of a]. b -> a
The advantage of
   let f : type 'a 'b. ([> `A of [> `B of 'b] as 'a] as 'b) -> 'a
is that is lighter.
Also, this is not fully compatible with the current short-hand
  type a b. ...
which should then be seen as an abbreviation for
  type a and b. ...
Not very coherent.

I may end up with the heavier syntax anyway, rather than creating something completely new.
This still requires heavy changes in the implementation of locally abstract types.

- Issue History
Date Modified Username Field Change
2013-08-22 22:57 jpdeplaix New Issue
2013-08-23 00:42 lpw25 Note Added: 0010229
2013-08-23 00:47 lpw25 Note Edited: 0010229 View Revisions
2013-08-23 01:02 lpw25 Note Added: 0010230
2013-08-23 01:31 garrigue Note Added: 0010231
2013-08-23 01:31 garrigue Assigned To => garrigue
2013-08-23 01:31 garrigue Status new => acknowledged
2013-08-23 01:41 lpw25 Note Added: 0010232
2013-08-23 01:55 garrigue Note Added: 0010233


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker