%% Proof trees
\usepackage{bussproofs}
+%% Diagrams
+\usepackage[all]{xy}
+
%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
\definecolor{AgdaBound} {HTML}{000000}
+\definecolor{AgdaHole} {HTML} {FFFF33}
\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
+\DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
+\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
+\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
+\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
+
%% -----------------------------------------------------------------------------
%% Commands
\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
-% TODO make this use AgdaBount
+% TODO make this use AgdaBound
\newcommand{\myb}[1]{\ensuremath{#1}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Kant}}
-\newcommand{\mysynel}[1]{\langle #1 \rangle}
+\newcommand{\mysynel}[1]{#1}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
-\newcommand{\myabs}[2]{\lambda #1 \mapsto #2}
+% TODO \mathbin or \mathre here?
+\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }
-\FrameSep0.3cm
+\FrameSep0.2cm
\newcommand{\mydesc}[3]{
\hfill \textbf{#1} $#2$
\vspace{-0.2cm}
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\mytya}{\myb{A}}
\newcommand{\mytyb}{\myb{B}}
-\newcommand{\myarr}{\mathbin{\textcolor{AgdaDatatype}{\to}}}
-\newcommand{\myprod}{\mathbin{\textcolor{AgdaDatatype}{\times}}}
+\newcommand{\mytycc}{\myb{C}}
+\newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
+\newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
\newcommand{\myctx}{\Gamma}
\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
\newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
-\newcommand{\myabss}[3]{\lambda #1 {:} #2 \mapsto #3}
+% TODO \mathbin or \mathrel here?
+\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
\newcommand{\mytt}{\mydc{tt}}
\newcommand{\myunit}{\mytyc{$\top$}}
-\newcommand{\mypair}[2]{(#1\mathpunct{\textcolor{AgdaInductiveConstructor}{,}} #2)}
-\newcommand{\myfst}[1]{\myapp{\myfld{fst}}{#1}}
-\newcommand{\mysnd}[1]{\myapp{\myfld{snd}}{#1}}
+\newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
+\newcommand{\myfst}{\myfld{fst}}
+\newcommand{\mysnd}{\myfld{snd}}
\newcommand{\myconst}{\myb{c}}
\newcommand{\myemptyctx}{\cdot}
-\newcommand{\myhole}{\AgdaUnsolvedMeta}
+\newcommand{\myhole}{\AgdaHole}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
+\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
+\newcommand{\myleft}[1]{\mydc{left}_{#1}}
+\newcommand{\myright}[1]{\mydc{right}_{#1}}
+\newcommand{\myempty}{\mytyc{$\bot$}}
+\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
+\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
+\newcommand{\myarg}{\_}
+\newcommand{\myderivsp}{\vspace{0.3cm}}
+\newcommand{\mytyp}{\mytyc{Type}}
+\newcommand{\myneg}{\myfun{$\neg$}}
+\newcommand{\myar}{\,}
+\newcommand{\mybool}{\mytyc{Bool}}
+\newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
+\newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
+\newcommand{\myite}[3]{\mysyn{if}\,#1\,\mysyn{then}\,#2\,\mysyn{else}\,#3}
+\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
+\newcommand{\myexi}[3]{(#1 {:} #2) \mysum #3}
%% -----------------------------------------------------------------------------
\iffalse
\begin{code}
module thesis where
-open import Level
\end{code}
\fi
}
The care required during substituting variables for terms is required to avoid
-name capturing.
+name capturing. We will use substitution in the future for other name-binding
+constructs assuming similar precautions.
These few elements are of remarkable expressiveness, and in fact Turing
complete. As a corollary, we must be able to devise a term that reduces forever
A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
this will be the case for an application in which the first term is an
-abstraction, but in general a term is reducible if it appears to the left of a
-reduction rule. When a term contains no redex it's said to be in \emph{normal
- form}. Given the observation above, not all terms reduce to a normal forms:
-we call the ones that do \emph{normalising}, and the ones that don't
-\emph{non-normalising}.
+abstraction, but in general we call aterm reducible if it appears to the left of
+a reduction rule. When a term contains no redexes it's said to be in
+\emph{normal form}. Given the observation above, not all terms reduce to a
+normal forms: we call the ones that do \emph{normalising}, and the ones that
+don't \emph{non-normalising}.
The reduction rule presented is not syntax directed, but \emph{evaluation
strategies} can be employed to reduce term systematically. Common evaluation
\subsection{The simply typed $\lambda$-calculus}
-A convenient way to `discipline' $\lambda$-terms is to assign \emph{types} to
-them, and then check that the terms that we are forming make sense given our
-typing rules \citep{Curry1934}. The first most basic instance of this idea
-takes the name of \emph{simply typed $\lambda$ calculus}.
+A convenient way to `discipline' and reason about $\lambda$-terms is to assign
+\emph{types} to them, and then check that the terms that we are forming make
+sense given our typing rules \citep{Curry1934}. The first most basic instance
+of this idea takes the name of \emph{simply typed $\lambda$ calculus}.
Our types contain a set of \emph{type variables} $\Phi$, which might correspond
to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
types of functions. The language is explicitly typed: when we bring a variable
into scope with an abstraction, we explicitly declare its type. $\mytya$,
-$\mytyb$ will be used to refer to a generic type. Reduction is unchanged from
-the untyped $\lambda$-calculus.
+$\mytyb$, $\mytycc$, will be used to refer to a generic type. Reduction is
+unchanged from the untyped $\lambda$-calculus.
\mydesc{syntax}{ }{
$
resulting term is also well-typed, and preserves the previous type.
\end{description}
-However, STLC buys us much more: every well-typed term is normalising. It is
-easy to see that we can't fill the blanks if we want to give types to the
-non-normalising term shown before:
+However, STLC buys us much more: every well-typed term is normalising
+\citep{Tait1967}. It is easy to see that we can't fill the blanks if we want to
+give types to the non-normalising term shown before:
\begin{equation*}
\myapp{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}
\end{equation*}
\subsection{The Curry-Howard correspondence}
-Moreover,
-we have a product (or pair, or tuple) type $\mytya \myprod \mytyb$ for each pair
-of types $\mytya$ and $\mytyb$, and a function (or arrow) type $\mytya \myarr
-\mytyb$ for each pair of types $\mytya$ and $\mytyb$. $\beta$-reduction is
-unchanged, but we have added reduction rules for products. Products are not
-essential, but they serve as a good example of a type former apart from the
-arrow type.
+It turns out that the STLC can be seen a natural deduction system for
+intuitionistic propositional logic. Terms are proofs, and their types are the
+propositions they prove. This remarkable fact is known as the Curry-Howard
+correspondence, or isomorphism.
+
+The arrow ($\myarr$) type corresponds to implication. If we wish to prove that
+that $(\mytya \myarr \mytyb) \myarr (\mytyb \myarr \mytycc) \myarr (\mytya
+\myarr \mytycc)$, all we need to do is to devise a $\lambda$-term that has the
+correct type:
+\[
+ \myabss{f}{(\mytya \myarr \mytyb)}{\myabss{g}{(\mytyb \myarr \mytycc)}{\myabss{x}{\mytya}{\myapp{g}{(\myapp{f}{x})}}}}
+\]
+That is, function composition. We can extend our bare lambda calculus with
+useful types to represent other logical constructs.
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \myb{x} \mysynsep \myconst \mysynsep
- \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
- (\myapp{\mytmsyn}{\mytmsyn}) \\
- & | & \mytt \mysynsep \mypair{\mytmsyn}{\mytmsyn} \mysynsep
- \myfst{\mytmsyn} \mysynsep \mysnd{\mytmsyn} \\
- \mytysyn & ::= & \mytysyn \myprod \mytysyn \mysynsep
- \mytysyn \myarr \mytysyn \mysynsep
- \mybasety{\myconst} \\
- \myb{x} & \in & \text{Some enumerable set of symbols} \\
- \myconst & \in & \text{Some set $C$ of constants} \\
+ \mytmsyn & ::= & \dots \\
+ & | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
+ & | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
+ \myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
+ \myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
+ & | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
+ \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
+ \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
\end{array}
$
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
\centering{
\begin{tabular}{cc}
- $\myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}$ &
$
- \begin{array}{r@{\ }c@{\ }l}
- \myapp{\myfst}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
- \myapp{\mysnd}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
+ \begin{array}{l@{ }l@{\ }c@{\ }l}
+ \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myleft{\mytya} &}{\mytmt})} & \myred &
+ \myapp{\mytmm}{\mytmt} \\
+ \myapp{\mycase{\mytmm}{\mytmn}}{(\myapp{\myright{\mytya} &}{\mytmt})} & \myred &
+ \myapp{\mytmn}{\mytmt}
+ \end{array}
+ $
+ &
+ $
+ \begin{array}{l@{ }l@{\ }c@{\ }l}
+ \myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
+ \myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
\end{array}
$
\end{tabular}
}
}
-% TODO write context rules
-% \mydesc{validity:}{\myvalid{\myctx}}{
-% \centering{
-% \begin{tabular}{ccc}
-% \AxiomC{}
-% \UnaryInfC{$\myvalid{\myemptyctx}$}
-% \DisplayProof
-% &
-% \AxiomC{$\mytmt : \mytya$}
-% \UnaryInfC{$\myvalid{\myctx; x : \mytya
-% bar &
-% baz
-% \end{tabular}
-% }
-% }
-
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
\centering{
\begin{tabular}{cc}
- \AxiomC{$x : A \in \myctx$}
- \UnaryInfC{$\myjud{x}{A}$}
+ \AxiomC{}
+ \UnaryInfC{$\myjud{\mytt}{\myunit}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\myempty}$}
+ \UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
+ \DisplayProof
+ \end{tabular}
+ }
+ \myderivsp
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\mytyb}$}
+ \UnaryInfC{$\myjud{\myapp{\myright{\mytya}}{\mytmt}}{\mytya \mysum \mytyb}$}
+ \DisplayProof
+
+ \end{tabular}
+ }
+ \myderivsp
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
+ \AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya \mysum \mytyb}$}
+ \TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
+ \DisplayProof
+ \end{tabular}
+ }
+ \myderivsp
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytmn}{\mytyb}$}
+ \BinaryInfC{$\myjud{\mypair{\mytmm}{\mytmn}}{\mytya \myprod \mytyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
+ \UnaryInfC{$\myjud{\myapp{\myfst}{\mytmt}}{\mytya}$}
\DisplayProof
&
- foo
+ \AxiomC{$\myjud{\mytmt}{\mytya \myprod \mytyb}$}
+ \UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
+ \DisplayProof
\end{tabular}
}
}
+Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
+Haskell) correspond to disjunctions, and dually tuples (or pairs, or
+products---$\myprod$ here, tuples in Haskell) correspond to conjunctions. This
+is apparent looking at the ways to construct and destruct the values inhabiting
+those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$
+introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$
+$\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to
+$\wedge$ elimination.
+
+The trivial type $\myunit$ corresponds to the logical $\top$, and dually
+$\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
+rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
+introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
+}$), corresponding to the logical \emph{ex falso quodlibet}. Note that in the
+constructors for the sums and the destructor for $\myempty$ we need to include
+some type information to keep type checking decidable.
+
+As in logic, if we want to keep our system consistent, we must make sure that no
+closed terms (in other words terms not under a $\lambda$) inhabit $\myempty$.
+The variant of STLC presented here is indeed consistent, a result that follows
+from the fact that it is normalising. % TODO explain
+Going back to our $\myfix{ }{ }{ }$ combinator, it is easy to see how it breaks
+our desire for consistency. The following term works for every type $\mytya$,
+including bottom:
+\[
+(\myfix{x}{\mytya}{x}) : \mytya
+\]
+
+With these rules, our STLC now looks remarkably similar in power and use to the
+natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
+\myarr \myempty$. However, there is an important omission: there is no term of
+the type $\mytya \mysum \myneg \mytya$ (excluded middle), or equivalently
+$\myneg \myneg \mytya \myarr \mytya$ (double negation), or indeed any term with
+a type equivalent to those.
+
+This has a considerable effect on our logic and it's no coincidence, since there
+is no obvious computational behaviour for laws like the excluded middle.
+Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
+and all the systems analysed will have this characteristic since they build on
+the foundation of the STLC\footnote{There is research to give computational
+ behaviour to classical logic, but I will not touch those subjects.}.
+
+
\section{Intuitionistic Type Theory}
\label{sec:itt}
+\subsection{Extending the STLC}
+
+The STLC can be made more expressive in various ways. \cite{Barendregt1991}
+succinctly expressed geometrically how we can add expressively:
+
+$$
+\xymatrix@!0@=1.5cm{
+ & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
+ & & \lambda C \ar@{-}[dd]
+ \\
+ \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
+ & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
+ \\
+ & \lambda\underline\omega \ar@{-}'[r][rr]
+ & & \lambda P\underline\omega
+ \\
+ \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
+ & & \lambda P \ar@{-}[ur]
+}
+$$
+Here $\lambda{\to}$, in the bottom left, is the STLC. From there can move along
+3 dimensions:
+\begin{description}
+\item[Terms depending on types (towards $\lambda{2}$)] We can quantify over
+ types in our type signatures. For example, we can defined a polymorphic
+ identity function:
+ $\displaystyle
+ (\myabss{\mytya}{\mytyp}{\myabss{x}{A}{x}}) : (\mytya : \mytyp) \myarr \mytya \myarr \mytya
+ $.
+ The first and most famous instance of this idea has been System F. This gives
+ us a form of polymorphism and has been wildly successful, also thanks to a
+ well known inference algorithm for a restricted version of System F known as
+ Hindley-Milner. Languages like Haskell and SML are based on this discipline.
+\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] We have
+ type operators. For example we could define a function that given types $R$
+ and $\mytya$ forms the type that represents a value of type $\mytya$ in
+ continuation passing style: $\displaystyle(\myabss{A \myar R}{\mytyp}{(\mytya
+ \myarr R) \myarr R}) : \mytyp \myarr \mytyp \myarr \mytyp$.
+\item[Types depending on terms (towards $\lambda{P}$)] Also known as `dependent
+ types', give great expressive power. For example, we can have values of whose
+ type depend on a boolean:
+ $\displaystyle(\myabss{x}{\mybool}{\myite{x}{\mynat}{\myrat}}) : \mybool
+ \myarr \mytyp$.
+\end{description}
+
+All the systems preserve the properties that make the STLC well behaved. The
+system we are going to focus on, Intuitionistic Type Theory, has all of the
+above additions, and thus would sit where $\lambda{C}$ sits in the
+`$\lambda$-cube'.
+
+\subsection{A Bit of History}
+
+Logic frameworks and programming languages based on type theory have a long
+history. Per Martin-L\"{o}f described the first version of his theory in 1971,
+but then revised it since the original version was inconsistent due to its
+impredicativity\footnote{In the early version there was only one universe
+ $\mytyp$ and $\mytyp : \mytyp$, see section \ref{sec:core-tt} for an
+ explanation on why this causes problems.}. For this reason he gave a revised
+and consistent definition later \citep{Martin-Lof1984}.
+
+A related development is the polymorphic $\lambda$-calculus, and specifically
+the previously mentioned System F, which was developed independently by Girard
+and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
+fact is that while System F is impredicative it is still consistent and strongly
+normalising. \cite{Coquand1986} further extended this line of work with the
+Calculus of Constructions (CoC).
+
+\subsection{A core type theory}
+\label{sec:core-tt}
+
+The calculus I present follows the exposition in \citep{Thompson1991}, and is
+quite close to the original formulation of predicative ITT as found in
+\citep{Martin-Lof1984}.
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \myb{x} \\
+ & | & \myunit \mysynsep \mytt \\
+ & | & \myempty \mysynsep \myapp{\myabsurd{\mytmsyn}}{\mytmsyn} \\
+ & | & \myfora{x}{\mytmsyn}{\mytmsyn} \mysynsep
+ \myabss{x}{\mytmsyn}{\mytmsyn} \\
+ & | & \myexi{x}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mypair{\mytmsyn}{\mytmsyn} \mysynsep \myapp{\myfst}{\mytmsyn}
+ \end{array}
+ $
+}
+
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+
+}
+
\section{The struggle for equality}
\label{sec:equality}
Typing derivations here.
}
-In the languages presented I will also use different fonts and colors for
-different things:
+In the languages presented I also highlight the syntax, following a uniform
+color and font convention:
\begin{center}
\begin{tabular}{c | l}
$\mytyc{Sans}$ & Type constructors. \\
$\mydc{sans}$ & Data constructors. \\
% $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
- $\mysyn{roman}$ & Syntax of the language. \\
- $\myfun{roman}$ & Defined values. \\
+ $\mysyn{roman}$ & Keywords of the language. \\
+ $\myfun{roman}$ & Defined values and destructors. \\
$\myb{math}$ & Bound variables.
\end{tabular}
\end{center}
-\section{Agda rendition of a core ITT}
+\section{Agda code}
\label{app:agda-code}
+\subsection{ITT}
+
\begin{code}
module ITT where
- data Empty : Set where
+ open import Level
+
+ data ⊥ : Set where
- absurd : ∀ {a} {A : Set a} → Empty → A
+ absurd : ∀ {a} {A : Set a} → ⊥ → A
absurd ()
- record Unit : Set where
+ record ⊤ : Set where
constructor tt
record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
- fst : A
- snd : B fst
+ fst : A
+ snd : B fst
data Bool : Set where
true false : Bool
- if_/_then_else_ : ∀ {a}
- (x : Bool) → (P : Bool → Set a) → P true → P false → P x
- if true / _ then x else _ = x
- if false / _ then _ else x = x
+ if_then_else_ : ∀ {a} {P : Bool → Set a} (x : Bool) → P true → P false → P x
+ if true then x else _ = x
+ if false then _ else x = x
data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
_◁_ : (s : S) → (P s → W S P) → W S P
rec : ∀ {a b} {S : Set a} {P : S → Set b}
- (C : W S P → Set) → -- some conclusion we hope holds
- ((s : S) → -- given a shape...
- (f : P s → W S P) → -- ...and a bunch of kids...
- ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
- C (s ◁ f)) → -- ...does C hold for the node?
- (x : W S P) → -- If so, ...
- C x -- ...C always holds.
+ (C : W S P → Set) → -- some conclusion we hope holds
+ ((s : S) → -- given a shape...
+ (f : P s → W S P) → -- ...and a bunch of kids...
+ ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
+ C (s ◁ f)) → -- ...does C hold for the node?
+ (x : W S P) → -- If so, ...
+ C x -- ...C always holds.
rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
\end{code}
projects / bitonic-mengthesis.git / commitdiff