GADT OCaml в качестве параметра для уровня выполнения - PullRequest
Новая
       42

GADT OCaml в качестве параметра для уровня выполнения

0 голосов
/ 22 мая 2018

Я пытаюсь написать функцию run, принимающую параметр для параметризации уровня его выполнения.Я хочу, чтобы эта функция возвращала свой вывод после заданного уровня.Я использовал GADT, чтобы вывод 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, который, очевидно, не может произойти.функция без дублирования кода и без сбоев?

1 Ответ

0 голосов
/ 22 мая 2018

Я считаю вашу функцию run1 самой читаемой на сегодняшний день.Одной из возможностей удалить некоторое дублирование кода может быть рекурсивное выполнение run1.

Сначала можно определить короткую вспомогательную функцию для извлечения данных из 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);;
...