Рекурсивное использование методов класса типов в Coq - PullRequest
Новая
       14

Рекурсивное использование методов класса типов в Coq

0 голосов
/ 15 сентября 2018

Есть ли способ использовать рекурсию с классами типов Coq?Как, например, при определении show для списков, если вы хотите рекурсивно вызывать функцию show для списков, вам придется использовать точку фиксирования, например, так: 

Require Import Strings.String.
Require Import Strings.Ascii.

Local Open Scope string_scope.


Class Show (A : Type) : Type :=
  {
    show : A -> string
  }.


Section showNormal.

Instance showList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ lshow xs
        end
  }.

End showNormal.

Что все хорошо, но что, если я хочу определить некоторую вспомогательную функцию, которую я буду использовать для определения Show экземпляров?Как я хочу создать еще одну функцию показа DAZZLING, которая называется magicShow, которая печатает звезды вокруг чего-либо ... 

Definition magicShow {A : Type} `{Show A} (a : A) : string :=
  "** " ++ show a ++ " **".


Instance showMagicList {A : Type} `{Show A} : Show (list A) :=
  {
    show :=
      fix lshow l :=
        match l with
        | nil => "[]"
        | x :: xs => show x ++ " : " ++ magicShow xs
        end
  }.

Однако в этом случае Coq не может найти экземпляр шоу для списка xsперейти на magicShow: 

Error:
Unable to satisfy the following constraints:
In environment:
A : Type
H : Show A
lshow : list A -> string
l : list A
x : A
xs : list A

?H : "Show (list A)"

Есть ли способ сделать это вообще?То есть, вы можете определить метод для класса типов, используя функции, которые полагаются на экземпляр класса типов, который вы определяете?

1 Ответ

0 голосов
/ 16 сентября 2018

Нет, это невозможно сделать. Это работает в Haskell, потому что разрешены произвольные рекурсивные привязки, а язык не заботится о порядке привязок. Coq является более строгим на обоих фронтах. Это имеет смысл, если вы подумаете о том, как выглядит десагеринг: рекурсивный вызов show будет ссылаться на определенный в данный момент экземпляр по имени, но эта привязка еще не находится в области видимости. И вы не можете сделать сам экземпляр фиксированной точкой, потому что вы рекурсивно обращаетесь к структуре типа , а не к значению алгебраического типа данных.

Ваша встроенная точка исправления работает для show, но проблема становится более сложной, если реализации вашего метода ссылаются друг на друга, например 

newtype MyInteger = MyInteger Integer

instance Num MyInteger where
  MyInteger m + MyInteger n = MyInteger $ m  + n
  negate (MyInteger m) = MyInteger $ negate m
  m - n = m + negate n
  -- other methods

Здесь вызовы (+) и negate в определении (-) должны ссылаться на определения (+) и negate выше, но это также не работает в Coq. Единственное решение состоит в том, чтобы определить все ваши методы отдельно, вручную ссылаясь друг на друга, а затем определить экземпляр просто установив для каждого метода тот, который вы определили выше. Например, 

Inductive MyInteger := Mk_MyInteger : Integer -> MyInteger.

Definition add__MyInteger (m n : MyInteger) : MyInteger :=
  let 'Mk_MyInteger m' := m in
  let 'Mk_MyInteger n' := n in
  Mk_MyInteger (add m' n').

Definition negate__MyInteger (m : MyInteger) : MyInteger :=
  let 'Mk_MyInteger m' := m in
  Mk_MyInteger (negate m').

Definition sub__MyInteger (m n : MyInteger) : MyInteger :=
  add__MyInteger m (negate__MyInteger n).

Instance Num__MyInteger : Num MyInteger := {|
  add    := add__MyInteger;
  negate := negate__MyInteger;
  sub    := sub__MyInteger;
  (* other methods *)
|}.
...