Re: [Caml-list] Late adding of type variable constraints

[Markus Mottl <markus.mottl@gmail.com>]

I see.  So it's not really a matter of soundness, but the type checker
changes would presumably be overly intrusive and possibly cause issues
with efficiency.  Ultimately, I wanted to be able to constrain type
variables via a functor argument, which is also apparently not
possible.

Maybe there are alternative solutions to what I'm trying to do, which
is actually a quite neat type system challenge:

Imagine you have a datastructure that is parameterized over an unknown
number of type variables.  Given such a datastructure, I want to be
able to map all these type variables from one type to another while
preserving the "skeleton" of that structure, but without limiting the
skeleton constructors to a specific number of type variables.

Lets assume the "skeleton" is the option type.  The first part of the
(slightly simplified) solution compiles just fine:

---
module type S = sig
  type 'a t
  type ('a, 'b) mapper

  val map : ('a, 'b) mapper -> 'a t -> 'b t
end

module Option (Arg : S) = struct
  type 'a t = 'a Arg.t option
  type ('a, 'b) mapper = ('a, 'b) Arg.mapper

  let map mapper = function
    | None -> None
    | Some el -> Some (Arg.map mapper el)
end
---

In order to introduce any number of type variables, I thought one
could use the following neat trick (example with two variables):

---
module Arg1 = struct
  type 'args t = 'arg1 constraint 'args = 'arg1 * _

  type ('src, 'dst) mapper = {
    map1 : 'src1 -> 'dst1;
    map2 : 'src2 -> 'dst2;
  }
  constraint 'src = 'src1 * 'src2
  constraint 'dst = 'dst1 * 'dst2

  let map mapper arg1 = mapper.map1 arg1
end
---

But "Option (Arg1)" will not type-check, because the constraints are
missing in signature "S".  This is unfortunate, because I think the
code would be correct.  The body of "Option" should preserve any
constraint on the type variables.

Is there any alternative that preserves extensibility, i.e. an
implementation of "Option" that will work with any number of type
parameters?

On Fri, Sep 4, 2015 at 6:19 PM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> On 2015/09/04 13:28, Markus Mottl <markus.mottl@gmail.com> wrote:
>>
>> Hi,
>>
>> I wonder whether there is a way to add constraints to type variables
>> in signatures after the signature was defined.  E.g.:
>>
>> ---
>> module type S = sig
>>  type 'a t
>>  type ('a, 'b) mappers
>>
>>  val map : ('a, 'b) mappers -> 'a t -> 'b t
>> end
>>
>> module type T = sig
>>  type 'a t constraint 'a = unit  (* whatever *)
>>  include S with type 'a t := 'a t
>> end
>> ---
>>
>> The above will fail, because 'a has additional constraints for type
>> "t" in signature "T".  If I write instead e.g. "type 'a t = 'a list",
>> this will work and also constrain the signature to something narrower.
>> What makes constraints on polymorphic variables special here?
>
> Consider this signature:
>
> module type S = sig
>   type 'a t
>   type 'a u = U of 'a t constraint 'a = < m: int; .. >
> end
>
> Now the signature
>    S with type 'a constraint 'a t = unit
> is ill-typed, but to see it you must type-check again all of its contents
> (not just the definition of t).
>
> This is the reason you cannot do that.
>
> Jacques Garrigue



-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com