OCaml 的 GADT 作为执行级别的参数

Question

我正在尝试编写一个函数 run 接受一个参数来参数化其执行级别。我希望此函数在给定级别后 return 其输出。我使用 GADTs 让 run 的输出取决于它的输入。

代码如下：

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"

run 共有三个版本。第一个运行良好，但存在代码重复，我想将其删除。我希望我的函数看起来更像 run2 但这个函数无法编译，因为类型检查器无法从 if 条件推断类型。这个问题的答案是 run3 但现在我有这个笨拙的 failwith 案例显然不可能发生。

我想知道是否有办法让我两全其美，一个没有代码重复且没有 failwith 案例的函数？

Answer 1

我发现你的函数 run1 是迄今为止最易读的函数。删除某些代码重复的一种可能性是使运行1 递归。

首先，可以定义一个简短的辅助函数来从 level_output

中提取数据

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

那么运行的递归变体可以写成

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);;

OCaml 的 GADT 作为执行级别的参数

OCaml's GADT as parameter for level of execution

ocaml

gadt