[Caml-list] Late adding of type variable constraints

[Caml-list] Late adding of type variable constraints

[Markus Mottl]

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?

Regards,
Markus

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

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

[Jacques Garrigue]

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

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

[Markus Mottl]

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

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

[Mikhail Mandrykin]

On Friday, September 04, 2015 07:58:26 PM Markus Mottl wrote:
> 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.
 
Not sure if it's exactly what's desired, but I'd suggest Format-like 
implementation in spirit of the following:

(* The mapper "format" GADT, support for pairs, options, results and type 
variables *)
type ('c, 'r, 'i, 'o) mfmt =
(* 'c -- continuation,
    'r -- result of the form (('a -> 'b) -> ... -> ('y -> 'z) -> 'c),
    'i -- input type, o -- output type *)
  | T_v : ('c, ('e -> 'f) -> 'c, 'e, 'f) mfmt
  | Pair :
      ('r1, _ -> _ as 'r2, 'i1, 'o1) mfmt *
      ('c, _ -> _ as 'r1, 'i2, 'o2) mfmt ->
    ('c, 'r2, 'i1 * 'i2, 'o1 * 'o2) mfmt
  | Option : ('c, _ -> _ as 'r, 'i, 'o) mfmt -> ('c, 'r, 'i option, 'o option) 
mfmt
  | Result :
      ('r1, _ -> _ as 'r2, 'i1, 'o1) mfmt *
      ('c, _ -> _ as 'r1, 'i2, 'o2) mfmt ->
    ('c, 'r2, ('i1, 'i2) result, ('o1, 'o2) result) mfmt
  constraint 'r = 'x -> 'y

(* The CPS mapper generator, accepts continuation after mapper "format" *)
let rec map : type a y z d e x. (x -> e, (y -> z), a, d) mfmt -> ((a -> d) -> 
x -> e) -> (y -> z) =
  function
  | T_v -> fun c f -> c f
  | Pair (m1, m2) ->
    fun c -> map m1 @@ fun f1 -> map m2 @@ fun f2 ->c @@ fun (a, b) -> f1 a, 
f2 b
  | Option m ->
    fun c -> map m @@ fun f -> c (function Some a -> Some (f a) | None -> 
None)
  | Result (m1, m2) ->
    fun c -> map m1 @@ fun f1 -> map m2 @@ fun f2 -> c @@
      function
      | Ok a -> Ok (f1 a)
      | Error b -> Error (f2 b)

(* The final mapper generator *)
let map f = map f (fun x -> x)

(* Examples *)

 (* Mapper for the skeleton (('a, 'b) option, 'c option * 'd) result *)
let map_1 m1 m2 m3 m4 = map (Result (Pair (T_v, Option T_v), Pair (Option T_v, 
T_v))) m1 m2 m3 m4;;

let f = map_1 succ int_of_string string_of_int pred;;

f (Ok (5, Some "6"));;
(* Ok (6, Some 6) *)
f (Error (None, 0));;
(* Error (None, -1) *)

