OCaml's GADT as parameter for level of execution

Question

I am trying to write a function run taking a parameter to parametrize its level of execution. I want this function to return its output after a given level. I used GADTs to have the output of run depends on its input.

Here is the code:

type _ level_output =                                                                                                                   
  | FirstO  : int -> int level_output                                                                                                  
  | SecondO : float -> float level_output                                                                                              
  | ThirdO  : string -> string level_output                                                                                            

type _ run_level_g =                                                                                                                    
  | First  : int run_level_g                                                                                                           
  | Second : float run_level_g                                                                                                         
  | Third  : string run_level_g 

type run_level = Any : 'a run_level_g -> run_level

let first _ =
  (*do stuff*)
  1

let second _ =
  (*do stuff*)
  2.5

let third _ =
  (*do stuff*)
  "third"

let run1 (type a) (level:a run_level_g) data : a level_output =
  let out = first data in
  match level with
  | First -> FirstO out
  | Second ->
    let out = second out in
    SecondO out
  | Third ->
    let out = second out in
    let out = third out in
    ThirdO out


let run2 (type a) (level:a run_level_g) data : a level_output =
  let out = first data in
  if Any level = Any First
  then FirstO out
  else
    let out = second out in
    if Any level = Any Second
    then SecondO out
    else
      let out = third out in
      ThirdO out


type (_,_) eq = Eq : ('a,'a) eq

let eq_level (type a b) (x:a run_level_g) (y:b run_level_g) : (a, b) eq option =
  match x, y with
  | First, First -> Some Eq
  | Second, Second -> Some Eq
  | Third, Third -> Some Eq
  | _ -> None

let cast_output (type a b) (Eq:(a, b) eq) (v:a level_output) : b level_output = v

let run3 (type a) (level:a run_level_g) data : a level_output =
  let out = first data in
  let eq = eq_level First level in
  match eq with
  | Some eq -> cast_output eq (FirstO out)
  | None ->
    let out = second out in
    let eq = eq_level Second level in
    match eq with
    | Some eq -> cast_output eq (SecondO out)
    | None ->
      let out = third out in
      let eq = eq_level Third level in
      match eq with
      | Some eq -> cast_output eq (ThirdO out)
      | None -> failwith "this can't happen"

There are three versions of run. The first one works well but there is code duplication, which I would like to remove. I would like my function to look more like run2 but this one does not compile because the type checker can't infer the type from the if-condition. An answer to that problem is run3 but now I have this clunky failwith case that obviously can't happen.

I was wondering if there was a way for me to have the best of both worlds, a function with no code duplication and no failwith case?

Answer 1

I find your function run1 the most readable one, by far. One possibility to remove some code duplication may be to make run1 recursive.

First, one can define a short helper function to extract data from level_output

let proj (type a) (x:a level_output): a = 
  match x with
  | FirstO x -> x
  | SecondO x -> x
  | ThirdO x -> x;;

then a recursive variant of run may be written as

let rec run: type a. a run_level_g -> 'b -> a level_output = 
  fun level data -> match level with 
  | First -> FirstO(first data)
  | Second -> SecondO(second @@ proj @@ run First data)
  | Third -> ThirdO(third @@ proj @@ run Second data);;