В чем разница между `overloading` и` adhoc_overloading`? - PullRequest
Новая
       72

В чем разница между `overloading` и` adhoc_overloading`?

4 голосов
/ 09 мая 2020

Справочное руководство Isabelle описывает способы выполнения перегрузки констант на основе типов: «Adho c перегрузка констант» в разделе 11.3 и «Перегруженные определения констант» в разделе 5.9.

Кажется что перегрузка 5.9 требует, чтобы все параметры типа были известны до принятия решения о перегруженной константе, тогда как перегрузка 11.3 (adho c) определяет перегруженную константу, если существует только одно соответствие: 

consts 
  c1 :: "'t ⇒ 'a set"
  c2 :: "'t ⇒ 'a set"

definition f1 :: ‹'a list ⇒ 'a set› where 
  ‹f1 s ≡ set s›

adhoc_overloading
  c1 f1

overloading
  f2 ≡ ‹c2 :: 'a list ⇒ 'a set›
begin
  definition ‹f2 w ≡ set w›
end

context 
  fixes s :: ‹int list›
begin
  term ‹c1 s› (* c1 s :: int set *)
  term ‹c2 s› (* c2 s :: 'a set  *)
end

Что такое разница между двумя? Когда я могу использовать одно вместо другого?

1 Ответ

3 голосов
/ 09 мая 2020

Перегрузка - ключевая особенность logi c Изабель. Это позволяет вам объявить единственную константу с "широким" типом, который может быть определен для определенных c типов. Пользователям редко приходится делать это вручную. Это базовый механизм, используемый для реализации классов типов. Например, если вы определяете класс типа следующим образом: 

class empty =
  fixes empty :: 'a
  assumes (* ... *)

Затем команда class объявляет константу empty типа 'a', а последующие экземпляры просто предоставляют определение из empty для определенных типов c, например nat или list.

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

Ad-ho c перегрузка , на мой взгляд, вводящее в заблуждение имя. Насколько я понимаю, это происходит из Haskell (см. эту статью Wadler and Blott ). Там они используют его для точного описания механизма классов типов, который в Isabelle был бы придуман как просто «перегрузка». В Isabelle ad-ho c overloading означает нечто совершенно иное. Идея состоит в том, что вы можете использовать его для определения абстрактного синтаксиса (например, нотации до монад) , который не может быть точно уловлен системой простых типов Изабель в стиле ML . Как и в случае с перегрузкой, вы должны определить константу с «широким» типом. Но эта константа никогда не получает никаких определений! Вместо этого вы определяете новые константы с более конкретными c типами. Когда синтаксический анализатор терминов Изабель обнаруживает использование абстрактной константы, он пытается заменить конкретной константой.

Например: вы можете использовать do-notation с option, list и несколько других типов. Если вы напишете что-то вроде: 

do { x <- foo; bar }

, Изабель увидит: 

Monad_Syntax.bind foo (%x. bar)

На втором этапе, в зависимости от типа foo, он преобразует его в один из этих возможных терминов: 

Option.bind foo (%x. bar)
List.bind foo (%x. bar)
(* ... more possibilities ...*)

Опять же, пользователям, вероятно, не нужно иметь дело с этой концепцией явно. Если вы извлечете Monad_Syntax из библиотеки, вы получите одно приложение специальной перегрузки c, которое будет легко сконфигурировано.

Короче говоря: специальная перегрузка c - это механизм для включения «модный» синтаксис в Изабель. Новичков это может смутить, потому что сообщения об ошибках, как правило, трудно понять, если что-то не так во внутреннем переводе.

...