(* Mapper for skeleton ('a * ('c * 'e), 'g option * 'i option) result *)
let map_2 m1 m2 m3 m4 m5 = map (Result (Pair (T_v, Pair (T_v, T_v)), Pair 
(Option T_v, Option T_v))) m1 m2 m3 m4 m5;;

let f =
  map_2
    succ
    (fun (a, b) -> Some (int_of_string b, string_of_int a))
    float_of_int
    pred
    (function Ok a -> Some (Error a) | Error a -> Some (Ok a));;

f (Ok (1, ((6, "7"), 0)));;
(* Ok (2, (Some (7, "6"), 0.)) *)
f (Error (None, Some (Ok "5")));;
(* Error (None, Some (Some (Error "5"))) *)

With open extensible types it's possible to extend this approach to unlimited 
number of supported basic skeleton types, but the resulting usages would look 
somewhat messy, e.g.:

let map_1 m1 m2 m3 m4 =
  let open T_v in
  let module O = Option (T_v) in
  let module P1 = Pair (T_v) (O) in
  let module P2 = Pair (O) (T_v) in
  let module R = Result (P1) (P2) in
  R.map (R.Result (P1.Pair (T_v, O.Option T_v), P2.Pair (O.Option T_v, T_v))) 
m1 m2 m3 m4

-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru

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

[Markus Mottl]

On Mon, Sep 7, 2015 at 2:33 PM, Mikhail Mandrykin <mandrykin@ispras.ru> wrote:
> Not sure if it's exactly what's desired, but I'd suggest Format-like
> implementation in spirit of the following:

Though it only solves part of my particular problem, this is a pretty
clever encoding to create mapping functions for structures with
arbitrary numbers of type parameters so thanks for sharing.

In my case I also need to define a type ('a t) such that I can pass it
on in a functor.  The functor body needs to know that invariants are
maintained after each mapping: the skeleton, as captured by t, and
that the same constraints hold for type parameter 'a across mappings.
Only then can the functor body easily map back and forth between
various encodings of the type parameters while maintaining the
skeleton.

Right now my solution to stay extensible is to simply syntactically
include the file containing the functors "Option", "Pair", etc., using
a macro preprocessor.  The environment into which it is included
defines the constraints on the type variables for this particular
instance.  This approach works for arbitrary constraints, which is why
I'm disappointed that this apparently cannot be done without macros.
Somehow it feels like a problem that should be easily solvable within
the core language.

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

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

[Mikhail Mandrykin]

On Wednesday, September 09, 2015 10:00:34 AM Markus Mottl wrote:

> In my case I also need to define a type ('a t) such that I can pass it
> on in a functor.  The functor body needs to know that invariants are
> maintained after each mapping: the skeleton, as captured by t, and
> that the same constraints hold for type parameter 'a across mappings.
> Only then can the functor body easily map back and forth between
> various encodings of the type parameters while maintaining the
> skeleton.
> 

Probably the defunctionalization encoding used in the paper on Lightweight 
Higher-Kinded Polymorphism in OCaml 
(https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf) can help in some way. The corresponding library and examples 
are available at https://github.com/ocamllabs/higher.

The implementation used in the library doesn't perfectly fit the case, because 
the suggested encoding puts the type `t' capturing the type skeleton on an 
unknown depth inside the list of type constructor applications.  I tried the 
following slight variation on the initial encoding:

type ('p, 'f) app = App of 'p * 'f
type nil
type ('a, 'b) typ = .. (* To be used as `('a, M.t) typ' for different `M.t's 
*)

(* Slight change made to pull `M.t' (see below) from the inside of the 
parameter list *)

(* A couple of helper functors similar to the ones in the library *)

module Newtype1 (T : sig type 'a t end) =
struct
  type 'a s = 'a T.t
  type t
  type (_, _) typ += Mk : 'a T.t -> (('a, nil) app, t) typ
  let inj v = Mk v
  let prj (Mk v) = v
end

module Newtype2 (T : sig type ('a, 'b) t end) =
struct
  type ('a, 'b) s = ('a, 'b) T.t
  type t
  type (_, _) typ += Mk : ('a, 'b) T.t -> (('a, ('b, nil) app) app, t) typ
  let inj v = Mk v
  let prj (Mk v) = v
end

(* The common signature for all the skeletons regardless of the number of type 
parameters *)
module type S =
sig
  type t
  type ('a, 'b) mapper = ('a, t) typ -> ('b, t) typ
  
  type task = (* This is just an example of how the mappers can be used *)
      Task :
        ('a, t) typ *
        ('a, 'b) mapper * ('b, 'c) mapper * ('c, 'a) mapper *
        (('a, t) typ -> string) -> task
end

(* The skeleton is captured by M.t .*)
(* The passed type is "('a, M.t) typ" *)
module Performer (M : S) =
struct
  let perform =
    function
    | M.Task  (v, m1, m2, m3, s) ->
      let s = v |> m1 |> m2 |> m3 |> s in
      prerr_endline s
end

(* Example skeleton definitions *)

module Pair =
struct
  include Newtype2 (struct type ('a, 'b) t = 'a * 'b end)
  type ('a, 'b) mapper = ('a, t) typ -> ('b, t) typ
  type task =
      Task : ('a, t) typ * ('a, 'b) mapper * ('b, 'c) mapper * ('c, 'a) mapper 
* (('a, t) typ -> string) -> task
end

module Singleton =
struct
  include Newtype1 (struct type 'a t = 'a end)
  type ('a, 'b) mapper = ('a, t) typ -> ('b, t) typ
  type task =
      Task : ('a, t) typ * ('a, 'b) mapper * ('b, 'c) mapper * ('c, 'a) mapper 
* (('a, t) typ -> string) -> task
end

(* Example usages *)

let mappers =
  (fun (x, y) -> int_of_string x, int_of_string y),
  (fun (x, y) -> float_of_int x, float_of_int y),
  (fun (x, y) -> string_of_float x, string_of_float y)

let pair_tasks =
  let open Pair in
  let m1, m2, m3 = mappers in
  let wrap m x = x |> prj |> m |> inj in
  let m1, m2, m3 = wrap m1, wrap m2, wrap m3 in
  [|Task (inj ("1", "2"), m1, m2, m3, fun x -> let a, b = prj x in a ^ ", " ^ 
b);
    Task (inj (1, 2), m2, m3, m1, fun x -> let a, b = prj x in string_of_int a 
^ ", " ^ string_of_int b)|]

let mappers = int_of_string, float_of_int, string_of_float

let singleton_tasks =
  let open Singleton in
  let m1, m2, m3 = mappers in
  let wrap m x = x |> prj |> m |> inj in
  let m1, m2, m3 = wrap m1, wrap m2, wrap m3 in
  [|Task (inj (1), m2, m3, m1, fun x -> "Just " ^ string_of_int @@ prj x);
    Task (inj ("1"), m1, m2, m3, fun x -> "Just " ^ prj x)|]

module Pair_performer = Performer (Pair)
module Single_performer = Performer (Singleton)

let () = Pair_performer.perform pair_tasks.(0)
(* "1", "2" --> 1, 2 --> 1., 2. --> "1.", "2." --> "1., 2."*)
(* Stderr: 1., 2. *)
let () = Single_performer.perform singleton_tasks.(1)
(* "1" --> 1 --> 1. --> "1." --> "Just 1." *)
(* Stderr: Just 1.*)

let () = Pair_performer.perform pair_task.(1)
(* 1, 2 -> 1., 2. --> "1.", "2." --> Failure: int_of_string *)

-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru

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

[Markus Mottl]

On Wed, Sep 9, 2015 at 3:28 PM, Mikhail Mandrykin <mandrykin@ispras.ru> wrote:
> Probably the defunctionalization encoding used in the paper on Lightweight
> Higher-Kinded Polymorphism in OCaml
> (https://ocamllabs.github.io/higher/lightweight-higher-kinded-polymorphism.pdf) can help in some way. The corresponding library and examples
> are available at https://github.com/ocamllabs/higher.

Thanks a lot for this reference and your code.  Though my problem
still seems slightly different, I found this to be a very interesting
paper.  I remember reading Reynolds' work on defunctionalization many
years ago, and it's fascinating how his work translates from the
object to the type language.

> The implementation used in the library doesn't perfectly fit the case, because
> the suggested encoding puts the type `t' capturing the type skeleton on an
> unknown depth inside the list of type constructor applications.  I tried the
> following slight variation on the initial encoding:

I think the main problem for me is not so much capturing the skeleton,
which the initial approach does just fine, but that type constraints
on the polymorphic variables are maintained with mapper functions.
Maybe the more complicated approaches can be combined to solve the
problem, but that is likely not trivial.

> module Newtype1 (T : sig type 'a t end) =
> struct
>   type 'a s = 'a T.t
>   type t
>   type (_, _) typ += Mk : 'a T.t -> (('a, nil) app, t) typ
>   let inj v = Mk v
>   let prj (Mk v) = v
> end

The compiler will warn above that "prj" is not exhaustive.  If I
understand this correctly, the reasoning is that it's impossible for
two GADT constructors to yield the same type so the warning should be
spurious.  But wouldn't this require making Newtype1 a generative
functor (i.e. adding "()")?  Otherwise the type "t" could be seen as
equivalent if Newtype1 is applied to the same module more than once,
which would allow for more than one "Mk" case and could hence cause a
runtime match error.

I think for the while being I'll just stick to the syntactic approach.
Users who want to extend the number of base types to be mapped over
would have to include code with "Pair", "Option", etc. within an
environment with augmented constraints.

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

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

[Mikhail Mandrykin]

On Friday, September 11, 2015 11:56:33 AM Markus Mottl wrote:
> But wouldn't this require making Newtype1 a generative
> functor (i.e. adding "()")?  Otherwise the type "t" could be seen as
> equivalent if Newtype1 is applied to the same module more than once,
> which would allow for more than one "Mk" case and could hence cause a
> runtime match error.

Yes, indeed.

module T : sig type t = int end;;
module N1 = Newtype0(T);;
module N2 = Newtype0(T);;
# N1.prj @@ N2.inj 0;;
Exception: Match_failure ("//toplevel//", 10, 10).

With generative functors this causes a typing error.  In this case it's also 
possible to use even simpler encoding without open types (`('a, ... ('z, nil) 
app) ...) app) t'):

type ('p, 'f) app = App of 'p * 'f
type nil

module Newtype1 (T : sig type 'a t end) =
struct
  type 'a t = Mk : 'a T.t -> (('a, nil) app) t
  let inj v = Mk v
  let prj (Mk v) = v
end

-- 
Mikhail Mandrykin
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: mandrykin@ispras.ru