[Caml-list] Constraining abstract type to be of a given subtype

[Caml-list] Constraining abstract type to be of a given subtype

[Dario Teixeira]

Hi,

In a signature FOO, I'm trying to constrain an abstract type kind_t to be a
subtype of Kind.t (please see code below).  However, I get a compiler error
when I declare an actual struct Foo1 which supposedly obeys signature FOO:

  Type declarations do not match:
    type 'a kind_t = [ `A ]
  is not included in
    type 'a kind_t = 'a constraint 'a = [< Kind.t ]


Any hints as to what is wrong here?  Thanks in advance for your help!

Best regards,
Dario Teixeira


module Kind:
sig
	type t = [ `A | `B | `C ]

	val to_string: t -> string
end =
struct
	type t = [ `A | `B | `C ]

	let to_string = function
		| `A -> "A"
		| `B -> "B"
		| `C -> "C"
end


module type FOO =
sig
	type custom_t
	type 'a kind_t = 'a constraint 'a = [< Kind.t ]
	type 'a t = int * custom_t * 'a kind_t

	val make: int -> custom_t -> 'a kind_t -> 'a t
	val string_of_custom: custom_t -> string
	val string_of_kind: 'a kind_t -> string
end


module Foo1: FOO =
struct
	type custom_t = float
	type 'a kind_t = [ `A ]
	type 'a t = int * custom_t * 'a kind_t

	let make id custom kind = (id, custom, kind)
	let string_of_custom = string_of_float
	let string_of_kind k = Kind.to_string (k :> Kind.t)
end



      

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Guillaume Yziquel]

Le Monday 21 Feb 2011 à 07:56:43 (-0800), Dario Teixeira a écrit :
> Hi,
> 
> In a signature FOO, I'm trying to constrain an abstract type kind_t to be a
> subtype of Kind.t (please see code below).  However, I get a compiler error
> when I declare an actual struct Foo1 which supposedly obeys signature FOO:
> 
>   Type declarations do not match:
>     type 'a kind_t = [ `A ]
>   is not included in
>     type 'a kind_t = 'a constraint 'a = [< Kind.t ]
> 
> 
> Any hints as to what is wrong here?  Thanks in advance for your help!

Well, I clearly see to what 'a is bound to in

	type 'a kind_t = 'a constraint 'a = [< Kind.t ]

but I do not see to what 'a is bound to in

	type 'a kind_t = [ `A ]

As 'a kind_t is declared to be 'a in the first type declaration, it
should also be the case in the second type declaration. However, 'a is a
phantom type parameter there.

> Best regards,
> Dario Teixeira

But I think that you will not be able to do such type narrowing in a
module interface / module interface fashion. At least not without an
indication of covariance or contravariance. And even then, I'm not sure
if that is possible.

-- 
     Guillaume Yziquel

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Dario Teixeira]

Hi,

> But I think that you will not be able to do such type narrowing in a
> module interface / module interface fashion. At least not without an
> indication of covariance or contravariance. And even then, I'm not sure
> if that is possible.

Perhaps I am indeed pushing the module language beyond its design
intentions, but my requirement does not strike me as completely
unreasonable...

If I get rid of the constraint altogether, then I lose the guarantee that
kind_t is a subtype of Kind.t.  But if I declare kind_t = Kind.t in the
signature FOO, then I lose the ability to declare particular instances
of FOO to be more *tightly* constrained than the generic Kind.t.

Any further ideas on how I may be able to have my cake and eat it too?

Cheers,
Dario Teixeira



      

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Guillaume Yziquel]

Le Monday 21 Feb 2011 à 10:42:43 (-0800), Dario Teixeira a écrit :
> Hi,
> 
> > But I think that you will not be able to do such type narrowing in a
> > module interface / module interface fashion. At least not without an
> > indication of covariance or contravariance. And even then, I'm not sure
> > if that is possible.
> 
> Perhaps I am indeed pushing the module language beyond its design
> intentions, but my requirement does not strike me as completely
> unreasonable...
> 
> If I get rid of the constraint altogether, then I lose the guarantee that
> kind_t is a subtype of Kind.t.  But if I declare kind_t = Kind.t in the
> signature FOO, then I lose the ability to declare particular instances
> of FOO to be more *tightly* constrained than the generic Kind.t.
> 
> Any further ideas on how I may be able to have my cake and eat it too?
> 
> Cheers,
> Dario Teixeira

