Sorry, I don’t think I follow what you mean.
I should point out that it would be fine to allow:
type i = I of int
type t = private i = private I of int
to give a type t that is a subtype of i and has a private I constructor. Perhaps that is what @kantian had in mind.
To do that though, it is important that the constructors are given as part of the definition of t. Otherwise you get code like:
module M : sig
module N : sig
type i = I of int
end
type t = private N.i
end = struct
module N = struct
type i = I of int
end
type t = N.i
end
where module subtyping has added new elements to M – the original type of M has no M.I constructor whilst the coerced type of M does.
This kind of solution still doesn’t help with the original example however, since it relies of disambiguation and we only have disambiguation for variant and record constructors, not for string patterns etc.
It’s closer, and indeed I tried your example for illustration purpose but it’s rejected by the compiler (hence, I wrote another ones). By the way, I realise that I was not very clear to explain what I have in mind.
With algebraic data type, the constructors and pattern matching mimic the introduction and elimination rules of proof theory (rules of disjunctive judgments in the case of variants, and rules of conjunctive ones for records). But when we define a module with a private concrete type, the module user can only use the elimination rules and not the introduction ones : one can destruct a value, but one can not construct a value (the module should provide some functions for this purpose).
What I try to say is that if we define a private alias, it’s type safe to use the destructors of the aliased type against a value of the private type and that the type checker should permit this. In the case of primitive types (as int, string…) we can consider that literals are both constructors and destructors for those types. That’s why I said this is not really implicit subtyping (even if do not really see where are the difficulties, this is already the case for instance with functors application).
For the implicit subtyping on function applications (which is another question), consider this example:
module type S1 = sig val i : int val j : int end
module type S2 = sig val i : int end
module Foo (M : S2) = struct let i = succ M.i end
module Bar (M : S1) = Foo(M)
where the type checker do not complain. 
As an aside, during my experiments with the type checker I discovered a difference of behavior between abstract type and private aliased type, and I do not know if it is intentional.
module M : sig
type t
val eq : (t, int) eq
end = struct
type t = int
let eq = Refl
end
module N : sig
type t = private int
val eq : (t, int) eq
end = struct
type t = int
let eq = Refl
end
let (i : M.t) = match M.eq with Refl -> 1;;
val i : M.t = <abstr>
let (i : N.t) = match N.eq with Refl -> 1;;
Error: This expression has type int but an expression was expected of type N.t
but it’s rejected by the compiler
I was suggesting a feature that could be supported, not pointing out existing syntax.
it’s type safe to use the destructors of the aliased type
It’s not about what is type safe. It’s obviously type safe which is why an explicit coercion could be supported. It is a question of what can be inferred in a predictable way.
where the type checker do not complain
The module system doesn’t do any inference, and in particular does not currently do any unification, so it is easy for it to support implicit subtyping.
I do not know if it is intentional.
I wouldn’t say that it is intentional, but it is not surprising that it doesn’t work. The issue is that private int is already represented as an equation, and a type cannot have two equations, so you cannot add type t = int to the environment when you match on the GADT. You could possibly add type int = t, and I can’t remember off the top of my head why it wouldn’t do that, possibly it doesn’t like the circularity that would be created (type int = t = private int).
You should probably report it on Mantis so we can track the issue.
Yes, and I’ve already tried this before you posted your comment. But since it was rejected, I wrote another example to illustrate my thought. By the way, you said this would be fine to allow this, but what I said is that the compiler could do this automatically for us.
For instance, if I write:
type ty = A | B
module M : sig
type t = private ty
end = struct
type t = ty
end
the compiler could interpret this as:
type ty = A | B
module M : sig
type t = private ty = private A | B
end = struct
type t = ty = A | B
end
that is one can destruct an M.t value using ty constructors, but cannot use them to construct an M.t value.
For sure, with your proposition one have to pattern match against M.A or M.B, but is there a real difference if we match directly against A or B?
At that time if I wrote this:
type ty = A | B
module M : sig
type t = private ty
end = struct
type t = ty
end
let f (x : M.t) = match x with
| A -> 'a'
| B -> 'b';;
Error: This pattern matches values of type ty
but a pattern was expected which matches values of type M.t
the type checker complains. But is it difficult to modify the instructions flow such that, before throwing an error, the type checker verify that M.t is a subtype of ty and hence this is fine?
And if I take your last example:
let foo (_ : M.t) = ()
let f x =
match x with
| M.I y -> foo x; y + 1
| _ -> 0
if it’s fine to write a thing such:
module M : sig
type i = I of Int
type t = private i = private I of int
end = struct
type i = I of int
type t = i = I of int
end
you will ask the same disambiguation question to the type checker (has x type M.i or M.t?), and it should infer that x has type M.t.
I’ll do as soon as I’ll receive the confirmation email to create my account.
the compiler could interpret this as:
That would require treating all:
type t = T
module M : sig
type s = t
end
as
type t = T
module M : sig
type s = t = T
end
which is not backwards compatible and makes the elements of M unstable under substitution.
But is it difficult to modify the instructions flow such that, before throwing an error, the type checker verify that M.t is a subtype of ty and hence this is fine?
The aim is not to make type inference work on the most possible programs but to make type inference work in a predictable and principal way. It’s easy to add ad-hoc bits of implicit subtyping in a few places – but then you have no clear narative about why some things work and some others do not.
you will ask the same disambiguation question to the type checker
It’s a subtly different question, it is trying to disambiguate which constructor was used, not trying to work out whether an implicit coercion was added. As I’ve said a few times – adding implicit subtyping to OCaml is not impossible but it needs to be done carefully and with well thought out and predictable rules for when it applies. The same is true of constructor disambiguation – but that work has already been done so we can take advantage of it to solve this issue.
Disambiguation is also easier to make predictable than subtyping because it is much more restricted. With implicit subtyping you need to explain why you can infer a coercion in one place and not in another, with disambiguation it can only occur on an actual constructor pattern/expression so there is less to explain.
This is not what I asked.
This is exactly what I asked, but maybe I was not clear enough : the possibility to use the elimination rules of the aliased type for the values of the private one, i.e. constructor disambiguation.
That’s why I said this is not implicit subtyping (we’re agree on this point), and the examples you gave didn’t fit this question (constructor disambiguation) since you didn’t destruct the value in your pattern matching (except in the last one).
I have just a last question about the original example of this topic: are literals considered as constructors for the primitive types?
You’re still missing the point, but at this point we’re just going around in circles.
are literals considered as constructors for the primitive types?
That are not treated the same as variant constructors if that’s what you mean.
I agree that, if t <= u hold, then just as (e : t :> u) turns an expression e from type t to type uthen (p : u <: t) should turn a pattern p matching on a u into a pattern matching on a t. This is the nice way to solve this question.
2 Likes
For case 2,
is it possible to do something like this? Edit: Yes it is, like so:
type t = private [< 'A of int | 'B of int | 'C of int > 'B 'C]
with result being the same as your case but 'C can also be constructed or matched on in addition to 'B.
Sure, it will solve the problem and it should be added to the language for uniformity reason (this is the dual of value coercion as you noticed). Nevertheless, I wonder if such annotations could be infered by the type checker (without too intrusive modification to its code); otherwise I’m afraid this will be too cumbersome to use in practice. Moreover, I still do not understand why these implicit type coercions on pattern will necessarly need full implicit subtyping (I mean implicit subtyping on all possible values).
module M : sig
type t = private int
end = struct
type t = int
end
type ab = A of int | B of M.t
let foo (i : int) = ()
let bar (x : M.t) = ()
Currently, if we want to write “complex” patter matching, we have to write:
function
| A 1 -> "int 1"
| A 2 -> "int 2"
| A _ -> "an int"
| B x -> match (x :> int) with
| 1 -> "private int 1"
| 2 -> "private int 2"
| _ -> foo (x :> int); bar x; "a private int";;
- : ab -> string = <fun>
With explicit pattern coercion, we could write:
function
| A 1 -> "int 1"
| A 2 -> "int 2"
| A _ -> "an int"
| B (1 : int <: M.t) -> "private int 1"
| B (2 : int <: M.t)-> "private int 2"
| B x -> foo (x :> int); bar x; "a private int"
It would be simpler if we could only write:
function
| A 1 -> "int 1"
| A 2 -> "int 2"
| A _ -> "an int"
| B 1 -> "private int 1"
| B 2-> "private int 2"
| B x -> foo (x :> int); bar x; "a private int"
and for example, we could write:
function
| (1 : int <: M.t) -> "private int 1"
| 2 -> "private int 2"
| x -> foo (x :> M.t); bar x; "a privatet int"
where from the first clause the type checker infers that we are matching a M.t value, in the second clause the pattern 2 is implicitly coerced to match a M.t value, and the variable x in the catch-all clause has type M.t and must be explicitly coerced to int in order to be used with foo — no implicit coercion on values, only on patterns.
In that way, it will be close to @Chris00 trick with a wrapped private type:
module M : sig
type t = private W of int [@@ unboxed]
val cast : t -> int
end = struct
(* we wrapped the int in an unboxed variant,
hence we do not have a runtime overhead. *)
type t = W of int [@@ unboxed]
let cast (W i) = i
end
let foo (i : int) = ()
let bar (i : M.t) = ()
the last example is written:
function
| M.W 1 -> "private int 1"
| M.W 2 -> "private int 2"
| x -> foo (M.cast x); bar x; "a private int"
- : M.t -> string = <fun>
and is currently allowed by the type checker.
I also wonder. The question is whether we can do this while preserving principality. In general just trying to guess subtyping coercions is a sure way to make inference fairly unprincipled (in absence of MLsub, of course), but are there clearly-delimited sub-cases where it is reasonable?
I am not convinced that asking for the explicit coercion is unreasonable in practice, especially if we consider allowing the short form (p <: M.t), which is another (weaker) way to make inference less principled in exchange of convenience. I think that the annotation overhead may be reasonable in practice.
1 Like