OCaml 5.0.0~beta1: How to use an argument of Effect when their effect handler is not specified (Usin-CodePudding

I am using opam switch: 5.0.0~beta1

I was playing around with some simple functions (on utop):

type _ Effect.t  = Foo : (unit -> unit) -> unit Effect.t
let a = try perform (Foo (fun () -> Printf.printf "Hello from Foo\n ")) with
| Unhandled (Foo f) -> f ();;
Output: Hello from Foo
 val a: unit = ()

This works well. But when we change the definition of Foo effect,

type _ Effect.t  = Foo : ('a -> unit) -> unit Effect.t
let a = try perform (Foo (fun n -> Printf.printf "Hello from Foo\n ")) with
| Unhandled (Foo f) -> f 45;;
Error: This expression has type int but an expression was expected of type
         $Foo_'a

Here I understand that it needs 'a as an input, but while calling the function, shouldnt it infer the type as int and replace 'a with int and execute the function accordingly? I want to call function f from Foo effect with different argument.

Here is the another example:

 type _ Effect.t  = Suspend : 'a -> unit Effect.t
let a = try perform (Suspend 32) with
| Unhandled (Suspend x) -> x;;
Error: This expression has type $Suspend_'a
       but an expression was expected of type $Unhandled_'a

Here, I understand that return value of (try _ with) i.e. (unit) should be the type of $Unhandled_ 'a. But I also want to know, what is $Unhandled_ 'a type? How is normal 'a is different from $Unhandled_ 'a? How to return $Unhandled_ 'a here? Why there is this special use of $Unhandled? What will be its scope (In some examples where I was using following code,

type _ Effect.t  = Foo : ('a -> unit) -> unit Effect.t
 let p = try Lwt.return (some_function x) with
                | Unhandled (Foo f) -> let (pr, res) = Lwt.task () in 
                    let wkup v = (Lwt.wakeup res v; ()) in
                        f wkup;
                    pr

I also got error as :

    This expression has type $Unhandled_'a Lwt.t
        but an expression was expected of type 'a Lwt.t
        The type constructor $Unhandled_'a would escape its scope

)?
Why there is

        The type constructor $Unhandled_'a would escape its scope

error?

CodePudding user response：

The effect part is a red-herring here, the root issue stems from the notion of existentially-quantified types in GADTs.

When you have a GADT which is defined as

type t = Foo : ('a -> unit) -> t

the type of Foo means that you can construct a t for any type 'a and any function of type 'a -> unit. For instance:

let l = [Foo ignore; Foo print_int]

However, once you have constructed such value, you can no longer knows which type was used to construct the value. If you have a value

let test (Foo f) = ...

you only know that there exists some type 'a such that f has type 'a -> unit. This why the type 'a is called an existentially type (aka a type such that we only know that it exists). The important things to remember is that you don't know which 'a. Consequently you cannot apply the function because applying to the wrong 'a would be a type error.

In other words, the function boxed in Foo f can never be called on any value. This is slightly more subtle variant than the any type

type any = Any: 'a -> any

where the constructor Any takes a value of any type and put it in a black box from which it can never be extracted.

In a way existentially-quantified type variables in a GADT lives in their own world and they cannot escape it. But they can be still be useful if this inner world is large enough. For instance, I can bundle a value with a function that prints that value and then forget the type of this value with:

type showable = Showable: {x:'a; print:'a -> unit} -> showable

Here, I can call the function print on the value x because I know that whatever is 'a it is the same 'a for both x and print:

let show (Showable {x;print}) = print x

Thus I can store few showable values in a list

let l = [ Showable(0, print_int), Showable("zero", print_string)]

and print them later

let () = List.iter show l