Использование полиморфных функций в определениях - PullRequest
Новая
       8

Использование полиморфных функций в определениях

0 голосов
/ 22 ноября 2018

После моего вопроса здесь у меня есть несколько функций с различными типами аргументов, которые я определил для них индуктивным типом formula.Есть ли в любом случае использовать Inductive formula в compute_formula.Я делаю это, чтобы упростить проверку, уменьшив число конструкторов, которые я должен обрабатывать в доказательствах.Спасибо.

Fixpoint add (n:type1) (m:type2): type3 :=
  match n with
     (*body for add*)
  end.

Fixpoint mul (n:type1) (m:type4): type5 :=
  match n with
   (*body for mul*)
  end.

Inductive formula : Type :=
| Formula {A B}: type1-> A -> (type1->A->B) -> formula.

(* How should I write this *)
Definition compute_formula {A B} (f: formula) (extraArg:A) : B :=
 match f with
  |Formula {A B} part1 part2  part3=>  
        if (A isof type2 && B isof type3) then add part1 part2+extraArg
        if (A isof type4 && B isof type5) then mul part1 part2+extraArg     

  end.

1 Ответ

0 голосов
/ 24 ноября 2018

Каким должен быть тип вывода compute_formula?При написании подписи функция должна иметь возможность вычислять элемент B независимо от того, что такое B.Поскольку это, очевидно, невозможно (что, если B равно Empty?), Я покажу вам другой подход.

Идея состоит в том, чтобы использовать formula для получения типа вывода. 

Definition output_type (f: formula) :=
  match f with
  | @Formula _ B _ _ _ => B
  end.

Тогда мы можем определить compute_formula как 

Definition compute_formula (f: formula): output_type f :=
  match f with
  | @Formula _ _ t a func => func t a
  end.

Несколько других вещей.Я не уверен, что вы имеете в виду под частью extraArg.Если вы уточните, что это значит, я смогу вам помочь.Кроме того, нет (по крайней мере вне тактики) способа сделать то, что вы хотите, с помощью A isof type2.

...