diff --git a/.gitignore b/.gitignore index 65ee745..1f07b18 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,8 @@ *.bbl *.blg *.dvi +*.fdb* +*.fls *.log *.out *~ diff --git a/finite-dtypes.bib b/finite-dtypes.bib index 19d4d2f..57bb784 100644 --- a/finite-dtypes.bib +++ b/finite-dtypes.bib @@ -136,3 +136,18 @@ @Misc{self howpublished = {\url{https://github.com/asajeffrey/finite-dtypes}}, } +@Article{AP16, + author = {A. Abel and B. Pientka}, + title = {Well-founded recursion with copatterns and sized types}, + journal = {J. Functional Programming}, + year = {2016}, + volume = {26}, +} + +@InProceedings{FGGvW18, + author = {D. Frumin and H. Geuvers and L. Gondelman and N. van der Weide}, + title = {Finite Sets in Homotopy Type Theory}, + year = {2018}, + note = {Submitted for publication}, +} + diff --git a/finite-dtypes.lagda b/finite-dtypes.lagda index 1e06697..5b50737 100644 --- a/finite-dtypes.lagda +++ b/finite-dtypes.lagda @@ -315,67 +315,66 @@ In particular, systems programs are usually parameterized by $\kw{WORDSIZE}$, and assume that data fits into memory (for example that arrays are indexed by a word, not by a natural number). -A simple language of finite types is given in Figure~\ref{simple-types}. -In this language, all types are finite, in particular -$\kw{FSet}(n) \in \kw{FSet}(\kw{one} + n)$ -(the size is slightly arbitrary, we could have chosen any increasing -size, for instance $\kw{FSet}(n) \in \kw{FSet}(\kw{one} \ll n)$). - -The system is based on a theory of binary arithmetic, but even -that is definable within the language, for example the type -of bitstrings is definable by induction: +An overview of approaches to finite sets in dependent type theory is +given in~\cite{FGGvW18}, which defines +a type constructor $\mathcal{K}(A)$ (the +Kuratowski-finite subsets of $A$), and defines the finite +types to be a type $A$ together with an $X \in \mathcal{K}(A)$ +such that every $x:A$ has $x \in X$. +Type constructors such as dependent functions and pairs, preserve +finiteness, but the type of finite types is not itself finite. + +In Figure~\ref{simple-types}, we posit a type system with +a type-of-types $\kw{FSet}(n)$, +containing types with at most $2^n$ elements. +In this system, all types are finite, in particular $\kw{FSet}(n) +\in \kw{FSet}(\kw{one} + n)$. We expect that this explicit bound on +the size of $\kw{FSet}(n)$ cannot be expressed internally inside an +off-the-shelf dependent type theory, but we conjecture that an extension +like this is consistent. + +This system is based on a theory of binary arithmetic, but even that is +definable within the language, in the presence of an appropriate +induction principal for binary arithmetic. For example the type of +bitstrings is definable by induction: \begin{code} -/binary/ = /indn/ +/binary/ = & /indn/ (/FSet/) (/unitp/) - (/fn/ n /cdot/ /fn/ A /cdot/ (/bool/ /times/ A)) -\end{code} -For example: -\begin{code} + (/fn/ n /cdot/ /fn/ A /cdot/ (/bool/ /times/ A)) \\ %WORDSIZE = /WORDSIZE/ &/in/ /binary/(/WORDSIZE/) \end{code} -Some issues finite types raise include: -\begin{description} - -\item[Induction:] - As the type for $\kw{WORDSIZE}$ suggests, - this is all spookily cyclic. In particular, binary numbers - are parameterized by their bitlength, which is itself - a binary number. An induction principal is needed, - even if it is extra-logical, similar to - Agda's universe polymorphism~\cite{agda}. We hypothesize - that a theory of irrelevant natural numbers might suffice. - -\item[Path types:] Dependent type systems usually come with an identity type $a - \equiv_A b$ where $a : A$ and $b : A$. - If identity types are interpreted as paths as in Homotopy Type Theory~\cite{hott}, - then the size of $A \equiv_{\kw{FSet}(n)} B$ is at most the size of $A \rightarrow B$, - which would suggest considering $(a \equiv_A b) \in \kw{FSet}(n \ll n)$ - when $A \in \kw{FSet}(n)$. - This makes the type of identities over $A$ much larger than the type of $A$, - which may give problems with, for example, codings of indexed types. - -\item[Theory of binary arithmetic:] - The theory of finite types is very dependent on the theory of bitstrings, - and it is very easy to end up type checking modulo - properties such as associativity and commutativity of $+$. - Such theorems could be handled by an SMT solver, but this has its own - issues, such as type inference and complexity. - -\item[Pointers:] - In systems programming languages such as Rust, cyclic data structures - are mediated by pointers. In a finite type system, we could allow a - type of pointers $\&(A)$ where $\&(A) \in \kw{FSet}(\kw{WORDSIZE})$ - when $A \in \kw{FSet}(n)$. - Pointer creation can fail in low-memory situations, so should be - encapsulated in a monad, similar to Haskell's $\kw{ST}$ monad. - -\item[Error messages:] - Type systems should not just reject incorrect programs, - they should provide useful hits about fixing them. - -\end{description} +As the type for $\kw{WORDSIZE}$ suggests, this is all spookily +cyclic. In particular, binary numbers are parameterized by their +bitlength, which is itself a binary number. A bootstrapping induction principal is +needed, similar to Agda universe +polymorphism~\cite{agda}. We hypothesize that irrelevant +natural numbers might suffice. + +Potential advantages of explicitly finite dependent types +include: +\begin{itemize} + +\item A better fit with systems programming languages such as Rust, + where sized types are the default. + +\item Domain specific techniques for arithmetic can better support + type inference. + +\item Simpler induction schemes, such as over the irrelevant naturals, + similar to the use of sized types in taming coinduction~\cite{AP16}, + but without the use of ordinals. + +\end{itemize} +Dependent type systems usually come with an identity type $a \equiv_A +b$ where $a : A$ and $b : A$. If identity types are interpreted as +paths as in Homotopy Type Theory~\cite{hott}, then the size of $A +\equiv_{\kw{FSet}(n)} B$ is at most the size of $A \rightarrow B$, +which would suggest considering $(a \equiv_A b) \in \kw{FSet}(n \ll +n)$ when $A \in \kw{FSet}(n)$. This makes the type of identities over +$A$ much larger than the type of $A$, which may give problems with, +for example, codings of indexed types. \section{Conclusions} diff --git a/finite-dtypes.pdf b/finite-dtypes.pdf index 55a7874..69b7bd7 100644 Binary files a/finite-dtypes.pdf and b/finite-dtypes.pdf differ