I think it's going to be tough. The closest I've come to is:

# module type Q = sig type 'a t end;;
module type Q = sig type 'a t end
# module type W = Q with type 'a t = [< `A | `B] as 'a;;
Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained
signature:
       Type declarations do not match:
         type 'a t = 'a constraint 'a = [< `A | `B ]
       is not included in
         type 'a t
       Their constraints differ.

While it is possible to 'specialise' a type in a module type signature,
it seems unlikely that it is possible to 'specialise' constraints to
narrower constraints.


-- 
     Guillaume Yziquel

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Daniel Bünzli]

I'm just wondering.

Abstraction is about hiding type representation. Variant subtyping is
a kind of structural subtyping and is thus about type representation.
So constraining an abstract type to be of a given structural subtype
seems contradictory.

The only way I see to type what you want is to make FOO.kind_t
abstract. This doesn't ensure that the implementation of 'a kind_t is
a subtype of Kind.t itself. However if your goal is some kind of
phantom type constraints, it will do the job. And you can still
require a function to convert 'a kind to Kind.t. See the code below.

Best,

Daniel


module Kind:
sig
       type t = [ `A | `B | `C ]

       val to_string: t -> string
end =
struct
       type t = [ `A | `B | `C ]

       let to_string = function
               | `A -> "A"
               | `B -> "B"
               | `C -> "C"
end

module type FOO =
sig
       type custom_t
       type 'a kind_t constraint 'a = [< Kind.t]
       type 'a t = int * custom_t * 'a kind_t

       val make: int -> custom_t -> 'a kind_t -> 'a t
       val string_of_custom: custom_t -> string
       val string_of_kind: 'a kind_t -> string
       val kind_to_kind : 'a kind_t -> Kind.t
end


module Foo1: FOO =
struct
       type custom_t = float
       type 'a kind_t = [`A] constraint 'a = [< Kind.t]
       type 'a t = int * custom_t * 'a kind_t

       let make id custom kind = (id, custom, kind)
       let string_of_custom = string_of_float
       let string_of_kind k = Kind.to_string (k :> Kind.t)
       let kind_to_kind k = (k :> Kind.t)
end

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Dario Teixeira]

Hi,

> Abstraction is about hiding type representation. Variant subtyping is
> a kind of structural subtyping and is thus about type representation.
> So constraining an abstract type to be of a given structural subtype
> seems contradictory.

Yes, you're right, I abused the term "abstract type", when I meant to
say that the type exposed by the interface was not your run-of-the-mill
concrete type but instead any type that satisfied a given constraint.
What would be the proper terminology in this case?


> The only way I see to type what you want is to make FOO.kind_t
> abstract. This doesn't ensure that the implementation of 'a kind_t is
> a subtype of Kind.t itself. However if your goal is some kind of
> phantom type constraints, it will do the job. And you can still
> require a function to convert 'a kind to Kind.t. See the code below.

Which does work quite nicely, thanks!

Cheers,
Dario



      

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Daniel Bünzli]

> Which does work quite nicely, thanks!

In fact it does compile but I don't think it does what you want
because the 'a is completly unrelated to the `A in Foo1.kind_t

Daniel

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Daniel Bünzli]

> In fact it does compile but I don't think it does what you want
> because the 'a is completly unrelated to the `A in Foo1.kind_t

Oh well it's always the same error : when you are doing phantom types,
the type with phantoms should be abstract. See below.

Daniel

module Kind:
sig
      type t = [ `A | `B | `C ]

      val to_string: t -> string
end =
struct
      type t = [ `A | `B | `C ]

      let to_string = function
              | `A -> "A"
              | `B -> "B"
              | `C -> "C"
end

module type FOO =
sig
      type custom_t
      type 'a kind_t constraint 'a = [< Kind.t]
      type 'a t = int * custom_t * 'a kind_t

      val make: int -> custom_t -> 'a kind_t -> 'a t
      val string_of_custom: custom_t -> string
      val string_of_kind: 'a kind_t -> string
      val kind_to_kind : 'a kind_t -> Kind.t
end


module Foo1 : sig
      type custom_t
      type 'a kind_t constraint 'a = [< Kind.t]
      type 'a t = int * custom_t * 'a kind_t

      val make_custom : float -> custom_t
      val make: int -> custom_t -> 'a kind_t -> 'a t
      val string_of_custom: custom_t -> string
      val string_of_kind: 'a kind_t -> string
      val kind_of_kind : ([ `A ] as 'a) -> 'a kind_t
      val kind_to_kind : 'a kind_t -> Kind.t
