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

Allowing soften locally abstract types #6137

Closed
vicuna opened this issue Aug 22, 2013 · 10 comments
Closed

Allowing soften locally abstract types #6137

vicuna opened this issue Aug 22, 2013 · 10 comments

Comments

@vicuna
Copy link

vicuna commented Aug 22, 2013

Original bug ID: 6137
Reporter: jpdeplaix
Assigned to: @garrigue
Status: acknowledged (set by @garrigue on 2013-08-22T23:31:45Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.01.0+beta/+rc
Category: typing
Monitored by: @Drup @gasche @lpw25 @yallop

Bug description

I 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 information

I 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.

@vicuna
Copy link
Author

vicuna commented Aug 22, 2013

Comment author: @lpw25

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]

@vicuna
Copy link
Author

vicuna commented Aug 22, 2013

Comment author: @lpw25

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

@vicuna
Copy link
Author

vicuna commented Aug 22, 2013

Comment author: @garrigue

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...

@vicuna
Copy link
Author

vicuna commented Aug 22, 2013

Comment author: @lpw25

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]) ...

@vicuna
Copy link
Author

vicuna commented Aug 22, 2013

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented May 30, 2017

Comment author: roshanjames

+1 for having language support.

I end up creating constructors to constrain GADTs, which gets
tedious.

type packed = T : [< `A | `B] t -> packed

 ... (t : _ t) .. 
 let T t =
   match t with
   | A -> T t
   | B -> T t
   | _ -> raise..
 in
 .. (t : [< `A | B] t) .. 

Having some syntax in the language to do this more directly would
be nice.

@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
@lpw25
Copy link
Contributor

lpw25 commented May 15, 2020

I think we should implement the "heavy" syntax and be done with it. This has been an annoying issue for years and having a slightly heavyweight syntax is better than having no syntax.

@garrigue
Copy link
Contributor

Ok for that syntax. I will give it a try.
On a side note, after all these years we do not have syntax for binding existential types in patterns either.

@github-actions github-actions bot removed the Stale label Jun 17, 2020
@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.

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