[Caml-list] Can we have more flexible destructive type substitution?

[Caml-list] Can we have more flexible destructive type substitution?

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 1094 bytes --]

Currently, for [sig ... end with type lhs := rhs] to be valid, rhs needs to
be an application of a type constructor to the same type parameters as lhs.

I'd like to do, at a minimum, [sig ... end with type 'a t := 'a], but this
is currently forbidden. Are there conceptual obstacles to permitting
arbitrary type expressions on the RHS, or are they simply not implemented
yet?

Note that I can do [type 'a id = 'a] and then [... with type 'a t := 'a
id], but it's clumsy to have to define an auxiliary type for this and it's
not always easy to find an appropriate place to do so.

In particular, I have modules with a blocking interface and an Async
interface, so I define:

module type Thing = sig
  type 'a result
  val read_thing : in_channel -> thing result
  val write_thing : out_channel -> unit result
end

thing_async.mli:
include Thing with type 'a result := 'a Deferred.t
thing_or_error.mli:
include Thing with type 'a result := 'a Or_error.t
thing_exn.mli:
include Thing with type 'a result := 'a (* fails :( *)

Having Thing_exn.id be a useless type constructor would be pretty sad.

[-- Attachment #2: Type: text/html, Size: 1423 bytes --]

Re: [Caml-list] Can we have more flexible destructive type substitution?

[Jacques Garrigue]

On 2015/07/24 23:25, Ben Millwood wrote:
> 
> Currently, for [sig ... end with type lhs := rhs] to be valid, rhs needs to be an application of a type constructor to the same type parameters as lhs.
> 
> I'd like to do, at a minimum, [sig ... end with type 'a t := 'a], but this is currently forbidden. Are there conceptual obstacles to permitting arbitrary type expressions on the RHS, or are they simply not implemented yet?

I think there is no problem in theory.
The reason it is not allowed currently is that substitution relies on the path substitution code, which allows only replacing a path by another path.
Would have to think about how much new code this would require to implement. It might not be that much in practice.

Jacques Garrigue