# HG changeset patch # User haftmann # Date 1461005778 -7200 # Node ID 9a9c2d846d4a3b0eb901d7844eac69ebbbee56f5 # Parent 92680537201f7ed2db8b79a263674a85563a4bae fragment of a HOL type class primer diff -r 92680537201f -r 9a9c2d846d4a src/Doc/ROOT --- a/src/Doc/ROOT Mon Apr 18 20:56:13 2016 +0200 +++ b/src/Doc/ROOT Mon Apr 18 20:56:18 2016 +0200 @@ -483,3 +483,23 @@ "tutorial.sty" "typedef.pdf" "types0.tex" + +session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = "Typeclass_Hierarchy_Basics" + + options [document_variants = "typeclass_hierarchy"] + theories Typeclass_Hierarchy + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" + +session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL" + + options [document = false] + theories + Setup diff -r 92680537201f -r 9a9c2d846d4a src/Doc/Typeclass_Hierarchy/Setup.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Typeclass_Hierarchy/Setup.thy Mon Apr 18 20:56:18 2016 +0200 @@ -0,0 +1,16 @@ +theory Setup +imports Complex_Main "~~/src/HOL/Library/Lattice_Syntax" +begin + +ML_file "../antiquote_setup.ML" +ML_file "../more_antiquote.ML" + +attribute_setup all = + \Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\ + "quantified schematic vars" + +setup \Config.put_global Printer.show_type_emphasis false\ + +declare [[show_sorts]] + +end diff -r 92680537201f -r 9a9c2d846d4a src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy Mon Apr 18 20:56:18 2016 +0200 @@ -0,0 +1,176 @@ +theory Typeclass_Hierarchy +imports Setup +begin + +section \Introduction\ + +text \ + The {Isabelle/HOL} type-class hierarchy entered the stage + in a quite ancient era -- first related \emph{NEWS} entries date + back to release {Isabelle99-1}. Since then, there have been + ongoing modifications and additions, leading to ({Isabelle2016}) + more than 180 type-classes. This sheer complexity makes access + and understanding of that type-class hierarchy difficult and + involved, let alone maintenance. + + The purpose of this primer is to shed some light on this, + not only on the mere ingredients, but also on the design + principles which have evolved and proven useful over time. +\ + +section \Foundations\ + +subsection \Locales and type classes\ + +text \ + Some familiarity with the Isabelle module system is assumed: + defining locales and type-classes, interpreting locales and + instantiating type-classes, adding relationships between + locales (@{command sublocale}) and type-classes + (@{command subclass}). Handy introductions are the + respective tutorials \cite{isabelle-locale} + \cite{isabelle-classes}. +\ + +subsection \Strengths and restrictions of type classes\ + +text \ + The primary motivation for using type classes in {Isabelle/HOL} + always have been numerical types, which form an inclusion chain: + + \begin{center} + @{typ nat} @{text \} @{typ int} @{text \} @{typ rat} + @{text \} @{typ real} @{text \} @{typ complex} + \end{center} + + \noindent The inclusion @{text \} means that any value of the numerical + type to the left hand side mathematically can be transferred + to the numerical type on the right hand side. + + How to accomplish this given the quite restrictive type system + of {Isabelle/HOL}? Paulson \cite{paulson-numerical} explains + that each numerical type has some characteristic properties + which define an characteristic algebraic structure; @{text \} + then corresponds to specialization of the corresponding + characteristic algebraic structures. These algebraic structures + are expressed using algebraic type classes and embeddings + of numerical types into them: + + \begin{center}\begin{tabular}{lccc} + @{term of_nat} @{text "::"} & @{typ nat} & @{text \} & @{typ [source] "'a::semiring_1"} \\ + & @{text \} & & @{text \} \\ + @{term of_int} @{text "::"} & @{typ int} & @{text \} & @{typ [source] "'a::ring_1"} \\ + & @{text \} & & @{text \} \\ + @{term of_rat} @{text "::"} & @{typ rat} & @{text \} & @{typ [source] "'a::field_char_0"} \\ + & @{text \} & & @{text \} \\ + @{term of_real} @{text "::"} & @{typ real} & @{text \} & @{typ [source] "'a::real_algebra_1"} \\ + & @{text \} \\ + & @{typ complex} + \end{tabular}\end{center} + + \noindent @{text "d \ c"} means that @{text c} is subclass of @{text d}. + Hence each characteristic embedding @{text of_num} can transform + any value of type @{text num} to any numerical type further + up in the inclusion chain. + + This canonical example exhibits key strengths of type classes: + + \<^item> Sharing of operations and facts among different + types, hence also sharing of notation and names: there + is only one plus operation using infix syntax @{text "+"}, + only one zero written @{text 0}, and neutrality + (@{thm add_0_left [all, no_vars]} and + @{thm add_0_right [all, no_vars]}) + is referred to + uniformly by names @{fact add_0_left} and @{fact add_0_right}. + + \<^item> Proof tool setups are shared implicitly: + @{fact add_0} and @{fact add_0_right} are simplification + rules by default. + + \<^item> Hence existing proofs about particular numerical + types are often easy to generalize to algebraic structures, + given that they do not depend on specific properties of + those numerical types. + + Considerable restrictions include: + + \<^item> Type class operations are restricted to one + type parameter; this is insufficient e.g. for expressing + a unified power operation adequately (see \secref{sec:power}). + + \<^item> Parameters are fixed over the whole type class + hierarchy and cannot be refined in specific situations: + think of integral domains with a predicate @{term is_unit}; + for natural numbers, this degenerates to the much simpler + @{term [source] "HOL.equal (1::nat)"} but facts + refer to @{term is_unit} nonetheless. + + \<^item> Type classes are not apt for meta-theory. There + is no practically usable way to express that the units + of an integral domain form a multiplicative group using + type classes. But see session @{text "HOL-Algebra"} + which provides locales with an explicit carrier. +\ + + +subsection \Navigating the hierarchy\ + +text \ + An indispensable tool to inspect the class hierarchy is + @{command class_deps} which displays the graph of classes, + optionally showing the logical content for each class also. + Optional parameters restrict the graph to a particular segment + which is useful to get a graspable view. See + the Isar reference manual \cite{isabelle-isar-ref} for details. +\ + + +section \The hierarchy\ + +subsection \Syntactic type classes\ + +text \ + At the top of the hierarchy there are a couple of syntactic type + classes, ie. classes with operations but with no axioms, + most notably: + + \<^item> @{class plus} with @{term [source] "(a::'a::plus) + b"} + + \<^item> @{class zero} with @{term [source] "0::'a::zero"} + + \<^item> @{class times} with @{term [source] "(a::'a::times) * b"} + + \<^item> @{class one} with @{term [source] "1::'a::one"} + + \noindent Before the introduction of the @{command class} statement in + Isabelle \cite{Haftmann-Wenzel:2006:classes} it was impossible + to define operations with associated axioms in the same class, + hence there were always pairs of syntactic and logical type + classes. This restriction is lifted nowadays, but there are + still reasons to maintain syntactic type classes: + + \<^item> Syntactic type classes allow generic notation to be used + regardless of a particular logical interpretation; e.g. + although multiplication @{text "*"} is usually associative, + there are examples where it is not (e.g. octonions), and + leaving @{text "*"} without axioms allows to re-use this + syntax by means of type class instantiation also for such + exotic examples. + + \<^item> Type classes might share operations but not necessarily + axioms on them, e.g. @{term gcd} (see \secref{sec:gcd}). + Hence their common base is a syntactic type class. + + \noindent However syntactic type classes should only be used with striking + cause. Otherwise there is risk for confusion if the notation + suggests properties which do not hold without particular + constraints. This can be illustrated using numerals + (see \secref{sec:numerals}): @{lemma "2 + 2 = 4" by simp} is + provable without further ado, and this also meets the typical + expectation towards a numeral notation; in more ancient releases + numerals were purely syntactic and @{prop "2 + 2 = 4"} was + not provable without particular type constraints. +\ + +end diff -r 92680537201f -r 9a9c2d846d4a src/Doc/Typeclass_Hierarchy/document/build --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Typeclass_Hierarchy/document/build Mon Apr 18 20:56:18 2016 +0200 @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +set -e + +FORMAT="$1" +VARIANT="$2" + +"$ISABELLE_TOOL" logo Isar +"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" + diff -r 92680537201f -r 9a9c2d846d4a src/Doc/Typeclass_Hierarchy/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Typeclass_Hierarchy/document/root.tex Mon Apr 18 20:56:18 2016 +0200 @@ -0,0 +1,38 @@ +\documentclass[12pt,a4paper,fleqn]{article} +\usepackage{latexsym,graphicx} +\usepackage{iman,extra,isar} +\usepackage{isabelle,isabellesym} +\usepackage{style} +\usepackage{pdfsetup} + +\hyphenation{Isabelle} +\hyphenation{Isar} +\isadroptag{theory} + +\title{\includegraphics[scale=0.5]{isabelle_isar} + \\[4ex] The {Isabelle/HOL} type-class hierarchy} +\author{\emph{Florian Haftmann}} + +\begin{document} + +\maketitle + +\begin{abstract} + \noindent This primer introduces corner stones of the {Isabelle/HOL} + type-class hierarchy and gives some insights into its internal + organization. +\end{abstract} + +\thispagestyle{empty}\clearpage + +\pagenumbering{roman} +\clearfirst + +\input{Typeclass_Hierarchy.tex} + +\begingroup +\bibliographystyle{plain} \small\raggedright\frenchspacing +\bibliography{manual} +\endgroup + +\end{document} diff -r 92680537201f -r 9a9c2d846d4a src/Doc/Typeclass_Hierarchy/document/style.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/Typeclass_Hierarchy/document/style.sty Mon Apr 18 20:56:18 2016 +0200 @@ -0,0 +1,38 @@ + +%% toc +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1} +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}} + +%% paragraphs +\setlength{\parindent}{1em} + +%% references +\newcommand{\secref}[1]{\S\ref{#1}} +\newcommand{\figref}[1]{figure~\ref{#1}} + +%% logical markup +\newcommand{\strong}[1]{{\bfseries {#1}}} + +%% typographic conventions +\newcommand{\qt}[1]{``{#1}''} +\newcommand{\ditem}[1]{\item[\isastyletext #1]} + +%% quote environment +\isakeeptag{quote} +\renewenvironment{quote} + {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax} + {\endlist} +\renewcommand{\isatagquote}{\begin{quote}} +\renewcommand{\endisatagquote}{\end{quote}} +\newcommand{\quotebreak}{\\[1.2ex]} + +%% presentation +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} + +%% character detail +\renewcommand{\isadigit}[1]{\isamath{#1}} +\binperiod + +%% format +\pagestyle{headings} +\isabellestyle{it} diff -r 92680537201f -r 9a9c2d846d4a src/Doc/manual.bib --- a/src/Doc/manual.bib Mon Apr 18 20:56:13 2016 +0200 +++ b/src/Doc/manual.bib Mon Apr 18 20:56:18 2016 +0200 @@ -909,6 +909,18 @@ number = 5, month = May} +@inproceedings{Hoelzl-Huffman-Immler:2013:typeclasses, + author = {Johannes H{\"o}lzl and Fabian Immler and Brian Huffman}, + title = {Type Classes and Filters for Mathematical Analysis in {Isabelle/HOL}}, + booktitle = {Interactive Theorem Proving (ITP 2013)}, + editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David}, + year = 2013, + volume = 7998, + series = LNCS, + publisher = Springer, + isbn = {978-3-642-39633-5}, + pages = {279--294}} + @book{Hudak-Haskell,author={Paul Hudak}, title={The Haskell School of Expression},publisher=CUP,year=2000} @@ -1476,6 +1488,16 @@ month = mar, pages = {175-204}} +@article{paulson-numerical, + author = {Lawrence C. Paulson}, + title = {Organizing numerical theories using axiomatic type + classes}, + journal = JAR, + year = 2004, + volume = 33, + number = 1, + pages = {29-49}} + @manual{isabelle-intro, author = {Lawrence C. Paulson}, title = {Old Introduction to {Isabelle}}, diff -r 92680537201f -r 9a9c2d846d4a src/Doc/more_antiquote.ML --- a/src/Doc/more_antiquote.ML Mon Apr 18 20:56:13 2016 +0200 +++ b/src/Doc/more_antiquote.ML Mon Apr 18 20:56:18 2016 +0200 @@ -1,12 +1,30 @@ (* Title: Doc/more_antiquote.ML Author: Florian Haftmann, TU Muenchen -More antiquotations (depending on Isabelle/HOL). +More antiquotations (partly depending on Isabelle/HOL). *) structure More_Antiquote : sig end = struct +(* class specifications *) + +local + +fun class_spec ctxt s = + let + val thy = Proof_Context.theory_of ctxt; + val class = Sign.intern_class thy s; + in Thy_Output.output ctxt (Class.pretty_specification thy class) end; + +in + +val _ = + Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name) + (fn {context, ...} => class_spec context)); + +end; + (* code theorem antiquotation *) local @@ -21,7 +39,7 @@ val ((_, [thm]), _) = Variable.import true [thm] ctxt'; in thm end; -fun pretty_code_thm src ctxt raw_const = +fun pretty_code_thm ctxt source raw_const = let val thy = Proof_Context.theory_of ctxt; val const = Code.check_const thy raw_const; @@ -33,13 +51,13 @@ |> these |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |> map (holize o no_vars ctxt o Axclass.overload thy); - in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end; + in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt source thms) end; in val _ = Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term - (fn {source, context, ...} => pretty_code_thm source context)); + (fn {source, context, ...} => pretty_code_thm context source)); end;