Some more quantified types nightmare

Learning
1

Hi !

I’m still struggling with some dark parts of the type system in OCaml.
In particular, I am trying to model a specific kind of delayed computation, and I’m encountering some issues with unbound types getting out of scope. I am guessing there’s a way of fixing it but I can’t find it.

Here’ s a very simplified version of what I’m trying to do :

type 'a t =
  | Done : 'a -> 'a t
  | Delayed : (unit -> 'a t) -> 'a t
  | Chained : 'a t * ('a -> 'b t) -> 'b t

This type would come with the proper functions :

let return x = Done x
let delay f = Delayed f
let bind x f = Chained (x, f)
let (let*) = bind

That would let me do something like

let five : int t =
  let* three =
    delay (fun () ->
        let y = 1 in
        let z = 2 in
        delay (fun () -> return (y + z)))
  in
  return (three + 2)

and then a function that is called resolve and lets me do something like

let x : int = resolve five (* x is the int 5 *)

However, the implementation of resolve is not compiling :

let rec resolve : 'a t -> 'a = function
  | Done x -> x
  | Delayed f -> resolve (f ())
  | Chained (x, f) -> resolve (f (resolve x))

because

File "bin/test.ml", line 9, characters 42-43:
9 |   | Chained (x, f) -> resolve (f (resolve x))
                                              ^
Error: This expression has type $Chained_'a t
       but an expression was expected of type 'a t
       The type constructor $Chained_'a would escape its scope

This is disturbing to me because it is not the first time that I try hiding internal types and I have made it work in the past. For example :

type packedPP = PP : ((('a, Format.formatter, unit) format -> 'a) -> unit) -> packedPP
let pf fmt (PP msgf) = Format.fprintf fmt |> msgf
let msgf = PP (fun m -> m "aa %d" 4)
let () = pf Format.std_formatter msgf

It compiles and properly show “aa 4”…

Is there a way to make it work ?

Thanks :slight_smile:

1 Like
2

Hi @giltho.

You picked an interesting title, since your issue seems to be that resolve does not have a quantified type :slightly_smiling_face: Changing the type annotation to an explicitly polymorphic one works for me:

let rec resolve : 'a. 'a t -> 'a = ...

The difference between this example and the packedPP example you gave is that the former requires polymorphic recursion, for which type-checking is non-principal; so it may be necessary to add the right polymorphic annotations to get the program to compile. As you’ve discovered, without such annotations the compiler may complain about escaping type variables that can actually be bound by a quantifier.

(Note that your original type constraint ('a t -> 'a) is very weak, since type variables are not implicitly universally quantified in type constraints as they are in signatures. For instance, int t -> int is a valid subtype of 'a t -> 'a.)

1 Like
3

Your type is a GADT, so you should use the type annotation for GADT.

type _ t =
  | Done : 'a -> 'a t
  | Delayed : (unit -> 'a t) -> 'a t
  | Chained : 'a t * ('a -> 'b t) -> 'b t
;;

(* wrong type annotation *)

let rec resolve : 'a t -> 'a = function
  | Done x -> x
  | Delayed f -> resolve (f ())
  | Chained (x, f) -> resolve (f (resolve x))
;;
Error: This expression has type $Chained_'a t
       but an expression was expected of type 'a t
       The type constructor $Chained_'a would escape its scope

(* right type annotation *)

let rec resolve : type a. a t -> a = function
  | Done x -> x
  | Delayed f -> resolve (f ())
  | Chained (x, f) -> resolve (f (resolve x))
;;
val resolve : 'a t -> 'a = <fun>
1 Like
4

Oh wow, it works indeed. Thank you guys for the explanation !! :heart:

1 Like
5

Note that in this very specific case, introducing a locally abstract type is not needed: the GADT never refines the result type and only introduces an existentially quantified type 'b in:

 | Chained : 'b t * ('b -> 'a t) -> 'a t

In fact, this is one of the rare case where the typechecker knows that 'a t is covariant:

type +'a t =
  | Done : 'a -> 'a t
  | Delayed : (unit -> 'a t) -> 'a t
  | Chained : 'b t * ('b -> 'a t) -> 'a t

Thus the universal quantification ('a . 'a t -> 'a ) is sufficient
But using type a. is definitely simpler.

1 Like