предупреждение quotient_type "нет функции карты"

Question

При использовании команды quotient_type я получаю следующее предупреждение: «Не определена функция карты для Example.A. Это позже вызовет проблемы». Вот минимальный пример для запуска предупреждения (протестировано с Isabelle2017).

theory Example
imports
Main
begin
datatype 'a A = B "'a A" | C
  (*for map: map *) (* uncommenting doesn't fix the warning*)
quotient_type 'a Q = "'a A" / "op ="
  by (rule identity_equivp)
end

Итак, мои вопросы: Что понимается под функцией карты в этом контексте (я знаю только концепцию функции карты в контексте функторов в функциональном программировании)? Какое это имеет отношение к функциям отображения пакетов типов данных, например к функции, сгенерированной закомментированной строкой? Какие проблемы возникнут позже?

Answer 1

Команда datatype по умолчанию не регистрирует сгенерированную функцию карты в фактор-пакете, поскольку могут существовать более общие преобразователи (в случае, если есть переменные мертвого типа). Поэтому вы должны сделать объявление функтора вручную:

functor map_A
   by(simp_all add: A.map_id0 A.map_comp o_def)

Картограф и его теоремы необходимы, если позже вы захотите поднять определения через фактор-тип. Это было обсуждено в списке рассылки Изабель.