Вы включаете тег «Изабель», и, согласно Wiki Subtyping, Изабель обеспечивает одну форму подтипирования, принудительное подтипирование, хотя, как объяснил Андреас Лохбихлер, у Изабель на самом деле нет подтипирования, как то, что вы хотите (и другие тоже хотят).
Однако вы говорите расплывчатыми обобщениями, поэтому я легко приведу надуманный пример, который соответствует требованиям ваших 5 типов. И хотя это надумано, это не бессмысленно, как я объясню ниже.
(*The 5 types.*)
datatype tA = tA_con int rat real
type_synonym tB = "(nat * int)"
type_synonym tC = int
type_synonym tE = rat
type_synonym tF = real
(*The small amount of code required to automatically coerce from tC to tB.*)
fun coerce_C_to_B :: "tC => tB" where "coerce_C_to_B i = (0, i)"
declare [[coercion coerce_C_to_B]]
(*I can use type tC anywhere I can use type tB.*)
term "(2::tC)::tB"
value "(2::tC)::tB"
В приведенном выше примере видно, что типы tC, tE и tF естественным образом и легко поддаются приведению к типам tA или tB.
Это принуждение типов делается довольно часто в Isabelle. Например, тип nat используется для определения int, а int используется для определения rat. Следовательно, nat автоматически приводится к int, хотя int не соответствует rat.
Wrap I (вы не использовали канонический HOL):
- In your previous question examples, you've been using
typedecl to introduce new types, and that doesn't generally reflect how people define new types.
- Types defined with
typedecl are nearly always foundational and axiomatized, such as with ind, in Nat.thy.
- См. здесь: isabelle.in.tum.de/repos/isabelle/file/8f4a332500e4/src/HOL/Nat.thy#l21
- The keyword
datatype_new is one of the primary, automagical ways to define new types in Isabelle/HOL.
- Part of the power of
datatype_new (and datatype) is its use to define recursive types, and its use with fun, for example with pattern matching.
- По сравнению с другими помощниками по проверке, я полагаю, что новые способности
datatype_new не тривиальны. Например, отличительной особенностью типов и наборов ZFC является то, что наборы ZFC могут быть вложены произвольно глубоко. Теперь с помощью datatype_new можно определить тип счетного или конечного множества, которое может быть вложено сколь угодно глубоко.
- Вы можете использовать стандартные типы, такие как кортежи, списки и записи, для определения новых типов, которые затем можно использовать с приведением, как показано в моем примере выше.
Wrap II (но да, было бы неплохо):
Я мог бы продолжить приведенный выше список, но я отделил от него два других ключевых слова, чтобы определить новые типы, typedef и quotient_type.
Я разделяю эти два, потому что теперь мы вступаем в сферу вашей жалобы на то, что логика Isabelle/HOL во многих случаях не позволяет легко определить отношение типа/подтипа.
Ничего особо не зная, теперь я знаю, что мне следует использовать typedef только в крайнем случае. На самом деле он довольно часто используется в исходниках HOL, но затем разработчикам приходится проделывать много работы, чтобы сделать тип, определенный с его помощью, простым в использовании, например, с fset
Wrap III (однако в этом несовершенном мире нет совершенных):
Вы перечислили трех помощников, которые, вероятно, имеют наибольшую долю рынка: Coq, Isabelle и Agda.
С помощниками по проверке мы определяем ваши приоритеты, проводим исследование, а затем выбираем один, но это похоже на языки программирования. Мы не собираемся получать все ни с одним из них.
Для меня очень важен математический синтаксис и структурированные доказательства. Изабель кажется достаточно сильной, поэтому я выбираю ее. Конечно, это не идеальный мир.
Wrap IV (Haskell, Isablle и классы типов):
У Изабель действительно есть очень мощная форма создания подклассов — классы типов.
Что ж, это мощный инструмент, но он также ограничен тем, что вы можете использовать только одну переменную типа при определении класса типа.
Если вы посмотрите на Groups.thy, вы увидите введение класса за классом за классом, чтобы создать иерархию классов.
- isabelle.in.tum.de/repos/isabelle/file/8f4a332500e4/src/HOL/Groups.thy
Вы также включили тег haskell. Атрибуты функционального программирования Isabelle/HOL с его datatype и классами типов помогают связать использование Isabelle/HOL с использованием Haskell, о чем свидетельствует способность генератора кода Isabelle создавать код Haskell.
person
noAccountHombre
schedule
11.11.2014
