Polymorphic Recursive Type Errors

Learning
1

Given the following types:

type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b task) * 'a task -> 'b task
| OnError : ('a -> 'b task) * 'a task -> 'b task

type _ stack =
| NoStack : 'a stack
| AndThenStack : ('a -> 'b task) * 'b stack -> 'a stack
| OnErrorStack : ('a -> 'b task) * 'b stack -> 'a stack

type 'a process = 
{ root: 'a task 
; stack: 'a stack 
}

let rec loop : 'a. 'a process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack
| Fail value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)}

I get an error from the compiler:

Error: This expression has type b#1 stack but an expression was expected of type 'a stack The type constructor b#1 would escape its scope

In this line of code:

| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack

I’ve only been working in OCaml for a few months now, and it’s taken a while to get this far without running into an obscure error message that is inevitably corrected by using some helper types for evaluating the GADT types. I haven’t had any luck using a helper type to solve this issue, so I’m starting to wonder if I’m attempting to do something impossible with the type system.

Can anyone shed light on this error? Many Thanks!

2

You may need to annotate step with a universal type such as type a. a stack -> something.

3

I tried to succeed with the example and it seems the error is not spurious, mere type annotations won’t help and you need to change the type definitions to consider success and error result types separately:

type (_, _) task =
| Success : 'a -> ('a, _) task
| Fail : 'a -> (_, 'a) task
| Binding : ((('a, 'b) task -> unit) -> unit) -> ('a, 'b) task
| AndThen : ('a -> ('b, 'c) task) * ('a, 'c) task -> ('b, 'c) task
| OnError : ('c -> ('a, 'b) task) * ('a, 'c) task -> ('a, 'b) task

type (_, _) stack =
| NoStack : (_, _) stack
| AndThenStack : ('a -> ('b, 'c) task) * ('b, 'c) stack -> ('a, 'c) stack
| OnErrorStack : ('a -> ('b, 'c) task) * ('b, 'c) stack -> ('b, 'a) stack

type ('a, 'b) process = 
{ root: ('a, 'b) task 
; stack: ('a, 'b) stack 
}

let rec loop : type a b. (a, b) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'b. (a, 'b) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest
    in
    step proc.stack
| Fail value -> 
    let rec step : 'a. ('a, b) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)};;

Example usage (as I understand it from the code):

loop {root =
        AndThen ((fun s ->
                    Printf.eprintf "I finished with %s!\n" s;
                    Success ()),
        OnError ((fun s ->
                    Printf.eprintf "Error: %s\n" s;
                    Success "error"),
        AndThen ((fun i ->
                    Printf.eprintf "Success: %d\n" i;
                    Success "success"),
        Binding (fun cnt ->
                      cnt
                      (AndThen
                        ((fun i ->
                          if i <= 0 then Fail (string_of_int i)
                                      else Success (i - 1)),
        Success ~-1))))));
        stack = NoStack };;
loop {root = AndThen ((fun s -> Printf.eprintf "I finished with %s!\n" s; Success ()), OnError ((fun s -> Printf.eprintf "Error: %s\n" s; Success "error"), AndThen ((fun i -> Printf.eprintf "Success: %d\n" i; Success "success"), Binding (fun cnt -> cnt (AndThen ((fun i -> if i <= 0 then Fail (string_of_int i) else Success (i - 1)), Success ~-1)))))); stack = NoStack };;
1 Like
4

Amazing. I actually have a full example with 2 variable types (type (a,x) task), but I was still getting errors , so I wasn’t sure if it was the right direction.

These annotations…

let rec loop : type a x. (a, x) process -> unit = fun proc ->...

let rec step : 'x. (a, 'x) stack -> unit = function...

let rec step : 'a. ('a, x) stack -> unit = function...

… clearly describe what is happening in those recursive functions, but I can’t say I would have come to those annotation on my own. While I was digging around the web searching for solutions, I got the impression that the following 2 annotations could be used interchangeably, which is clearly not the case.

    let rec loop : type a x. (a, x) process -> ....

    let rec loop : 'a 'x. ('a, 'x) process -> ....

Now I see exactly what is going on, and how these types are being used. Thank You!

5

Actually in this particular case the annotations can indeed be used interchangeably:

let rec loop : 'a 'b. ('a, 'b) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'b. (_, 'b) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest
    in
    step proc.stack
| Fail value -> 
    let rec step : 'a. ('a, _) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)};;

This is also typechecked without error.
In general, the difference is that the “rigid”, or locally abstract type (type a) is refined separately in each branch of a match on the annotated value, but the polymorphic type annotation ('a.) only allows to use the annotated function polymorphically in its own body. For example:

type _ t = A : int * 'a t -> < k : int * 'a > t | B : string * 'b t-> < k : string * 'b> t;;
let rec cycle = A (1, B ("2", cycle));;
let rec print : 'a. 'a t -> unit =
  function
  | A (i, t) -> Printf.eprintf "%d" i; print t
  | B (s, t) -> Printf.eprintf "%s" s; print t;;

Will give an error, because the types in different branches cannot be unified. Using a local abstract type fixes this:

let rec print =
  fun (type a) ->
  function
  | (A (i, t) : a t) -> Printf.eprintf "%d" i; print t
  | (B (s, t) : a t) -> Printf.eprintf "%s" s; print t;;

But now the existential type from the branch escapes into the type of the function because of lack of polymorphism. So in this example both annotations are needed:

let rec print : 'a. 'a t -> _ =
  fun (type a) ->
  function
  | (A (i, t) : a t) -> Printf.eprintf "%d" i; print t
  | (B (s, t) : a t) -> Printf.eprintf "%s" s; print t;;

The form type a. is just a shortcut for this combination (see section on polymorphic syntax), so the above is equivalent to:

let rec print : type a. a t -> _ =
  function
  | A (i, t) -> Printf.eprintf "%d" i; print t
  | B (s, t) -> Printf.eprintf "%s" s; print t;;

There is also one tricky issue explained here. It’s the reason why the following:

let rec loop : 'a 'b. ('a, 'b) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'b. ('a, 'b) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest
    in
    step proc.stack
| Fail value -> 
    let rec step : 'a. ('a, 'b) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)};;

gives very surprising error message about less general type. To put it shortly, the two different unification variables named 'a here have different scopes, and the scope of the second (in ('a, 'b) stack)) variable starts earlier than the scope of the first (in 'a 'b. ('a, 'b) process). The error message says nothing about the scope and so looks confusing.

3 Likes
6

I’ve used your examples so many times in the past few days that I’ve actually made a note to come back and thank you again for your explanation. If only all of the document explained concepts as clearly as this…

Huge thumbs-up.