end = struct
      type custom_t = float
      type 'a kind_t = [`A] constraint 'a = [< Kind.t]
      type 'a t = int * custom_t * 'a kind_t

      let make_custom f = f
      let make id custom kind = (id, custom, kind)
      let string_of_custom = string_of_float
      let string_of_kind k = Kind.to_string (k :> Kind.t)
      let kind_of_kind k = k
      let kind_to_kind k = (k :> Kind.t)
end

let (v : [`A] Foo1.t) =
  Foo1.make 2 (Foo1.make_custom 2.) (Foo1.kind_of_kind `A)

(* Should not typecheck
let (v : [`B] Foo1.t) =
  Foo1.make 2 (Foo1.make_custom 2.) (Foo1.kind_of_kind `A)
*)

module FOOCheck = (Foo1 : FOO)

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Daniel Bünzli]

Ok last message I promise.

I don't know exactly what you want but you may prefer the following
FOO (see the signature of kind_to_kind)  :

module type FOO =
sig
      type custom_t
      type 'a kind_t constraint 'a = [< Kind.t]
      type 'a t = int * custom_t * 'a kind_t

      val make: int -> custom_t -> 'a kind_t -> 'a t
      val string_of_custom: custom_t -> string
      val string_of_kind: 'a kind_t -> string
      val kind_to_kind : 'a kind_t -> 'a
end

In that case the idea is that each implementer declares kind as :

type 'a kind = 'a constraint 'a = [< Kind.t]

but controls which 'a it will actually allow via the kind_of_kind
function (better names to be found)  :

module FooAB : sig
      type custom_t
      type 'a kind_t constraint 'a = [< Kind.t]
      type 'a t = int * custom_t * 'a kind_t

      val make_custom : float -> custom_t
      val make: int -> custom_t -> 'a kind_t -> 'a t
      val string_of_custom: custom_t -> string
      val string_of_kind: 'a kind_t -> string
      val kind_of_kind : ([ `A | `B] as 'a) -> 'a kind_t
      val kind_to_kind : 'a kind_t -> 'a
end = struct
      type custom_t = float
      type 'a kind_t = 'a constraint 'a = [< Kind.t]
      type 'a t = int * custom_t * 'a kind_t

      let make_custom f = f
      let make id custom kind = (id, custom, kind)
      let string_of_custom = string_of_float
      let string_of_kind k = Kind.to_string (k :> Kind.t)
      let kind_of_kind k = k
      let kind_to_kind k = k
end

let (v : [`A | `B] FooAB.t) =
  FooAB.make 2 (FooAB.make_custom 2.) (FooAB.kind_of_kind `A)

let (v : [`A | `B] FooAB.t) =
  FooAB.make 2 (FooAB.make_custom 2.) (FooAB.kind_of_kind `B)

let (k : [`A |`B]) = FooAB.kind_to_kind (FooAB.kind_of_kind `A)

(* Should not typecheck
 let v = FooAB.make 2 (FooAB.make_custom 2.) (FooAB.kind_of_kind `C) *)



module FOOCheck = (FooAB : FOO)

Re: [Caml-list] Constraining abstract type to be of a given subtype

[Dario Teixeira]

Hi Daniel,

> Ok last message I promise.

No problem -- I appreciate the help, thanks!

> I don't know exactly what you want but you may prefer the following
> FOO (see the signature of kind_to_kind)  :

I decided to take a step back and forgo the constraint.  That is, I'm
making the type really abstract, even if in practice all the concrete
implementations of signature FOO will have a kind_t that is a subtype
of Kind.t.

Though it's nice to use the type system to ensure correctness by
construction, in situations (like this one) where one is pushing
against the limits of the type system, the solution can end up
being too cumbersome to use in practice.  Cf, per example, the
pre-3.13 type system tricks to encode GADTs that have been presented
in this list: though brilliant, they haven't gained that much
traction in actual usage because of the associated overhead.

Best regards,
Dario Teixeira