Combining phantom types?

Learning
1

Let’s suppose this:

type t = Int of int | Float of float | Pair of t * t | Func of (t -> t)
let rec print = function
  | Int n -> print_int n
  | Float f -> print_float f
  | Pair (t1, t2) -> print t1 ; print t2
  | Func _ -> invalid_arg "print: not for functions"

Of course, I’d like print (Func (fun x->x)) to be a compile time error rather than a runtime error.
I’ve tried to add phantom types and some GADT to no avail, yet I believe this is doable.
Any idea on how to achieve this behavior?

1 Like
2

A quick attempt at it:

type _ t =
  | Int: int -> [> `Printable ] t
  | Float: float -> [> `Printable ] t
  | Pair: ('printable t * 'printable t) -> 'printable t
  | Function : (_ t -> _ t) -> [`Unprintable ] t

let rec print: [ `Printable ] t -> unit  = function
  | Int i -> print_int i
  | Float f -> print_float f
  | Pair (t1, t2) -> print t1; print t2

let () =
  print (Int 42);
  print (Float 51.);
  print (Pair (Int 42, Float 51.))

It will reject unprintable items:

let () =
  print (Function (fun _ -> Int 0))
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type [ `Unprintable ] t
       but an expression was expected of type [ `Printable ] t
       These two variant types have no intersection

Works with composite values:

let () =
  print (Pair (Int 0, Function (fun _ -> Int 0)))
                      ^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type [> `Unprintable ] t
       but an expression was expected of type [ `Printable ] t
       The second variant type does not allow tag(s) `Unprintable

However I’ve been bitten in the past while trying to be too fancy with GADT + polymorphic types, I believe some constructs are undecidable, so maybe expect some backfire if you push it too far.

Importantly we can still combine printable and unprintable values, which will yield an unprintable value:

let x = Pair (Int 0, Function (fun _ -> Int 0))
(* typed [> `Unprintable | `Printable ] t *)

`Printable is probably a poor name, it’s just a dummy base variant because the empty polymorphic variant is a pain to work with, but if anyone can simplify I’m interested.

5 Likes
3

Ah! this is the bit that I couldn’t figure out!
Thank you!