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

add support for type expressions on the right-hand side of type substitutions in signatures #6756

Closed
vicuna opened this issue Jan 20, 2015 · 7 comments

Comments

@vicuna
Copy link

vicuna commented Jan 20, 2015

Original bug ID: 6756
Reporter: sweeks
Status: acknowledged (set by @damiendoligez on 2015-02-19T19:44:49Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.1
Target version: undecided
Category: typing
Monitored by: @gasche @yallop @hcarty yminsky @mmottl

Bug description

It would be nice to be able to write:

module type S = sig
type t
end with type t := int list

Currently, one has to write something like:

type t_ = int list
module type S = sig
type t
end with type t := t_

@vicuna
Copy link
Author

vicuna commented Jan 20, 2015

Comment author: yminsky

There's a simliar weakness in destructive substitution. I'd like to write:

module type S = sig
type _ t
val v : _ t
end

module type Z' = S with type 'a t := int

But to get the right effect, one has to write:

type _ u = int
module type Z = S with type 'a t := 'a u

@vicuna
Copy link
Author

vicuna commented Jan 20, 2015

Comment author: sweeks

The only difference I see between my example and Ron's is the arity of [t]. Both examples use destructive substitution. In any case, I would like to be able to write an arbitrary type expression on the RHS, possibly even using the type variables (which neither of our examples does).

@vicuna
Copy link
Author

vicuna commented Jan 21, 2015

Comment author: @garrigue

Just a small explication of the current restriction: destructive substitution relies on path substitution, which only allows to replace a path by another path. I.e. the substituted type must be a type constructor with the same arguments.
From the beginning I wanted to generalize it in the way you suggest here, but I'm not sure of the best way to do it. Maybe extending path substitution to full types is the simplest solution.

@vicuna
Copy link
Author

vicuna commented Apr 20, 2016

Comment author: @mmottl

It would be really nice if this restriction could be lifted. Since we are at it, the following related restriction affects me even more frequently:

module type S = sig module Sub : sig type t end end
module type T = S with type Sub.t := int

If you have many such signatures and deep nesting, workarounds become truly ugly.

@vicuna
Copy link
Author

vicuna commented May 19, 2016

Comment author: @mmottl

@sweeks Since I just ran into exactly that problem, there is a workaround for the case where the substituted type depends on other types in the signature. E.g. the following shows the intention, but won't work, because "type t := ..." is not supported:

module type S = sig
  type el1
  type el2
  type t
  val t : t
end  (* S *)

module type T = sig
  type el1
  type el2

  include S
    with type el1 := el1
    with type el2 := el2
    with type t := (el1 * el2) list  (* This doesn't work *)
end  (* T *)

But the following works:

module type S = sig
  module Subst : sig
    type ('el1, 'el2) t
  end  (* Subst *)

  type el1
  type el2

  val t : (el1, el2) Subst.t
end  (* S *)

module MySubst = struct
  type ('el1, 'el2) t = ('el1 * 'el2) list
end  (* MySubst *)

module type T = S with module Subst := MySubst

Using a module instead of a type substitution makes things a lot simpler, especially if we wanted to substitute several types, since we don't have to both define and substitute long type equations.

Unfortunately, the original signature will look pretty ugly and requires some foresight by the developer to support these kinds of substitutions. Each occurrence of type "t" has to be replaced by a parameterized type.

There is another OCaml feature request somewhere to introduce type aliases in signatures that don't become a required entry. This feature would make the above look a lot nicer.

Anyway, I think I'd still prefer lifting all artificial restrictions on substitutions.

@vicuna vicuna added the typing label Mar 14, 2019
@yminsky
Copy link

yminsky commented Mar 15, 2019

@lpw25 Is this one now resolved?

@lpw25
Copy link
Contributor

lpw25 commented Mar 15, 2019

Fixed by #792

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