The Next 700 Module Systems
Extending Dependently-Typed Languages to Implement Module System Features In The Core Language
Table of Contents
1 Introduction —The Proposal's “Story”
In this chapter we aim to present the narrative that demonstrates the distinction between what can currently be accomplished and what is desired when working with composition of software units. We arrive at the observation that packaging concepts differ only in their use –for example, a typeclass and a record are both sequences of declarations that only differ in the former used for polymorphism with instance search whereas the latter is used as a structure grouping related items together. In turn, we are led to propose that the various packaging concepts ought to have a uniform syntax. Moreover, since records are a particular notion of packaging, the commitment to syntactic similarity gives rise to a homoiconic nature to the host language.
Within this work we refer to a simple type theory as a language that contains typed lambda terms for terms and formuale; if in addition it contains typed lambda terms for ‘proofs’ —which are members of types that could be interpreted as propositions— then we say it is a dependently-typed language, or ‘DTL’ for short. More precisely, if type formation is indexed, i.e., types may depend on a context, then we have a DTL. With the exception of declarations and ephemeral notions, nearly everything in a DTL is a typed lambda term. Just as Lisp's homoiconic nature blurs data and code leaving it not as a language with primitives but rather a language with meta-primitives, so too the lack of distinction between term and type lends itself to generic and uniform concepts in DTLs thereby leaving no syntactic distinction between a constructive proof and an algorithm.
Proofs are not a necessary ingredient for dependent types (and are anyways only a matter of intent, as you yourself also emphasised in the last meeting).
The sections below explore our primary observation, which is discussed further later on in chapter 3 as preliminary research. Section 1 demonstrates the variety of languages present in a single system which are conflated in a DTL, section 2 discusses that such conflation should by necessity apply to notions of packaging, and section 3 concludes with proposed work to ensure that happens.
- In the introduction to section 1, you discuss "the variety of languages present in a single system". I feel this makes sense after reading "A coding language is actually many languages working together" below, but I found it confusing on first read. Maybe put languages in quotes and change system to language?
1.1 A Language Has Many Tongues
A programming language is actually many languages working together.
The most basic of imperative languages comes with a notion of ‘statement’ that is executed
by the computer to alter ‘state’ and a notion of ‘value’ that can be assigned to memory locations.
Statements may be sequenced or looped, whereas values may be added or multiplied, for example.
In general, the operations on one linguistic category cannot be applied to the other.
Unfortunately, a rigid separation between the two sub-languages means that binary choice, for example,
conventionally invites two notations with identical semantics —e.g.; in C
one writes if (cond) clause₁ else clause₂
for statements but must use the notation cond?term₁:term₂
for values.
Hence, there are value and statement languages.
Let us continue using the C
language for our examples since it is so ubiquitous
and has influenced many languages. Such a choice has the benefit of referring to
a concrete language, rather than speaking in vague generalities.
Besides Agda –a language mentioned throughout the proposal–
we shall also refer to Haskell as a representative of the functional
side of programming. For example, in Haskell there is no distinction between values and statements
—the latter being a particular instance of the former— and so it uses the same notation if_then_else_
for both.
However, in practice, statements in Haskell are more pragmatically used as a body of a do
block for which
the rules of conditionals and local variables change –hence, Haskell is not as uniform as it initially appears.
In C
, one declares an integer value by int x;
but a value of a user-defined type T
is declared struct T x;
since, for simplicity, one may think of C
having an array named struct
that contains the definitions of user-defined types T
and the notation struct T
acts as an array access.
Since this is a clunky notation, we can provide an alias using the declaration typedef existing-name new-name;
.
Unfortunately, the existing name must necessarily be a type, such as struct T
or int
, and cannot be an arbitrary
term. One must use #define
to produce term aliases, which are handled by the C
preprocessor,
which also provides #include
to import existing libraries.
Hence, the type language is distinct from the libraries language, which is part of the preprocessor language.
In contrast, Haskell has a pragma language for enabling certain features of the compiler. Unlike C
, it
has an interface language using typeclass
-es which differs from its module
language
\parencite{haskell_modules_formally, haskell_in_haskell, classic_haskell_genericity}
since the former's names
may be qualified by the names of the latter but not the other way around. In turn, typeclass
names may be used
as constraints on types, but not so with module
names. It may be argued that this interface language is part
of the type language, but it is sufficiently different that it could be thought of as its own language \parencite{modular_modules}
—for example, it comes with keywords class, instance, =>
that can only appear in special phrases.
In addition, by default, variable declarations are the same for built-in and user-defined types –whereas C
requires using typedef
to mimic such behaviour.
However, Haskell distinguishes between term and type aliases.
In contrast, Agda treats aliasing as nothing more than a normal definition.
Certain application domains require high degrees of confidence in the correctness of software.
Such program verification settings may thus have an additional specification language.
For C
, perhaps the most popular is the ANSI C Specification Language, ACSL \parencite{acsl}.
Besides the C
types, ACSL provides a type integer
for specifications referring to unbounded integers
as well as numerous other notions and notations not part of the C
language. Hence, the specification language
generally differs from the implementation language. In contrast, Haskell's specification are generally \parencite{programatica} in comments
but its relative Agda allows specifications to occur at the type level.
Whether programs actually meet their specifications ultimately requires a proof language. For example, using the Frama-C tool \parencite{frama_c}, ACSL specifications can be supported by Isabelle or Coq proofs. In contrast, being dependently-typed, Agda allows us to use the implementation language also as a proof language ---the only distinction is a shift in our perspective; the syntax is the same. Tools such as Idris and Coq come with ‘tactics’ —algorithms which one may invoke to produce proofs— and may combine them using specific operations that only act on tactics, whence yet another tongue.
Hence, even the simplest of programming languages contain the first three of the following sub-languages –types may be treated at runtime.
- Expression language;
- Statement, or control flow, language;
- Type language;
- Specification language;
- Proof language;
- Module language;
- Meta-programming languages —including Coq tactics, C preprocessor, Haskell pragmas, Template Haskell's various quotation brackets
[x| ... ]
, Idris directives, etc.
As briefly discussed, the first five languages telescope down into one uniform language within the dependently-typed language Agda. So why not the module language?
1.2 Needless Distinctions for Containers
Computing is compositionality. Large mind-bending software developments are formed by composing smaller, much more manageable, pieces together. How? In the previous section we outlined a number of languages equipped with term constructors, yet we did not indicate which were more primitive and which could be derived.
The methods currently utilised are ‘ad hoc’, e.g., “dump the contents of packages into a new \"uber package”. What about when the packages contain conflicting names? “Make an uber package with field names for each package's contents”. What about viewing the new uber package as a hierarchy of its packages? “Make conversion methods between the two representations.” ─This should be mechanically derivable.
In general, there are special-purpose constructs specifically for working with packages of “usual”, or “day-to-day” expression- or statement-level code. That is, a language for working with containers whose contents live in another language. This forces the users to think of these constructs as rare notions that are rarely needed —since they belong to an ephemeral language. They are only useful when connecting packages together and otherwise need not be learned.
When working with mutually dependent modules, a simple workaround to cyclic
typechecking and loading is to create an interface file containing the
declarations that dependents require. To mitigate such error-prone duplication of
declarations, one may utilise literate programming to tangle the declarations to
multiple files —the actual parent module and the interface module.
This was the situation with Haskell before its recent module signature
mechanism \parencite{haskell_backpack}.
Being a purely functional language, it is unsurprising that Haskell treats
nested record field updates awkwardly: Where a C-like language may have \newline
a.b.c := d
, Haskell requires a { b = b a {c = d}}
which necessarily has
field names b, c
polluting the global function namespace as field projections.
Since a record is a possibly deeply nested list of declarations,
it is trivial to flatten such a list to mechanically generate the names
“a-b-c”
—since the dot is reserved— unfortunately this is not possible
in the core language thereby forcing users to employ ‘lenses’ to generate such
accessors by compile-time meta-programming.
In the setting of DTLs, records in the form of nested Σ-types
tend to have tremendously poor performance
—in existing implementations of Coq \parencite{coq_cat_experiences} and Agda \parencite{perna},
the culprit generally being projections.
More generally,
what if we wanted to do something with packages that the host language does not
support? “Use a pre-processor, approximate packaging at a different language level,
or simply settle with what you have.”
Main Observation Packages, modules, theories, contexts, traits, typeclasses, interfaces, what have you all boil down to dependent records at the end of the day and really differ in how they are used or implemented. At the end of section 3 we demonstrate various distinct presentations of such notions of packaging arising from a single package declaration.
1.3 Proposed Contributions
The proposed thesis investigates the current state of the art of grouping mechanisms \newline —sometimes referred to as modules or packages—, their shortcomings, and a route to implementing candidate solutions based upon a dependently-typed language.
The introduction of first-class structuring mechanisms drastically changes the situation by allowing the composition and manipulation of structuring mechanisms within the language itself. Granted, languages providing combinators for structuring mechanisms are not new; e.g., such notions already exist for Full Maude \parencite{maude_module_algebra} and B \parencite{B_reuse}. The former is closer in spirit to our work, but it differs from ours in that it is based on a reflective logic: A logic where certain aspects of its metatheory can be faithfully represented within the logic itself. It may well be that the meta-theory of our effort may involve reflection, yet our distinction is that our aim is to form powerful module system features for Dependently-Typed Languages (DTLs).
To the uninitiated, the shift to DTLs may not appear useful, or at least would not differ much from existing approaches. We believe otherwise; indeed, in programming and, more generally, in mathematics, there are three —below: 1, 2a, 2b— essentially equivalent perspectives to understanding a concept. Even though they are equivalent, each perspective has prompted numerous programming languages; as such, the equivalence does not make the selection of a perspective irrelevant. The perspectives are as follows:
“Point-wise” or “Constituent-Based”: A concept is understood by studying the concepts it is “made out of”. Common examples include:
- A mathematical set is determined by the elements it contains.
- A method is determined by the sequence of statements or expressions it is composed from.
- A package —such as a record or data declaration— is determined by its components, which may be thought of as fields or constructors.
Object-oriented programming is based on the notion of inheritance which informs us of “has a” and “is a” relationships.
“Point-free” or Relationship Based: A concept is understood by its relationship to other concepts in the domain of discourse. This approach comes into two sub-classifications:
“First Class Citizen” or “Concept as Data”: The concept is treated as a static entity and is identified by applying operations onto it in order to observe its nature. Common examples include:
- A singleton set is a set whose cardinality is 1.
- A method, in any coding language, is a value with the ability
to act on other values of a particular type.
- A renaming scheme to provide different names for a given package;
more generally, applicative modules.
“Second Class Citizen” or “Concept as Method”: The concept is treated as a dynamic entity that is fed input stimuli and is understood by its emitted observational output. Common examples include:
- A singleton set is a set for which there is a unique mapping to it
from any other set. Input any set, obtain a map from it to the singleton set.
- A method, in any coding language, is unique up to observational equality:
Feed it arguments, check its behaviour. Realistically, one may want to also consider efficiency matters.
- Generative modules as in the
new
keyword from Object oriented programming:
Basic construction arguments are provided and a container object is produced.
Observing such a sub-classification as distinct led to traditional structural programming languages, whereas blurring the distinction somewhat led to functional programming.
A simple selection of equivalent perspectives leads to wholly distinct paradigms of thought. It is with this idea that we propose an implementation of first-class grouping mechanisms in a dependently typed language —theories have been proposed, on paper, but as just discussed actual design decisions may have challenging impacts on the overall system. Most importantly, this is a requirements driven approach to coherent modularisation constructs in dependently typed languages.
Later on, we shall demonstrate that with a sufficiently expressive type system, a number of traditional programming notions regarding ‘packaging up data’ become conflated —in particular: Records and modules; which for the most part can all be thought of as ``dependent products with named components''. Languages without such expressive type systems necessitate certain constraints on these concepts according to their intended usage —e.g., no multiple inheritance for Java's classes and only one instance for Haskell's typeclasses. It is not clear whether such constraints have been brought to more expressive languages out of necessity, convention, or convenience. Hence we propose a systematic exploration of the structuring-mechanism design space for DTLs as a starting point for the design of an appropriate dependently-typed module system. Along the way, we intend to provide a set of atomic combinators that suffice as building blocks for generally desirable features of grouping mechanisms, and moreover we intend to provide an analyses of their interactions.
That is, we want to look at the edge cases of the design space for structuring-mechanism systems, not only what is considered `convenient' or `conventional'. Along the way, we will undoubtedly encounter `useless' or non-feasible approaches. The systems we intend to consider would account for, say, module structures with intrinsic types —hence treating them as first class concepts— so that our examination is based on sound principles.
Understandably, some of the traditional constraints have to do with implementations. For example, a Haskell typeclass is generally implemented as a dictionary that can, for the most part, be inlined whereas a record is, in some languages, a contiguous memory block: They can be identified in a DTL, but their uses force different implementation methodologies and consequently they are segregated under different names.
In summary, the proposed research is to build upon the existing state of module systems \parencite{types_for_modules} in a dependently-typed setting \parencite{dtls_give_modules} which is substantiated by developing an extension to a compiler. The intended outcomes include:
- A clean module system for DTLs that treats modules uniformly as any other value type.
- A variety of use-cases contrasting the resulting system with previous approaches.
- A module system that enables rather than inhibits efficiency.
- Demonstrate that module features traditionally handled using meta-programming can be brought to the data-value level; thereby not actually requiring the immense power and complexity of meta-programming.
Most importantly, we intend to implement our theory to obtain validation that it ‘works’.
1.4 Overview of the Remaining Chapters
When a programming languages does not provide sufficiently expressive primitives for a concept —such as typeclass derivation \parencite{deriving_via}— users use some form of pre-processing to accomplish their tasks. In our case, the insufficient primitives are regarding the creation and manipulation of theories —i.e., records, classes, packages, modules. In section 3, we will demonstrate an undisciplined prototype that clarified the requirements of our envisioned system. Even though the prototype appears to be metaprogramming, the aim is not to force users interested in manipulating packages to worry about the intricacies of representations; that is, the end goal is to avoid metaprogramming —which is an over-glorified form of preprocessing. The goal is to use a dependently-typed language to implement the ‘missing’ module system features directly inside the language.
The remainder of the thesis proposal is organised as follows.
- Chapter II discusses what is expected of modularisation mechanisms, how they could be simulated, their interdefinability in Agda, and discuss a theoretical basis for modularisation.
- Chapter III outlines missing features from current modularisation systems, their use cases, and provides a checklist for a candidate module system for DTLs.
- Chapter IV discusses issues regarding implementation matter and the next steps in this research, along with a proposed timeline.
- Chapter V outlines the intended outcomes of this research effort.
An important design decision is whether the resulting development is intended to be reasoned about or not. If reasoning is important, then a language that better supports it is ideal. That is why we are using Agda –using a simpler language and maintaining data invariants eventually becomes much harder \parencite{hasochism}.
Let us conclude by attempting to justify the title of this thesis proposal.
Landin's The Next 700 Programming Languages \parencite{seven_hundred_langs}
inspired a number of works, including
\parencite{seven_hundred_tt_models,seven_hundred_provers, seven_hundred_hoas,seven_hundred_libraries, seven_hundred_data}
and more.
The intended aim of the thesis is a requirements driven approach to coherent
modularisation constructs in DTLs. In particular, we wish to extend Agda
to be powerful enough to implement the module system features, in the core language,
that people actually want and currently mimic by-hand or using third-party preprocessors.
An eager fix would be to provide metaprogramming features,
but unless one is altering the syntax or producing efficient code, this is
glorified pre-processing —it is a means to fake missing abstraction features.
Moreover, metaprogramming would be a hammer too big for the nail we are interested in;
so big that its introduction might ruin the soundness of the DTLs
—e.g., two terms may be ill-typed and ill-formed, such as x +
and 5 = 3
, but
are meaningful when joined together, as in x + 5 = 3
.
Our aim is to provide just the right level of abstraction so that, if anything,
users can write a type of container or method upon it then derive ‘700’ simple
alternate views of the same container and method.
To be clear, consider a semi-ring —or any simple record of 17 different kinds of data. A semi-ring consists of two monoids —each consisting of a total of 7 items of data and proof matter— where one of them is commutative and there are two distributivity axioms. Hence, a semi-ring consists of 17 items. If we wanted to expose, say, 3 such items —for example, the shared carrier and the identities of each monoid— then there are a total of \(\binom{17}{3} = 680\) ways, and if we jump to 4 items we have \(\binom{17}{4} = 2380\) possible forms. Of course these numbers are only upper bounds when record fields depend on earlier items. In section 3, we provide explicit examples of different structural presentations of packages.
Usually, library designers provide one or two views, along with conversion functions, and commit to those; instead we want to liberate them to choose whatever presentation is convenient for the tasks at hand and to work comfortably with the guarantee that all the presentations are isomorphic. Humans should be left to tackle difficult and interesting problems; machines should derive the tedious and uninteresting —even if it's simple, it saves time, is less error-prone, and clearly communicates the underlying principle.
If anything, our aim is practical —to save developers from ad hoc copy-paste preprocessing hacks.
2 Current Approaches
Structuring mechanisms for proof assistants are seen as tools providing administrative support for large mechanisation developments \parencite{LF_practical_module_system}, with support for them usually being conservative: Support for structuring-mechanisms elaborates, or rewrites, into the language of the ambient system's logic. Conservative extensions are reasonable to avoid bootstrapping new foundations altogether but they come at the cost of limiting expressiveness to the existing foundations; thereby possibly producing awkward or unusual uses of linguistic phrases of the ambient language.
We may use the term ‘module’ below due to its familiarity, however some of the issues addressed also apply to other instances of grouping mechanisms —such as records, code blocks, methods, files, families of files, and namespaces.
In section 2.1 we define modularisation; in section 2.2 we discuss how to simulate it, and in section 2.3 we review what current systems can and cannot do; then in section 2.4 we provide legitimate examples of the interdefinability of different grouping mechanisms within Agda. We conclude in section 2.5 by taking a look at an implementation-agnostic representation of grouping mechanisms that is sufficiently abstract to ignore any differences between a record and an interface but is otherwise sufficiently useful to encapsulate what is expected of module systems. Moreover, besides looking at the current solutions, we also briefly discuss their flaws.
2.1 Expectations of Module Systems
Packaging systems are not so esoteric that we need to dwell on their uses; yet we recall primary use cases to set the stage for the rest of our discussions.
- Namespacing
Modules provide new unique local scopes for identifiers thereby permitting de-coupling.
The ability to have multiple files contribute to the same namespace is also desirable for de-coupled developments. This necessitates an independence of module names from the names of physical files —such de-conflation permits recursive modules.
- Information Hiding
- Modules ought to provide the ability to enforce content not to be accessible, or alterable, from outside of the module to enforce that users cannot depend on implementation design decisions.
- Citizenship
Grouping mechanisms need not be treated any more special than record types. As such, one ought to be able to operate on them and manipulate them like any first-class citizen.
In particular, packages themselves have types which happen to be packages. This is the case with universal algebra, and OCaml, where ‘structures’ are typed by ‘signatures’ —note that OCaml's approach is within the same language, whereas, for example, Haskell's recent retrofitting \parencite{haskell_backpack}, of its weak module system to allow such interfacing, is not entirely in the core language since, for example, instantiating happens by the package manager rather than by a core language declaration.
- Polymorphism
Grouping mechanisms should group all kinds of things without prejudice.
This includes ‘nested datatypes’: Local types introduced for implementation purposes, where only certain functionality is exposed. E.g., in an Agda record declaration, it may be nice to declare a local type where the record fields refer to it. This approach naturally leads into hierarchical modules as well.
Interestingly, such nesting is expressible in Cayenne, a long-gone predecessor of Agda. The language lived for about 7 years and it is unclear why it is no longer maintained. Speculation would be that dependent types were poorly understood by the academics let alone the coders —moreover, it had essentially one maintainer who has since moved on to other projects.
With the metaprogramming inspired approach we are proposing, it is only reasonable that, for example, one be able to mechanically transform a package with a local type declaration into a package with the local declaration removed and a new component added to abstract it. That is, a particular implementation is no longer static, but dynamic.
It would not be unreasonable to consider adding to this enumeration:
- Sharing
- The computation performed for a module parameter should be shared across its constituents, rather than inefficiently being recomputed for each constituent —as is the case in the current implementation of Agda.
It is however debatable whether the following is the ‘right’ way to incorporate object-oriented notions of encapsulation.
- Generative modules
A module, rather than being pure like a function, may have some local state or initial setup that is unique to each ‘instantiation’ of the module —rather than being purely applying a module to parameters.
SML supports such features. Whereas Haskell, for example, has its typeclass system essentially behave like an implicitly type-indexed record for the ‘unnamed instance record’ declarations; thereby rendering useless the interfaces supporting, say, only an integer constant.
- Subtyping
This gives rise to ‘heterogeneous equality’ where altering type annotations can suddenly make a well-typed expression ill-typed. E.g., any two record values are equal at the subtype of the empty record, but may be unequal at any other type annotation.
Since a package could contain anything, such as notational declarations, it is unclear how even homogeneous equality should be defined —assuming notations are not part of a package's type.
There are many other concerns regarding packages —such as deriving excerpts, decoration with higher-order utilities, literate programming support, and matters of compilation along altered constituents— but they serve to distract from our core discussions and are thus omitted.
2.2 Ad hoc Grouping Mechanisms
Many popular coding languages do not provide top-level modularisation mechanisms, yet users have found ways to emulate some or all of their requirements. We shall emphasise a record-like embedding in this section, then illustrate it in Agda in the next section.
Namespacing: Ubiquitous languages, such as C, Shell, and JavaScript, that do not
have built-in support for namespaces mimic it by a consistent naming
discipline as in \newline theModule_theComponent
. This way, it is clear where theComponent
comes from; namely, the `module' theModule
which may have its interface expressed as a
C header file or as a JSON literal. This is a variation of
Hungarian Notation \cite{hungarian_notation}.
Incidentally, a Racket source file, module, and `language' declaration
are precisely the same.
Consequently, Racket modules, like OCaml's, may contain top-level
effectful expressions.
In a similar fashion, Python packages
are directories containing an __init__.py
file which is used for the the same
purpose as Scala's package object
's —for package-wide definitions.
Objects: An object can be simulated by having a record structure contain the properties of the class which are then instantiated by record instances. Public class methods are then normal methods whose first argument is a reference to the structure that contains the properties.
Template | \(\qquad\text{has a}\qquad\) | Instance |
≈ class | ≈ object | |
≈ type | ≈ value | |
≈ theorem statement | ≈ witnessing proof | |
≈ specification | ≈ implementation | |
≈ interface | ≈ implementation | |
≈ signature | ≈ algebra | |
≈ logic | ≈ theory |
Modules: Languages that do not support a module may mimic it by placing ``module contents'' within a record. Keeping all contents within one massive record also solves the namespacing issue.
In JavaScript, for example, a module is a JSON literal —i.e., a comma separated list of key-value pairs. Moreover, encapsulation is simulated by having the module be encoded as a function that yields a record which acts as the public contents of the module, while the non-returned matter is considered private. Due to JavaScript's dynamic nature we can easily adjoin functionality to such `modules' at any later point; however, we cannot access any private members of the module. This inflexibility of private data is a heavy burden in an Object Oriented Paradigm.
Sub-Modules: If a module is encoded as a record, then a sub-module is a field in the record which itself happens to be a module encoding.
Parameterised Modules: If a module can be considered as encoded as the returned record from a function, then the arguments to such a function are the parameters to the module.
Mixins: A mixin is the ability to extend a datatype X with functionality Y long after, and far from, its definition. Mixins ‘mix in’ new functionality by permitting X obtains traits Y —unlike inheritance which declares X is a Y. Examples of this include Scala's traits, Java's inheritance, Haskell's typeclasses, and C#'s extension methods.
Typescript \parencite{understanding_typescript}
occupies an interesting position with regards to mixins: It is one of the few
languages to provide union and intersection combinators for its interface
grouping mechanism,
thereby most easily supporting the little theories \parencite{little_theories}
method and making theories a true lattice. Interestingly intersection of interfaces
results in a type that contains the declarations of its arguments and if a field
name has conflicting types then it is, recursively, assigned the intersection of the distinct types
—the base cases of this recursive definition are primitive types, for which distinct types yield an empty intersection.
In contrast, its union types are disjoint sums.
In the dependently-typed setting, one also obtains so-called ‘canonical structures’ \parencite{coq_canonical}, which not only generalise the previously mentioned mixins but also facilitate a flexible style of logic programming by having user-defined algorithms executed during unification; thereby permitting one to omit many details \parencite{coq_canonical_tutorial} and have them inferred. As mentioned earlier regarding objects, we could simulate mixins by encoding a class as a record and a mixin as a record-consuming method. Incidentally languages admitting mixins give rise to an alternate method of module encoding: A ‘module of type M’ is encoded as an instantiation of the mixin trait M.
These natural encodings only reinforce our idea that there is no real essential difference between grouping mechanisms: Whether one uses a closure, record, or module is a matter of preference the usage of which communicates particular intent.
2.3 Existing Systems
Is there any actual need for the proposed research? Are the goals easily adaptable from the simply-typed settings? Is the declared arena of dependently-typed languages sufficiently intricate to warrant this much attention?
In this section, we shall outline that DTLs constitute a difficult and poorly understood domain in comparison to conventional programming languages, such as the purely functional Haskell or the imperative Java. Then we outline the merits of including dependent types. Finally, we close with a comparison of some of the most popular DTLs.
We want to implement solutions in a dependently typed language. Let us discuss which are active and their capabilities.
Dependent-types provide an immense level of expressivity thereby allowing varying degrees of precision to be embedded, or omitted, from the type of a declaration. This overwhelming degree of freedom comes at the cost of common albeit non-orthogonal styles of coding and compilation, which remain as open problems that are only mitigated by awkward workarounds such as Coq's distinction of types and propositions for compilation efficiency. The difficulties presented by DTLs are outweighed by the opportunities they provide \cite{dtl_why} —of central importance is that they blur distinctions between usual programming constructs, which is in alignment with our thesis.
To the best of our knowledge, as confirmed by Wikipedia in \parencite{wiki_proof_assistants, wiki_proof_assistants_dependent}, there are currently less than 15 actively developed dependently-typed languages in-use that are also used as proof-assistants —which are intersting to us since we aim to mechanise all of our results: Algorithms as well as theorems.
Agda \parencite{agda_overview, agda_thesis}: One of the more popular proof assistants around; possibly due to its syntactic inheritance from Haskell —as is the case with Idris. Its Unicode mixfix lexemes permit somewhat faithful renditions of informal mathematics; e.g., calculational proofs can be encoded to be read by those unfamiliar with the system. It also allows traditional functional programming with the ability to `escape under the hood' and write Haskell code. The language has not been designed solely with theorem proving in mind, as is the case for Coq, but rather has been designed with dependently-typed programming in mind \parencite{agda_web, agda_plf}.
The current implementation of the Agda language has a notion of second-class modules which may contain sub-modules along with declarations and definitions of first-class citizens. The intimate relationship between records and modules is perhaps best exemplified here since the current implementation provides a declaration to construe a record as if it were a module. This change in perspective allows Agda records to act as Haskell typeclasses. However, the relationship with Haskell is only superficial: Agda's current implementation does not support sharing. In particular, a parameterised module is only syntactic sugar such that each member of the module actually obtains a new functional parameter; as such, a computationally expensive parameter provided to a module invocation may be intended to be computed only once, but is actually computed at each call site.
Coq \parencite{coq_implementation, coq_cat_experiences}: Unquestionably one of, if not, the most popular proof assistant around. It has been used to produce mechanised proofs of the infamous Four Colour Theorem \parencite{coq_four_colour}, the Feit-Thompson Theorem \parencite{coq_feit}, and an optimising compiler for the C language: CompCert \parencite{coq_compcert, compcert_paper}.
Unlike Agda, Coq supports tactics \parencite{tacticstype} -a brute force approach that renders (hundredfold) case analysis as child's play: Just refine your tactics till all the subgoals are achieved. Ultimately the cost of utilising tactics is that a tactical proof can only be understood with the aid of the system, and may otherwise be un-insightful and so failing to meet most of the purposes of proof \parencite{purposes_of_proof} —which may well be a large barrier for mathematicians who value insightful proofs.
The current implementation of Coq provides the base features expected of any module system.
A notable difference from Agda is that it allows “copy and paste”
contents of modules using the include keyword. Consequently it provides a number
of module combinators, such as <+
which is the infix form of module inclusion
\parencite{coq_manual}. Since Coq module types are essentially contexts,
the module type X <+ Y <+ Z
is really the catenation of contexts, where later
items may depend on former items. The Maude \parencite{maude, maude_module_algebra} framework
contains a similar yet more comprehensive algebra of modules and how they
work with Maude theories. An important aspect of the thesis work will be to
actually investigate Maude further and attempt to reproduce and generalise
some of the use cases in ‘the Maude book’ \parencite{maude} using a core
set of packaging primitives for DTLs —we will return to what such primitives may be
in a later section, on preliminary research.
The Common Algebraic Specification Language
\parencite{casl_overview, casl_user_manual, casl_reference_manual}
will also be investigated with the aim of extracting, and generalising, useful module combinators
and their properties.
Maude is based on rewriting logic, which uses term rewrite rules in two roles:
- as equations, for algebraic specification
- as (labelled) transitions.
In the resulting transition systems, a ``state'' is an equivalence class of value terms modulo the associated set of equations, and transitions are rewrites using the second class of rules.
Theories (and functional modules fmod) can only contain equations.
Incidentally, Coq modules are essentially Agda records —which is unsurprising since our thesis states packaging containers are all essentially the same. In more detail, both notions coincide with that of a signature —a sequence of pairs of name-type declarations. Where Agda users would speak of a record instance, Coq users would speak of a module implementation. To make matters worse, Coq has a notion of records which are far weaker than Agda's; e.g., by default all record field names are globally exposed and records are non-recursive.
Coq's module system extends that of OCaml; a notable divergence is that Coq permits parameterised module types —i.e., parameterised record types, in Agda parlance. Such module types are also known as ‘functors’ by Coq and OCaml users; which are “generative”: Invocations generate new datatypes. Perhaps an example will make this rather strange concept more apparent.
-- Coq -- Corresponding Agda Module Type Unit. End Unit. -- record Unit : Set where Module TT <: Unit. End TT. -- tt : Unit; tt = record {} Module F (X : Unit). -- module F (X : Unit) where End F. -- data t : Set where C : t Module A := F TT. -- module A = F tt Module B := F TT. -- module B = F tt Fail Check eq_refl : A.t = B.t. -- ≠ eq : A.t ≡ B.t ; eq = refl
As seen, in Coq the inductive types are different yet in Agda they are the same. This is because Agda treats such parameterised records, or functors, as ‘applicative’: They can only be applied, like functions.
record Unit : Set where
tt : Unit tt = record {}
module F (X : Unit) where data t : Set where C : t
module A = F tt
module B = F tt
open import Relation.Binary.PropositionalEquality
it : A.t ≡ B.t it = refl
For simplicity, we may think of generative functor applications F X
as actually
F X t
where t
is an implicit tag such as textual position or clock time.
From an object-oriented programming perspective,
F X
for a generative functor F
is like the
new
keyword in Java/C#: A new instance is created
which is distinct from all other instances even though
the same class is utilised. So much for the esotericity of generative functors.
Unlike Agda, which uses records to provide traditional record types, Haskell-like typeclasses, and even a module perspective of both, Coq utilises distinct mechanisms for typeclasses and canonical structures. In contrast, Agda allows named instances since all instances are named and can be provided where an implicit failed to be found. Moreover, Coq's approach demands greater familiarity with the unifer than Agda's approach.
Idris \parencite{idris_main}: This is a general purpose, functional, programming language with dependent types; alongside ATS, below, it is perhaps the only language in this list that can truthfully boast to being general purpose and to have dependent types. It supports both equational and tactic based proof styles, like Agda and Coq respectively; unlike these two however, Idris erases unused proof-terms automatically rather than forcing the user to declare this far in advance as is the case with Agda and Coq. The only (negligible) downside, for us, is that the use of tactics creates a sort of distinction between the activities of proving and programming, which is mostly fictitious.
Moreover, Idris compiles to C whereas Agda compiles to Haskell thereby opening the possibility to use GHC's many optimisations without too much translation from the source: In contrast, Idris programs must be first transformed to their imperative counterparts \parencite{idris_website, idris_tdd}.
Intended to be a more accessible and practical version of Agda, Idris
implements the base module system features and includes interesting new ones.
Until recently, in Agda, one would write module _ (x : ℕ) where ⋯
to parameterise every
declaration in the block “⋯” by the name x
; whereas in Idris, one writes
parameters (x : ℕ) ⋯
to obtain the same behaviour
–which Agda has since improved upon it via ‘generalisation’:
A declaration's type gets only the variables it actually uses, not
every declared parameter.
Other than such pleasantries, Idris does not add anything of note. However, it does provide new constraints. As noted earlier, the current implementation of Idris attempts to erase implicits aggressively therefore providing speedup over Agda. In particular, Idris modules and records can be parameterised but not indexed —a limitation not in Agda.
Unlike Coq, Idris has been designed to “emphasise general purpose programming rather than theorem proving” \parencite{idris_faq, idris_tdd}. However, like Coq, Idris provides a Haskell-looking typeclasses mechanism; but unlike Coq, it allows named instances. In contrast to Agda's record-instances, typeclasses result in backtracking to resolve operator overloading thereby having a slower type checker.
Lean \parencite{lean_system_desc, lean_formalizing_math}: This is both a theorem prover and programming language; moreover it permits
quotient types and so the usually-desired notion of extensional equality.
It is primarily tactics-based, also permitting a calc
-ulational proof format
not too dissimilar with the standard equational proof format utilised in Agda.
Lean is based on a version of the Calculus of Inductive Constructions, like Coq. Lean is heavily aimed at metaprogramming for formal verification, thereby bridging the gap between interactive and automated theorem proving. Unfortunately, inspecting the language shows that its rapid development is not backwards-compatible —Lean 2 standard libraries have yet to be ported to Lean 3—, and unlike, for example, Coq and Isabelle which are backed by other complete languages, Lean is backed by Lean, which is unfortunately too young to program various tactics, for example.
The lean prover tutorial is not even complete!
It does not seem to be well docmented; only 1 file in the docs! It's been difficult finding anything superficially; I may need to install and try things out?
ATS, Applied Type System: This language combines programming and proving, but is aimed at unifying programming with formal specification. With the focus being more on programming than on proving. \parencite{ats_website, ats_combining}
ATS is intended as an approach to practical programming with theorem proving. Its module system is largely influenced by that of Modula-3, providing what would today be considered the bare bones of a module system. Advocating a programmer-centric approach to program verification that syntactically intertwines programming and theorem proving, ATS is a more mature relative of Idris —whereas Idris is Haskell-based, ATS is OCaml-based.
F*: This language supports dependent types, refinement types, and a weakest precondition calculus \parencite{fstar_website}. However it is primarily aimed at program verification rather than general proof. Even though this language is roughly 8 years in the making, it is not mature —one encounters great difficult in doing anything past the initial language tutorial.
F*'s module system is rather uninteresting, predominately acting as namespace management. It has very little to offer in comparison to Agda; e.g., within the last two years, it obtained a typeclass mechanism —regardless, typeclasses can be implemented as dependent records.
Beluga: The distinctive feature and sole reason that we mention this language
is its direct support for first-class contexts \parencite{beluga}.
A term t(x)
may have free
variables and so whether it is well-formed or what its type could be depend on the
types of its free variables, necessitating one to either declare them before hand
or to write, in Beluga, \newline [ x : T |- t(x) ]
for example.
As we have mentioned, and will
reiterate a few times, contexts are behaviourally indistinguishable from
dependent sums.
A displeasure of Beluga is that, while embracing the Curry-Howard Correspondence,
it insists on two syntactic categories: Data and computation.
This is similar to Coq's distinction of Prop
and Type
.
Another issue is that to a large degree the terms one uses in their type
declarations are closed and so have an empty context therefore one sees
expressions of the form [ |- t ]
since t
is a closed term needing only the empty
context. At a first glance, this is only a minor aesthetic concern; yet after
inspection of the language's webpage, tutorials, and publication matter, it is
concerning that nearly all code makes use of empty contexts —which are easily
spotted visually. The tremendous amount of empty contexts suggests that the language
is not actually making substantial use of the concept, or it is yet unclear what
pragmatic utility is provided by contexts, and, in either way,
they might as well be relegated to a less intrusive notation.
Finally, the language lacks any substantial standard libraries
thereby rendering it more as a proof of concept rather than a serious system
for considerable work.
Mizar: Unlike the rest, it is based on (untyped) Tarski–Grothendieck set theory which in some-sense has a ‘hierarchy of sets’. Being based on set theory, it is non-constructive. It has a large library of formalised mathematics; like Coq. \parencite{mizar_website, mizar_overview, mizar_library}.
Like Idris, it provide a ‘reservation’ mechanism to name parameters for a block
of code. Mizar environ
-ments are generally difficult to work with due to
multiple namespaces for articles and vocabularies.
There is otherwise nothing interesting to say regarding its module system.
Notable Mentions: The following are not actively being developed, as far we can tell from their websites or source repositories, but are interesting or have made useful contributions. In contrast to Beluga, Isabelle is a full-featured language and logical framework that also provides support for named contexts in the form of ‘locales’ \parencite{locales, isabelle_locales}; unfortunately it is not a dependently-typed language –though DTLs can be implemented in it. Mizar, unlike the above, is based on (untyped) Tarski–Grothendieck set theory which in some-sense has a hierarchy of sets. Like Coq, it has a large library of formalised mathematics \parencite{mizar_website, mizar_overview, mizar_library}. Developed in the early 1980s, Nuprl \parencite{prl_site} is constructive with a refinement-style logic; besides being a mature language, it has been used to provide proofs of problems related to Girard's Paradox \parencite{girard_paradox}. PVS, Prototype Verification System \parencite{pvs_prover}, differs from other DTLs in its support for subset types; however, the language seems to be unmaintained as of 2014. Twelf \parencite{twelf_site} is a logic programming language implementing Edinburgh's Logical Framework \parencite{lf_meta_mechanisation, lf_has_isabelle, lf_fast_proof_checking} and has been used to prove safety properties of ‘real languages’ such as SML. A notable practical module system \parencite{lf_practical_modules} for Twelf has been implemented using signatures and signature morphisms. Matita \parencite{matita_main, matita_site} is a Coq-like system that is much lighter \parencite{matita_is_coq_light}; it is been used for the verification of a complexity-preserving C compiler.
Dependent types are mostly visible within the functional community, however this is a matter of taste and culture as they can also be found in imperative settings, \parencite{dtl_imperative}, albeit less prominently.
2.4 Facets of Structuring Mechanisms: An Agda Rendition
open import Relation.Binary.PropositionalEquality open ≡-Reasoning -- Z-notation for sums open import Level open import Data.Product using (Σ ; proj₁ ; proj₂ ; _×_ ; _,_) Σ∶• : {a b : Level} (A : Set a) (B : A → Set b) → Set (a ⊔ b) Σ∶• = Σ infix -666 Σ∶• syntax Σ∶• A (λ x → B) = Σ x ∶ A • B open import Data.Nat open import Data.Nat.Properties
In this section we provide a demonstration that with dependent-types we can show records, direct dependent types, and contexts —which in Agda may be thought of as parameters to a module— are interdefinable. Consequently, we observe that the structuring mechanisms provided by the current implementation of Agda –and other DTLs– have no real differences aside from those imposed by the language and how they are generally utilised. More importantly, this demonstration indicates our proposed direction of identifying notions of packages is on the right track.
Our example will be implementing a monoidal interface in each format,
then presenting views between each format and that of the record
format.
Furthermore, we shall also construe each as a typeclass,
thereby demonstrating that typeclasses are, essentially, not only a
selected record but also a selected value of a dependent type
—incidentally this follows from the previous claim that records
and direct dependent types are essentially the same.
Recall that the signature of a monoid consists of
a type Carrier
with a method _⨾_
that composes values
and an Id
-entity value.
With Agda's lack of type-proof discrimination, i.e., its support for the
Curry-Howard Correspondence, the “propositions as types” interpretation, we can encode the signature as well as the
axioms of monoids to yield their theory presentation in the following two ways.
Additionally, we have the derived result:
Id
-entity can be popped-in and out as desired.
The following code blocks contain essentially the same content, but
presented using different notions of packaging. Even though both
use the record
keyword, the latter is treated as a typeclass
since the carrier of the monoid is given ‘statically’ and instance
search is used to invoke such instances.
record Monoid-Record : Set₁ where infixl 5 _⨾_ field -- Interface Carrier : Set Id : Carrier _⨾_ : Carrier → Carrier → Carrier -- Constraints lid : ∀{x} → (Id ⨾ x) ≡ x rid : ∀{x} → (x ⨾ Id) ≡ x assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z) -- derived result pop-Idᵣ : ∀ x y → x ⨾ Id ⨾ y ≡ x ⨾ y pop-Idᵣ x y = cong (_⨾ y) rid open Monoid-Record {{...}} using (pop-Idᵣ)
record HasMonoid (Carrier : Set) : Set₁ where infixl 5 _⨾_ field Id : Carrier _⨾_ : Carrier → Carrier → Carrier lid : ∀{x} → (Id ⨾ x) ≡ x rid : ∀{x} → (x ⨾ Id) ≡ x assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z) pop-Id-tc : ∀ x y → x ⨾ Id ⨾ y ≡ x ⨾ y pop-Id-tc x y = cong (_⨾ y) rid open HasMonoid {{...}} using (pop-Id-tc)
The double curly-braces {{...}}
serve to indicate that
the given argument is to be found by instance resolution:
The results for Monoid-Record
and HasMonoid
can be invoked without having to mention a monoid on
a particular carrier, provided there exists one unique record value
having it as carrier —otherwise one must use named instances \parencite{named_instances}.
Notice that the carrier argument in the typeclasses approach, “structure on a carrier”, is
an (undeclared) implicit argument to the pop-Id-tc
operation.
Alternatively, in a DTL we may encode the monoidal interface using dependent products
directly rather than use the syntactic sugar of records.
The notation Σ x ∶ A • B x
denotes the type of pairs (x , pf)
where x ∶ A
and pf ∶ B x
—i.e., a record consisting of two fields.
It may be thought of as a constructive analogue to the classical set comprehension \newline { x ∶ A❙B x}
.
-- Type alias Monoid-Σ : Set₁ Monoid-Σ = Σ Carrier ∶ Set • Σ Id ∶ Carrier • Σ _⨾_ ∶ (Carrier → Carrier → Carrier) • Σ lid ∶ (∀{x} → Id ⨾ x ≡ x) • Σ rid ∶ (∀{x} → x ⨾ Id ≡ x) • (∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) pop-Id-Σ : ∀{{M : Monoid-Σ}} (let Id = proj₁ (proj₂ M)) (let _⨾_ = proj₁ (proj₂ (proj₂ M))) → ∀ (x y : proj₁ M) → (x ⨾ Id) ⨾ y ≡ x ⨾ y pop-Id-Σ {{M}} x y = cong (_⨾ y) (rid {x}) where _⨾_ = proj₁ (proj₂ (proj₂ M)) rid = proj₁ (proj₂ (proj₂ (proj₂ (proj₂ M))))
Of the renditions thus far, the Σ
rendering makes it clear that a monoid could have
any subpart as a record with the rest being dependent upon said record.
For example, if we had a semigroup type, we could have declared \newline
Monoid-Σ = Σ S ∶ Semigroup • Σ Id ∶ Semigroup.Carrier S
.
There are a large number of such hyper-graphs, we have only presented a stratified view
for brevity. In particular, Monoid-Σ
is the extreme unbundled version, whereas
Monoid-Record
is the other extreme, and there is a large spectrum in between –all of which are
somehow isomorphic; e.g., Monoid-Record ≅ Σ C ∶ Set • HasMonoid C
.
Our envisioned system would be able to derive any such view at will \parencite{casl_overview}
and so programs may be written according to one view, but easily repurposed for other
view with little human intervention.
Like a Java class
, within the record
we may include derived results
that are then available to all values, `instances', of the record type.
Outside the record
, further properties may be added, though they now
require an actual value, instance, to be given.
Instances and their use are as follows.
One may realise that pop-0
proofs as a form of polymorphism
—we will return to package former polymorphism when discussing preliminary research.
instance ℕ-record = record { Carrier = ℕ ; Id = 0 ; _⨾_ = _+_ ; lid = +-identityˡ _ ; rid = +-identityʳ _ ; assoc = +-assoc } ℕ-tc : HasMonoid ℕ ℕ-tc = record { Id = 0; _⨾_ = _+_ ; lid = +-identityˡ _ ; rid = +-identityʳ _ ; assoc = +-assoc } ℕ-Σ : Monoid-Σ ℕ-Σ = ℕ , 0 , _+_ , +-identityˡ _ , +-identityʳ _ , +-assoc
ℕ-pop-0ᵣ : ∀ (x y : ℕ) → x + 0 + y ≡ x + y ℕ-pop-0ᵣ = pop-Idᵣ ℕ-pop-0-tc : ∀ (x y : ℕ) → x + 0 + y ≡ x + y ℕ-pop-0-tc = pop-Id-tc ℕ-pop-0ₜ : ∀ (x y : ℕ) → x + 0 + y ≡ x + y ℕ-pop-0ₜ = pop-Id-Σ
Interestingly, notice that the grouping in ℕ-Σ
is just an unlabelled (dependent) product,
and so when it is used in pop-Id-Σ
we project to the desired components.
Whereas in the Monoid-Record
case we could have projected the carrier by
Carrier M
, now we would write proj₁ M
.
This is nearly identical to the previous implementation and possibly
simpler due to the lack of the record { ⋯ }
clutter required of labelled products.
However, said clutter could have been removed by providing
a constructor
declaration in the definition of Monoid-Record
but we have decided not to do so, to make the labelling clear
and distinct from the unlabelled product presentations.
Observe the lack of informational difference between the presentations, yet there is a Utility Difference: Records give us the power to name our projections directly with possibly meaningful names. Of course this could be achieved indirectly by declaring extra functions; e.g.,
Carrierₜ : Monoid-Σ → Set Carrierₜ = proj₁
We will refrain from creating such boiler plate —that is, records allow us to omit such mechanical boilerplate.
Finally, let us exhibit views between this form and the record
form.
-- Following proves: Monoid-Record ≅ Σ Set HasMonoid. to-record-from-usual-type : Monoid-Σ → Monoid-Record to-record-from-usual-type (c , id , op , lid , rid , assoc) = record { Carrier = c ; Id = id ; _⨾_ = op ; lid = lid ; rid = rid ; assoc = assoc } -- Term construed by ‘Agsy’, -- Agda's mechanical proof search. from-record-to-usual-type : Monoid-Record → Monoid-Σ from-record-to-usual-type M = let open Monoid-Record M in Carrier , Id , _⨾_ , lid , rid , assoc {- Essentially moved from record{⋯} to product listing -}
Furthermore, by definition chasing, refl
-exivity, these operations are seen to be inverse of
each other. Hence we have two faithful non-lossy protocols for reshaping our grouped data.
In our final presentation, we construe the grouping of the monoidal interface
as a sequence of “variable : type” declarations —i.e., a ‘context’ or ‘telescope’.
Since these are not top level items by themselves, in Agda, we take a purely syntactic route
by positioning them in a module
declaration as follows.
module Monoid-Telescope-User (Carrier : Set) (Id : Carrier) (_⨾_ : Carrier → Carrier → Carrier) (lid : ∀{x} → Id ⨾ x ≡ x) (rid : ∀{x} → x ⨾ Id ≡ x) (assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) where pop-Idₘ : ∀(x y : Carrier) → (x ⨾ Id) ⨾ y ≡ x ⨾ y pop-Idₘ x y = cong (_⨾ y) (rid {x})
Notice that this is nothing more than the named fields of Monoid-Record
squished into six lines. Additionally, if we insert a Σ before each name
we essentially regain the Monoid-Σ
formulation.
It seems contexts, at least superficially, are a nice middle ground between
the previous two formulations.
As promised earlier, we can regard the above telescope as a record:
record-from-telescope : Monoid-Record record-from-telescope = record { Carrier = Carrier ; Id = Id ; _⨾_ = _⨾_ ; lid = lid ; rid = rid ; assoc = assoc }
The structuring mechanism module
is not a first class citizen in Agda.
As such, to obtain the converse view, we work in a parameterised module.
module record-to-telescope (M : Monoid-Record) where open Monoid-Record M -- Treat record type as if it were a parameterised module type, -- instantiated with M. open Monoid-Telescope-User Carrier Id _⨾_ lid rid assoc
Notice that we just listed the components out —rather reminiscent of the formulation
Monoid-Σ
. This observation only increases confidence in our thesis that there is no
real distinctions of packaging mechanisms in DTLs.
Undeniably instantiating the telescope approach to monoids for the natural number is nothing more than listing the required components.
open Monoid-Telescope-User ℕ 0 _+_ (+-identityˡ _) (+-identityʳ _) +-assoc
C.f., the definition of ℕ-Σ
: This is nearly the same instantiation with the primary
syntactical difference being that this form had its arguments separated by spaces rather than commas!
ℕ-popₘ : ∀(x y : ℕ) → x + 0 + y ≡ x + y ℕ-popₘ = pop-Idₘ
Notice how this presentation makes it explicitly clear why we cannot have multiple instances: There would be name clashes. Even if the data we used had distinct names, the derived result may utilise data having the same name thereby admitting name clashes elsewhere. —This could be avoided in Agda by qualifying names and/or renaming.
It is interesting to note that this presentation is akin to that of class
-es in C#/Java languages:
The interface is declared in one place, monolithic-ly, as well as all
derived operations there; if we want additional operations, we create
another module that takes that given module as an argument in the
same way we create a class that inherits from that given class.
Demonstrating the interdefinablity of different notions of packaging cements our thesis that it is essentially utility that distinguishes packages more than anything else. In particular, explicit distinctions have lead to a duplication of work where the same structure is formalised using different notions of packaging. In chapter 3 we will show how to avoid duplication by coding against a particular ‘package former’ rather than a particular variation thereof –this is akin to a type former.
2.5 Theory Presentations: A Structuring Mechanism
What of the most closely related theoretical work?
Our envisioned effort would support a “write one, obtain many” approach to package formation. We now turn to mentioning how package formers are currently treated formally under the name of ‘theory presentations’. It is the aim of this section to attest that the introduction's story is not completely on shaky foundations, thereby asserting that the aforementioned goals of the introduction are not unachievable —and the problems that will be posed in chapter 3 are not trivial.
As discussed, languages are usually designed with a bit more thought given to a first-class citizen notion of grouping than is given to second-class notions of packaging up defined content. Object-oriented languages, for example, comprise features of both views by treating classes as external structuring mechanisms even though they are normal types of the type system. This internalising of external grouping features has not received much attention with the notable mentions being \parencite{theories_as_types, focalize}. It is unclear whether there is any real distinction between these `internal, integrated' and `external, stratified' forms of grouping, besides intended use. The two approaches have different advantages. Both approaches permit separation of concerns: The external point of view provides a high-level structuring of a development, the internal point of view provides essentially another type which can be the subject of the language's operations —e.g., quantification or tactics— thereby being more amicable to computing transformations. Essentially it comes down to whether we want a `module parameter' or a `record field' —why not write it the way you like and get the other form for free.
Since external grouping mechanisms tend to allow for intra-language features —e.g., imports, definitions, notation, extra-logical declarations such as pragmas— their systematic internalisation necessitates expressive record types. As such, a labelled product type or context —being a list of name-type declarations with optional definitions— is a sufficiently generic rendition of what it means to group matter together.
Below is a grammar, from \parencite{theories_as_types}, for a simple yet powerful
module system based on theory (presentations) and theory morphisms –which are merely named contexts and named substitutions between contexts, respectively.
Both may be formed modularly by using includes to copy over declarations of previously named objects.
Unlike theories which may include arbitrary declarations, theory morphisms \texttt{(V : P → Q) := δ}
are well-defined if for every P
-declaration x ∶ T
, δ
contains a declaration x = t
where t
may refer to all names declared in Q
.
Observe that a context is, up to syntactical differences,
essentially JavaScript object notation literal.
Consequently, the notion of a mixin as described for JSON literals is here
rendered as a theory morphism.
-- Contexts Γ ::= · -- empty context | x : τ [:= τ′], Γ -- context with declaration, optional definition | includes X, Γ -- theory inclusion -- Terms τ ::= x | τ₁ τ₂ | λ x : τ′ • τ -- variables, application, lambdas | Π x : τ′ • τ -- dependent product | [Γ] | ⟨Γ⟩ | τ.x -- record “[type]” and “⟨element⟩” formers, projections | Mod X -- contravariant “theory to record” internalisation -- Theory, external grouping, level Θ ::= . -- empty theory | X := Γ, Θ -- a theory can contain named contexts | (X : (X₁ → X₂)) := Γ -- a theory can be a first-class theory morphism -- Proviso: In record formers, Γ must be flat; i.e., does not contain includes. -- Example theory hierarchy of signatures, abbrevating “(Π x : A • B) = (A → B)”. , MagmaSig := Carrier : Set, _⨾_ : Carrier → Carrier → Carrier, . , MonSig := includes MagmaSig, Id : Carrier, . , .
This concept of packaging indeed captures much of what's expected of grouping mechanisms; e.g.,
- Grouping mechanism should group all kinds of things and indeed there is no constraint on what a theory presentation may contain.
Namespacing: Every module context can be construed as a record whose contents can then be accessed by record field projection.
Theories as Types \parencite{theories_as_types} presents the first formal approach that systematically internalises theories into record types. Their central idea is to introduce a new operator
Mod
–read “models of”— that turns a theory \(T\) into a type \(\Mod T\) which behaves like a record type.- Operations on grouping mechanisms \parencite{tpc}.
As mentioned earlier, a theory morphism, also known as a ‘view’,
is a map between contexts that implements the interface of the source
using utilities of the target; whence results about specific structures can be
constructed by transport along views \parencite{little_theories}:
A view \texttt{V : P → Q} gives rise to a term homomorphism 𝒱
from P
-terms to Q
-terms
that is type-preserving in that whenever \texttt{Θ, P ⊢ t : T} then \texttt{Θ, Q ⊢ 𝒱 t : 𝒱 T}.
Thus, views preserve judgements and, via the propositions-as-types representations,
also preserve truth.
For example, a view \(\Phi = (U, \beta) : \mathcal{S} \to \mathcal{T}\) is essentially a predicate \(U\), of the target theory, denoting a universe of discourse along with an arity-preserving mapping \(\beta\) of 𝒮-symbols, or declarations, to 𝒯-expressions. It is lifted to terms as follows — notice translated variable-binders are relativised to the new domain.
The Standard Interpretation Theorem \parencite{theory_interpretations_farmer} provides sufficient conditions for a translation to be an ‘interpretation’ which transports results between formalisations. It states: A translation is an interpretation provided 𝒮-axioms \(P\) are lifted to theorems \(\Phi(P)\), the universe of discourse is non-empty \((\exists x \bullet U\, x)\), and the interpretation of the universe contains the interpretations of the symbols; i.e., for each 𝒮-symbol \(f\) of arity \(n\), \newline \(\Phi(∀ x₁, …, xₙ • ∃ y \,•\, f\, x₁\, …\, x\,ₙ = \,y)\).
By virtue of being a validity preserving homomorphism, a standard interpretation syntactically and semantically embeds its source theory in its target theory. The most important consequence of interpretability is the Standard Relative Satisfiability \parencite{theory_interpretations_farmer} which says that a theory which is interpretable in a satisfiable theory is itself satisfiable; in programming terms this amount to: If \(X\) is an implementation of `interface' 𝒯 and 𝒮 is interpretable in 𝒯 then \(X\) can be transformed into an implementation of 𝒮. Interestingly such ‘subtyping’ can be derived in a mechanical fashion, but it can leave the subtype relation to be cyclic. However, it is unclear under which conditions translations automatically give rise to interpretations: Can the issue be relegated to syntactic manipulation only?
Theory interpretation has been studied for first-order predicate logic then extended to higher-order logic \cite{theory_interpretations_farmer}. The advent of dependent-types, in particular the blurring of operations and formulae \cite{wiki_curry_howard}, means that propositions of a language can be encoded into it as other sorts, dependent on existing sorts, thereby questioning what it means to have a validity-preserving morphism when the axioms can be encoded as operations? As far as we can tell, it seems very little work regarding theory interpretations has been conducted in dependently-typed settings \parencite{mlt_partial, higher_order_interpretations, institution_interpretations, dtl_interpretations}.
Notice that records play dual roles. They not only serve as an internal form of grouping mechanisms, but inspired by the previous Agda renditions, also serve the purpose of forming dependent sum types.
What about the presence of non-termination or inheritance —i.e., partial functions and subtypes? The subject is only beginning to be seriously explored in higher-order logic and type theory. \cite{theory_interpretations_farmer}. Views associating base types with subtypes get complicated since functions must now deal with restricted domains, consequently necessitating that all predicates on functions also be relativised.
3 Solution Requirements
From the outset we have proposed a particular approach to resolving the needless duplication present in current module systems that are utilised in non-dependently-typed languages. Up to this point, we have only discussed how our approach could mitigate certain troubles; such as a difference of perspectives of modules, or of equivalent operations acting on different perspectives of modules. We now turn to discussing, in the following subsections, what it is that is missing from existing module systems, what one actually wants to do with modules, and conclude with a checklist of features that our proposed system should meet in order to be considered usable and adequate as a thesis-level effort.
3.1 Missing Features
Certain mechanically-derivable concepts, such as different perspectives, are needlessly delegated to the user by pedestrian packaging systems. Besides being tedious and error-prone, the inexpressibility of derivates obscures the corresponding general principles underlying them, thus foregoing any machine assistance in ensuring any correctness or safety-ness guarantees. The desire to pursue a more economical yet powerful packaging system follows from our research team's expedited efforts that could have been mechanised . We will only mention two such use cases.
\noindent Expressivity:
\noindent
A common pattern that can be seen, for example, in the Agda standard library,
is of a predicate ensuring desirable properties
OF its inputs, then of a record containing the inputs as fields along
with a proof of said predicate. More concretely, suppose we have a binary predicate
named IsSemi
and the record is named Semi
; the predicate form allows us to
quantify over inputs as in ∀ x y → IsSemi x y → ⋯
, in contrast the latter
approach is intrinsic in nature: ∀ (s ∶ Semi) → ⋯
—contrast this with a mathematician naturally declaring “let s
be a semigroup”,
whereas almost never do mathematicians say “let x
be a set and y
be an operation on it that together constitute a semigroup”.
At a first glance, it does not seem too troublesome to produce the record presentation from the predicate presentation: Simply repeat all the inputs under a record declaration along with a proof obligation. However, the word ‘repeat’ already suggests a problem, and ‘all’ suggests another one. What if one desires to utilise the record associated to the predicate by only packaging certain inputs but not others? This is akin to the problem of constructors in object-oriented languages: In Java, for example, one uses overloading to provide a number of user-written constructors for only a few resonable input invocations to construct an object; in contrast, Common Lisp permits optional named arguments, and so in one fell swoop, with one user-written, constructor, provides all possible combinations of constructor invocations —we are aiming at this level of power and flexibility.
Lest it's unclear, let's elaborate slightly on the idea.
open import Relation.Binary.PropositionalEquality open ≡-Reasoning -- Z-notation for sums open import Level open import Data.Product using (Σ ; proj₁ ; proj₂ ; _×_ ; _,_) Σ∶• : {a b : Level} (A : Set a) (B : A → Set b) → Set (a ⊔ b) Σ∶• = Σ infix -666 Σ∶• syntax Σ∶• A (λ x → B) = Σ x ∶ A • B
A semigroup is an algebraic structure that models (untyped) compositionality:
It consists of a collection of objects of interests called the Carrier
set,
and an operation _⨾_
to compose existing items to produce new items, and the operation
is associative.
Below is a spectrum of ways to bundle up such a structure
–starting from being completely bundled up all the way to being
completely exposed.
-- One extreme: Completely bundled up record Semigroup0 : Set₁ where field Carrier : Set _⨾_ : Carrier → Carrier → Carrier assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
-- ‘Typeclass’ on a given Carrier -- Alternatively: Carrier is known as runtime. record Semigroup1 (Carrier : Set): Set₁ where field _⨾_ : Carrier → Carrier → Carrier assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
-- Two items known at run time --c.f., “IsSemi” above. record Semigroup2 (Carrier : Set) (_⨾_ : Carrier → Carrier → Carrier) : Set where field assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)
-- A value of “Semigroup3 C op pf” is trivially the empty record, if any, -- provided ‘pf’ is a proof that ‘C’ forms a semigroup with ‘op’. -- This type is usualy written “Σ C ∶ Set • Σ _⨾_ ∶ C → C → C • Σ assoc ∶ ⋯”. record Semigroup3 (Carrier : Set) (_⨾_ : Carrier → Carrier → Carrier) (assoc : ∀ x y z → (x ⨾ y) ⨾ z ≡ x ⨾ (y ⨾ z)) : Set where -- no fields
Depending on the user's needs, it may be useful to have one form or another. Unfortunately they are enslaved to the choices of the library designer, or if they deviate then they must produce tedious conversion methods and use them to pad all the library methods for the structures. Even worse, such back and forth conversions will not only be representation shuffling but also wasteful of resources.
For example, every bijective function \(f : A \to B\) furnishes its target \(B\) with a semigroup
structure provided its source \(A\) has the structure to begin with.
Since the statement mentions the carriers of semigroups, it is only natural
to formulate it an prove it using presentation Semigroup1
.
Surjection : ∀{A B : Set} → (A → B) → Set Surjection {A} {B} f = ∀ (b : B) → Σ a ∶ A • b ≡ f a -- (Σ a ∶ A • P a) ≈ { (a, proof) ❙ a ∈ A ∧ pf is a proof of P(a) } Injection : ∀{A B : Set} → (A → B) → Set Injection {A} {B} f = ∀ {x y} → f x ≡ f y → x ≡ y
translate1 : ∀{A B} → (f : A → B) → Surjection f → Injection f → Semigroup1 A → Semigroup1 B translate1 f surj inj AS = let open Semigroup1 AS -- x ⨾′ y is obtained by applying f to the ⨾-composition of the pre-images of x and y. infix 5 _⨾′_ _⨾′_ = λ x y → let a0 = proj₁ (surj x); a1 = proj₁ (surj y) in f (a0 ⨾ a1) -- f distributes over ⨾ turning it into ⨾′. factor : ∀ {a a′} → f a ⨾′ f a′ ≡ f (a ⨾ a′) factor {a} {a′} = let 𝒶 , m = surj (f a) 𝒶′ , w = surj (f a′) in begin f a ⨾′ f a′ ≡⟨ refl ⟩ f (𝒶 ⨾ 𝒶′) ≡⟨ cong f (cong₂ _⨾_ (inj (sym m)) (inj (sym w))) ⟩ f (a ⨾ a′) ∎ distribute : ∀ {a a′} → f (a ⨾ a′) ≡ f a ⨾′ f a′ distribute {a} {a′} = sym (factor {a} {a′}) in -- Bundle up ⨾′ along with a proof of associtivity record { _⨾_ = _⨾′_; assoc = λ x y z → let -- Obtain f-pre-images a₀ , x≈fa₀ = surj x a₁ , y≈fa₁ = surj y a₂ , z≈fa₂ = surj z in {- Tersely, we rewrite along the pre-images, factor f, perform the associativity of ⨾, then distribute f and rewrite along the pre-images. -} begin (x ⨾′ y) ⨾′ z ≡⟨ cong₂ _⨾′_ (cong₂ _⨾′_ x≈fa₀ y≈fa₁) z≈fa₂ ⟩ (f a₀ ⨾′ f a₁) ⨾′ f a₂ ≡⟨ cong (_⨾′ f a₂) factor ⟩ f (a₀ ⨾ a₁) ⨾′ f a₂ ≡⟨ factor ⟩ f ((a₀ ⨾ a₁) ⨾ a₂) ≡⟨ cong f (assoc _ _ _) ⟩ f (a₀ ⨾ (a₁ ⨾ a₂)) ≡⟨ distribute ⟩ f a₀ ⨾′ f (a₁ ⨾ a₂) ≡⟨ cong (f a₀ ⨾′_) distribute ⟩ f a₀ ⨾′ (f a₁ ⨾′ f a₂) ≡⟨ sym (cong₂ _⨾′_ x≈fa₀ (cong₂ _⨾′_ y≈fa₁ z≈fa₂)) ⟩ x ⨾′ (y ⨾′ z) ∎ }
translate1
is a lengthy proof, we could repeat it, or invoke it.
Since duplication with alteration is error-prone and non-generic,
we shall aim for the latter.
translate0 : ∀{B : Set} (AS : Semigroup0) (f : Semigroup0.Carrier AS → B) → Surjection f → Injection f → Semigroup0 translate0 {B} AS f surj inj = record { Carrier = B ; _⨾_ = _⨾_ ; assoc = assoc } where -- Repackage ‘AS’ from a ‘Semigroup0’ to a ‘Semigroup1’ -- only to immediatley unpack it, so that its contents -- are available to be repacked above as a ‘Semigroup0’. pack : Semigroup1 (Semigroup0.Carrier AS) pack = let open Semigroup0 AS in record {_⨾_ = _⨾_; assoc = assoc } open Semigroup1 (translate1 f surj inj pack)
Observe that translate0
repackages AS
via pack
,
then passes that as an argument to translate1
, which in turn unpacks it
to form a new Semigroup0
, which is then unpacked in the
last line above.
Regardless of any possible wasteful amount of packing and unpacking of records
–which may be mitigated via inlining–
the way translate0
is written is far from ideal;
whereas translate1
is the appropriate level of abstraction to pose the problem.
Instead, it would be ideal to write the method at a sufficient level of generality
such that translate0
and translate1
are, say, polymorphic instances thereof.
This is what we shall propose in a later section.
Moreover, as a stylistic decision, implementers may prefer to view an object in either its predicate form —with the constituents varying— or in its record form —with the constituents fixed—, will all library utilities tied to a particular form.
Efficiency:
A hallmark of computing is to reduce new problems to ones already considered.
One realisation of this principle is found in the sharing mechanisms of
certain lazy languages: In the expression let y = f(x) in g(y, y)
,
the term y
is evaluated once and the result is shared among its multiple
call sites. This idea comes under the name of thunks:
When we encounter an instance of y
and we need to ‘think’
of its value, we realise we have already ‘thunk’ it.
Memory is tremendously difficult to reason about , and lazy sharing only compounds to the troubles of garbage collection and complexity analysis .
Dependently-typed languages are usually not only utilised for programming but generally also for proof; as such, their implementations adhere to a particular logic.
To be completed …
Excerption:
In order to produce reusable components, theories —i.e., packages— are formed from existing theories by adding only one new concept at a time. Such an approach reduces the possibility of missing a useful structure in the hierarchy, as well as provides tremendous generality —operations can be rendered using the minimal interface required rather than one that is overly expressive. This is a common scheme when formalising mathematics \parencite{typeclasses_for_maths,coq_cat_experiences}.
Unfortunately, a common scenario is when one wants to instantiate such a deeply nested theory. More concretely, suppose we have the following fine-grained hierarchy.
skinparam defaultTextAlignment center [*] -> Empty Empty -> Type Type -down-> Pointed Type -> Magma Magma -> Semigroup Pointed -down-> Pointed_Semigroup Semigroup -down-> Pointed_Semigroup Pointed_Semigroup -down-> Left_Unital_Semigroup Pointed_Semigroup -down-> Right_Unital_Semigroup Left_Unital_Semigroup -down-> Monoid Right_Unital_Semigroup -down-> Monoid Type : Carrier Pointed : Carrier, point Magma : Carrier, binary_op Semigroup : Carrier, binary_op, associativity Pointed_Semigroup : Carrier, point, binary_op, associativity Left_Unital_Semigroup : ⟪inherit above⟫, left_identity_law Right_Unital_Semigroup : ⟪inherit above⟫, right_identity_law Monoid : Carrier, point, binary_op, associativity, identity_laws center footer Example Hierarchy
If we have the ingredients for a monoid in hand, we are unfortunately first
required to produce a left or right unital semigroup, which requires us to produce
a pointed semigroup first, and this regress continues to the base theory, Type
.
Building on semigroups, monoids are a ubiquitous model of compositionality,
and so this scenario
happens rather often, in one guise or another. The amount of syntactic noise
required to produce a simple instantiation is unreasonable: One should not be forced
to work through the hierarchy if it provides no immediate benefit.
It is to be noted that this issue does not generally apply to implementations of
object-oriented class supporting multiple interfaces.
Even worse, pragmatically speaking, to access a field deep down in a nested structure results in overtly lengthy and verbose names. Indeed, in the above example, the monoid operation lives at the bottom-most level, we would need to access all the intermediary levels to simply refer to it. Such verbose invocations would immediately give way to helper functions to refer to fields lower in the hierarchy; yet another opportunity for boilerplate to leak in.
It is interesting to note that diamond hierarchies cannot be trivially eliminated when providing fine-grained hierarchies. As such, we make no rash decisions regarding limiting them —and completely forgoe the unreasonable possibility of forbidding them.
A more common example from programming is that of providing monad instances
in Haskell. Most often users want to avoid tedious case analysis or prefer a
sequential-style approach to producing programs, so they want to furnish a
type constructor with a monad instance in order to utilise Haskell's do
-notation.
Unfortunately, this requires an applicative instances, which in turn requires
a functor instance. However, providing the return-and-bind interface for monads
allows us to obtain functor and applicative instances.
Consequently, many users simply provide local names for the return-and-bind
interface then use that to provide the default implementations for the other
interfaces. In this scenario, the standard approach is side-stepped by manually
carrying out a mechanical and tedious set of steps that not only wastes time
but obscures the generic process and could be error-prone.
Instead, it would be desirable to ‘flatten’ the hierarchy into a single package, consisting of the fields throughout the hierarchy, possibly with default implementations, yet still be able to view the resulting package at base levels in the hierarchy. Another benefit of this approach is that it allows users to utilise the package without consideration of how the hierarchy was formed, thereby providing library designers with the freedom to alter it in the future.
These features are considered ‘missing’ since they are reasonably achievable in a dependently-typed system —e.g., the different forms of dependently-typed bundling suggest a form of polymorphism. Their absence may be due to logistic reasons, such as no effort expedited in their direction, or due to issues surrounding the logical frameworks of the systems. Which is to blame is an investigation matter left to the thesis research.
3.2 Desirable Features
Our preliminary research, and personal use with dependently-typed systems, has yielded three strongly desirable features of a module system for DTLs.
Uniformity:
A type alias and a value alias are merely aliases at the end of the day, so unlike Haskell, for example, which distinguishes the two, Agda, for example, does not. More generally, type families, simple types, type constructors, dependent types, etc, collapse into a single category: Dependent types.
In particular, recall the canonical definition of ‘term’:
term ::= x -- variable | f(term_0, …, term_N) -- function application
In pedestrian languages, one distinguishes between value terms and type terms,
whence the t_i
are constrained to be homogeneously all values or all types.
In contrast, a dependently-typed languages makes no such limitation, thereby allowing
the t_i
to be heterogeneous. For example, in a simple type system, Maybe (A × List B)
is a term where all variables, \(t_0, t_1 = A, B\), are of the same kind —types.
This is not so with the term \newline Maybe (A × Vec B n)
---A
and B
are types while n
is a number.
Our aim is not to educate the reader on the power and utility of dependent types;
we invite the reader to consult any of the existing material \parencite{dtl_why, agda_overview}.
In the same vein, the varying notions of packaging are treated differently even though they are isomorphic in certain scenarios or interdefinable in others. As such, it would be useful to reduce the syntactic distinction between them.
Genericity:
Type polymorphism permits us to produce functions written once with type variables and have them applied to radically different types. Likewise, it would be desirable to write once a generic function on a kind of package and have it operate on the many variations of packaging.
An example of this idea is presented at the end of this section, as part of preliminary research. In particular, we demonstrate a novel form of generic programming, package polymorphism: A method is written against a generic notion of container and is then applied to derived notions —such as the \texttt{Semigroup}\(i\) forms from the previous section.
Extensiblity:
Systems tend to come with a pre-defined set of operations for built-in constructs; the user is left to utilise third-party pre-processing tools, for example, to provide extra-linguistic support for common repetitive scenarios they encounter.
More concretely, a large number of proofs can be discharged by merely pattern matching on variables —this works since the case analysis reduces the proof goal into a trivial reflexitivity obligation, for example. The number of cases can quickly grow thereby taking up space, which is unfortunate since the proof has very little to offer besides verifying the claim. In such cases, a pre-process, perhaps an “editor tactic”, could be utilised to produce the proof in an auxiliary file, and reference it in the current file.
Perhaps more common is the renaming of package contents, by hand.
For example, when a notion of preorder is defined with relation named _≤_
,
one may rename it and all references to it by, say, _⊑_
. Again, a pre-processor
or editor-tactic could be utilised, but many simply perform the re-write by hand
—which is tedious, error prone, and obscures the generic rewriting method.
It would be desirable to allow packages to be treated as first-class concepts that could be acted upon, in order to avoid third-party tools that obscure generic operations and leave them out of reach for the powerful typechecker of a dependently typed system.
These features are desirable for working with modules, yet raise a number of immediate concerns. For example, uniformity may lead to ambiguous parsing, genericity may lead to inefficient execution, and extensibility borders on meta-programming thereby leaving the realm of types altogether. Possible limitations on these features may result in the thesis efforts to implement them in a dependently-typed system, such as Agda.
3.3 One-Item Checklist for a Candidate Solution
An adequate module system for dependently-typed languages should make use of dependent-types as much as possible. As such, there is essentially one and only one primary goal for a module system to be considered reasonable for dependently-typed languages: Needless distinctions should be eliminated as much as possible.
The “write once, instantiate many” attitude is well-promoted in functional communities predominately for functions, but we will take this approach to modules as well, beyond the features of, e.g., *ML functors. With one package declaration, one should be able to mechanically derive data, record, typeclass, product, sum formulations, among many others. All operations on the generic package then should also apply to the particular package instantiations.
This one goal for a reasonable solution has a number of important and difficult subgoals. The resulting system should be well-defined with a coherent semantic underpinning —possibly being a conservative extension—; it should support the elementary uses of pedestrian module systems; the algorithms utilised need to be proven correct with a mechanical proof assistant, considerations for efficiency cannot be dismissed if the system is to be usable; the interface for modules should be as minimal as possible, and, finally, a large number of existing use-cases must be rendered tersely using the resulting system without jeopardising runtime performance in order to demonstrate its success.
During the research stage of the thesis, some of the sub-goals may be altered radically, dismissed altogether, or new ones brought forth due to implementation considerations. However, the one main goal will remain unchanged as it is how we have chosen to measure the minimal adequacy for a module system for rich settings that include dependent-types.
3.4 Preliminary Research
The homogeneous treatment of structuring mechanisms is herein presented using a prototype developed using the user-friendly Emacs application framework by means of textual expansion, the details of which are largely uninteresting —suffice it to say, the code is tremendously terse. In this section we demonstrates that packaging concepts differ only in their use, leading to a uniform syntax of which first-class records are an instance and so the resulting system is homoiconic in nature. We introduce fictitious syntax, mostly in red, with its intended Agda elaboration in blue —the users write the red and expect it to behave like the blue; no “code generation” transpires.
The reader is advised to remember that the value of a prototype is in the guidance it provides, not the implementation itself nor any of its design decisions —such as using strings in meta-programming scenarios. In other words, for the reader, portions of this section may serve as an exercise in foresight and patience. ( A brief demonstration of the prototype may be viewed at https://www.youtube.com/watch?v=NYOOF9xKBz8 .)
A prime guiding design decision is try to avoid making any decisions, including unconscious restrictions, unless deemed necessary!
The initiated reader will quickly notice that our package formers are just theory presentations —a list of name-type pairs. The chosen phrasing is due to the target audience, DTL programmers. We are not committed to the name, but unlike the overloaded ‘module’, ‘package former’ is a good new name without too many meanings. We have not provided full semantics for package formers, but we have provided concrete well-defined elaborations to communicate the intent: A package former is akin to a type former, it is ‘incomplete’ and does not define a concrete package until a certain tag is provided. It is part of the thesis effort to investigate which features of our proposed package formers break, or become limited, when considered with other language constructs.
The uniformity in syntax reduces the variety of sub-languages in a dependently-typed language by eliminating needless distinctions for notions of containers. The first subsection below addresses syntactic similarity, whereas the second tackles computing similarity, and we conclude with a brief discussion on foundational concerns.
3.4.1 First Observation: Syntactic Similarity for Containers
Since the prototypical notion of packaging is that of records,
which are value terms, all, necessarily succeeding, notions of packaging
ought to be treated uniformly as value types.
Consequently, variations on packaging should only be signalled by necessary
keywords, and otherwise should be syntactically indistinguishable.
That is to say, a ‘variation’ is a tag identifying what particular
form of module is desired, such as datatype
for an algebraic data type
with the declared fields as constructors, or as record
to yield a record structure
with constituents being the declared fields.
For example, just as List
is a type-former, we may declare a ‘package former’:
PackageFormer TermP (v : Variation) : Set where Var : Int → TermP v Add : TermP v → TermP v → TermP v
Note that a package former is just a sequence of names with types and,
as will be demonstrated later, optional default types.
It requires a particular “interpretation” —possibly user-defined—,
to produce some notion of package. This is signalled by the Variation
type, which for brevity contains data, record, typeclass
, and a few more
that we will meet below.
For example, the data
variation of packaging gives us a
free data type.
TermData = TermP data {- ≅ data TermData : Set where Var : Int → TermData Add : TermData → TermData → TermData -}
In the comment above, we indicate how our fictitious syntax is intended to be elaborated into current Agda syntax. Besides syntax, induction principles are also derived: Our envisioned system would be able to derive simple, tedious, uninteresting concepts; leaving difficult, interesting, ones for humans to solve. For this type, below is the dependently typed eliminator, which in a DTL, corresponds to an induction principle.
{- term-data-elim : ∀ {ℓ} {R : TermData → Set ℓ} → (base : (n : Int) → R (Var n)) → (ind : ∀ {s t} → R s → R t → R (Add s t)) → (t : TermData) → R t term-data-elim base ind (Var n) = base n term-data-elim base ind (Add s t) = ind rs rt where rs = term-data-elim base ind s rt = term-data-elim base ind t -}
The type of the package former, for now, could simply be Set
—c.f., the commented-out elaboration which declares TermData ∶ Set
.
However, if we permit a sufficiently small subtyping system, we
may find it desirable to have the type of a package former be itself
a package former! Moreover, if package former t
has type package former t′
,
then the user should be able to use t
at the levels t ∶ s
without too much overhead, where s
is any subtype of t
with Set
being a minimal
such subtype. These thoughts are hurried and it is the purpose of the thesis
to investigate what is the appropriate route.
It is often the case that one begins working with a record
of useful semantic
data, but then, say, for proof automation, may want to use the associated datatype
for syntax. The latter should be mechanically derivable, and this is what we aim
provide with our package formers.
We will not delve into the relationship between free data types and how, for example,
their associated catamorphism is necessarily also an interpreter
—in the programming languages sense.
The reader is invited to consult a reference \parencite{cats_logic_shulman}.
We shall not discuss polymorphism along variations, the v
components above,
as it is orthogonal to our immediate goals. For example, TermP
could have a field typed
\newline \texttt{TermP (f v) → TermP (g v) → TermP v},
where f
and g
are operations on variations.
Nonetheless, this is a feature that one should be aware of.
The remaining items instantiate package formers for the usual common uses. Including notions of records in item 1; an algorithmic sketch underlying the examples of item 1 is presented in item2; union types and external, second-class, modules in item 3; package former polymorphism in item 4; operating on package formers and inheritance in items 5 and 6; then discuss how package formers handle the diamond problem in item 7. Finally, we close in item 8 by discussing a problem not generally found in pedestrian languages and how it is solved using package formers.
- The Generality of Package Formers —Products
To demonstrate the generality of the notion of package formers we shall demonstrate how other common forms could be ‘derived’ from the single declaration above. It is to be noted that for such a small example, such derived code may be taken for granted, however for much larger theories —for example, a “field” comes with more than 20 fields— the ability to derive different perspectives in a consistent fashion is indispensable; especially when the package is refactored. More realistically, a symmetric rig groupoid uses about 212 coherence laws \parencite{rig_computation}, for which case-splitting, to perform proofs, yields over 200 goals thereby making metaprogramming a tempting approach.
field ≅ ablean group ⟶ Carrier, op, inv, unit, assoc, 2 unit-laws, 2 inverse-laws, comm-law ⟶ 10 laws multiplicative monoid ⟶ Carrier, op, unit, assoc, 2 unit-laws ⟶ 6 laws the above two carries are identical ⟶ 1 law distributively laws ⟶ 2 laws integrity & div-op & non-zero division ⟶ 3 laws
Total ⟶ 22 laws
-- An instance of TermRecord should have a carrier type -- containing the integers, ‘Var’, and supports some binary operation, ‘Add’. TermRecord = TermP record {- ≅ record TermRecord : Set where field Carrier : Set Var : Int → Carrier Add : Carrier → Carrier → Carrier -}
In the previous and following invocations, the name
Carrier
is a system internal, for now, and can easily berenamed
—as will be demonstrated later on. For now, we adhere to a single-sorted stance: Unless indicated otherwise, aCarrier
will always be included. An example of a two-sorted algebraic structure, graphs, is demonstrated at the end of this subsection.Built-in names, such as
Carrier
, are generally not ideal. For example, a machine may provide the namesFourLeggedFeline
andCommutativeIdempotentMonoid
where a human may preferCat
andJoinSemilattice
instead. As such, the resulting system, would accept ‘renaming’ functions to generate names. For now, we mostly limit such an approach for brevity.TermOn = TermP typeclass {- ≅ record TermOn (Carrier : Set) : Set where field Var : Int → Carrier Add : Carrier → Carrier → Carrier -}
TermFunctionsOn = TermP tuples {- TermFunctionsOn : Set → Set TermFunctionsOn C = (Int → C) × (C → C → C) -}
TermFunctions = TermP Σ -- ≅ TermFunctions = Σ C ∶ Set • Σ Var : Int → C • (C → C → C)
Let's show a more intricate yet desirable use.
PointedSemigroup = TermP record hiding (Var) renaming (Add to _⨾_) field Id : Carrier ⨾-assoc : ∀ x y z → x ⨾ (y ⨾ z) ≡ (x ⨾ y) ⨾ z {- ≅ record PointedSemigroup : Set₁ where field Carrier : Set _⨾_ : Carrier → Carrier → Carrier Id : Carrier ⨾-assoc : ∀ x y z → x ⨾ (y ⨾ z) ≡ (x ⨾ y) ⨾ z -}
- Algorithmically Obtaining Elaborated Types
We have discussed how the generic package formers elaborate —each blue comment indicates a standalone isomorphic Agda rendition—, as such it should be unsurprising that the constituents of a package former are dependently typed functions consuming each concrete variation in its traditional fashion. Let's clarify this idea further.
PackageFormer TermP (v : Variation) : Set where Var : Int → TermP v Add : TermP v → TermP v → TermP v
The ‘type’ of the first item, for example, is as follows —where
TermP v
is rewritten using the above introduced names for the sake of clarity.Var : (v : Variation) → Set {- Datatype constructor -} Var datatype = Int → TermData {- Dependent projection -} Var record = (τ : TermRecord) → Int → TermRecord.Carrier τ Var Σ = (τ : TermFunctions) → Int → proj₁ τ {- Parameter of a constraint -} Var typeclass = ∀{C} {{_ : TermOn C}} → Int → C Var tuples = ∀{C} → TermFunctionsOn C → Int → C ⋯
An initial glance suggests that this is all ad-hoc; let us demonstrate that this is not the case. Suppose there were a method
𝒯
to obtain the user-provided types of constituents; e.g., the givenVar ∶ Int → TermP v
is indistinguishable from \newlineVar ∶ 𝒯 “Var” (TermP v)
.Constituent = String -- Draft idea, not ideal. -- “A ⟨n⟩→ B ≈ A → ⋯ → A → B” with n-many A's. _⟨_⟩→_ : Set → ℕ → Set → Set A ⟨ zero ⟩→ B = B A ⟨ succ n ⟩→ B = A → (A ⟨ n ⟩→ B) -- Constituents of package formers give rise to “Set ⟨n⟩→ Set” functions. 𝒯 : {P : PackageFormer} → Constituent P → Set ⟨ arity P ⟩→ Set 𝒯 “Var” X = Int → X 𝒯 “Add” X = X → X → X
It is now trivial to reify the above prescription for
Var
in a uniformly fashion —namely,Var = 𝓉𝓎𝓅𝒆 “Var”
.𝓉𝓎𝓅𝒆 : Constituent → Variation → Set 𝓉𝓎𝓅𝒆 c v@datatype = 𝒯 c (TermP v) 𝓉𝓎𝓅𝒆 c v@record = (τ : TermP v) → 𝒯 c ((TermP v).Carrier τ) 𝓉𝓎𝓅𝒆 c v@Σ = (τ : TermP v) → 𝒯 c (proj₁ τ) 𝓉𝓎𝓅𝒆 c v@typeclass = ∀{C} {{_ : TermP v C}} → 𝒯 c C 𝓉𝓎𝓅𝒆 c v@tuples = ∀{C} → TermP v C → 𝒯 c C ⋯
For example, invoking this approach we find that
Add
, onTermRecord
's, is typed \newline𝓉𝓎𝓅𝒆 “Add” record
, which may be rewritten as \newline(τ ∶ TermRecord) → TermRecord.Carrier τ → TermRecord.Carrier τ → TermRecord.Carrier τ
. That is, as expected,Add
on records consumes a record value then acts as a binary operation on the carrier of said record value. Likewise, we invite the reader to check thatAdd
on algebraic datatypeTermData
is typed as a binary constructor.Users have access to the elaborated types.
TermP.Var : ∀{v} → 𝓉𝓎𝓅𝒆 “Var” v TermP.Add : ∀{v} → 𝓉𝓎𝓅𝒆 “Add” v
This is particularly useful when one wants to extract such types for re-use elsewhere.
ListBop = TermP.Add datatype ∘ List {- ≅ ListBop : Set → Set ListBop C = (List C → List C → List C) -} ConstrainedBop : (Set → Set) → Set ConstrainedBop constraint = TermP.Add typeclass using constraint {- ≅ ConstrainedBop constraint = ∀{C} → constraint C → C → C → C -- N.B., this would not elaborate without the “using”. -- Semantically, “P.x y using z = (P.x y)[P v ≔ z]” -- ─the “v” appears from “∀{v}” above. -} SetoidBop = TermP.Add record using Setoid {- ≅ SetoidBop : Setoid ℓ₀ ℓ₀ → Set SetoidBop S = Setoid.Carrier C → Setoid.Carrier C → Setoid.Carrier C -- N.B., this would not elaborate if “Sectoid.Carrier” were undefiend. -}
These examples open a flurry of problems.
At this stage, it is sufficient to have observed what could possibly be performed and that it is not without burden. We will not attempt to clarify any problem nor propose any solution; the thesis effort will contend with these matters further.
- The Generality of Package Formers —Sums & Modules
Thus far we have only discussed products; however the proposed general notion of containers should also produce sum types and be used in modules —which are just packages.
TermFunctionsSumOn = TermP sum -- ≅ TermFunctionsSumOn C = (Int → C) ⊎ (C → C → C)
In general, this yields a disjoint collection of declarations where each declaration is itself a Σ consisting of the context necessary to ensure that the operations are well-defined.
For modules,
PackageFormer MyDriver (t : TermP record renaming (Carrier to C)) : Set where ⋯ -- ≅ module MyDriver (t : TermRecord[Carrier ≔ C]) where ⋯ -- ≅ module MyDriver (C : Set) (Var : Int → C) (Add : C → C → C) where ⋯
At least two ‘free’ invocation notations ought to be supplied:
MyDriver t
MyDriver type varOp addOp
Multifaceted invocations provide a common use case: No overhead to pack or unpack the constituents of a type former so the sole purpose of an invocation. However, the pragmatic feasibility of such an approach is unclear at this stage.
- Novel Genericity: ‘Package Polymorphism’
We have a sufficient number of elaborations thus far to demonstrate that the notion of package formers is not without merit. It is now an appropriate moment to address an elephant in the room: The phrase
TermP v
semantically refers to which type?If
v = datatype
thenTermP v
refers to the associated algebraic datatype. Ifv = record
, then there are at least two ways to interpretTermP v
: As either the record type or as the carrier of a record value. Likewise for other variations. For now, we settle with a monadic-like interpretation: We writedo τ ← TermP v; ⋯
whenever we wish to refer to the underlying carrier of a concrete package former. Loosely put,do τ ← TermP v; b ≈ v ╱ (λ τ → b) v@datatype ╱ f = f (TermP v) v@record ╱ f = ∀(τ : TermP v) → f ((TermP v).Carrier τ) v@Σ ╱ f = ∀(τ : TermP v) → f (proj₁ τ) v@typeclass ╱ f = ∀{τ} {{_ : TermP v τ}} → f τ v@tuples ╱ f = ∀{τ} → TermP v τ → f τ
The ‘over’ notation,
_╱_
, assumesf
is a function acting on types; however, this is not necessary, if the∀
were replaced withλ
, then the result would be a term expression. This is yet another opportunity for investigation during the thesis effort. Moreover, there is the possibility of providing “implicit counterparts” to these variations,; e.g., fortuples
one may want∀{τ} {_ ∶ TermP v τ} → f τ
instead, which could be variation, say,tuples-imp
. Likewise, we may want notationdo-Σ
to replace \newline∀ ⋯ → ⋯
withΣ ⋯ • ⋯
.Unsurprisingly, this approach subsumes our earlier typing elaboration: \newline
𝓉𝓎𝓅𝒆 c v = do τ ← TermP v; 𝒯 c τ
. More concretely, for example, a notion of ‘depth’ for terms may have type∀ {v} → do τ ← TermP v; (τ → ℕ)
—a function that takes a package and yields a number. In the case ofv = record
, such a function actually takes two items: The first being a record value, the second being an element of the carrier of that record value. In the case ofv = typeclass
, the function takes an argument found by instance search. Likewise, for the remaining variations.Let us now turn to an example of a function operating on the above many, and all, variations of such packages. This example may appear contrived, yet the power of this form of polymorphism appears at the end of this subsection where one programs towards a particular interface and has the result generalised to other variations —a prime use case is to code against a typeclass representation and use the same methods on bundled records.
-- Suppose I have the following syntactic construction. repeat : TermData → ℕ → TermData repeat t Zero = Var 0 repeat t (Succ n) = Add t (repeat t n) -- Here is its semantic counterpart. run : (τ : TermRecord) → TermRecord.Carrier τ → ℕ → TermRecord.Carrier τ run τ t Zero = TermRecord.Var τ 0 run τ t (Succ n) = TermRecord.Add τ t (run τ t n) -- Which is merely multiplication for the naturals. _×_ : ℕ → ℕ → ℕ t × Zero = Zero t × (Succ n) = t + (t × n)
The first two are instances of a package former, and it is not diffcult to construe the naturals as the carrier of a package former. After which, we should be able to write one generic function, by writing according to the pacakge former as the interface.
instance ℕTerms : TermOn ℕ ℕTerms = record {Var = λ n → 0; Add = _+_} {- IsConsumer is defined below; ignore for now. -} exp : ∀{v} {{_ : IsConsumer v}} → do τ ← TermP v; τ → ℕ → τ exp t Zero = Var 0 exp t (Succ n) = Add t (exp t n)
For example, we immediately obtain an instance for strings.
instance STerms : TermOn (List Char) STerms = record {Var = λ n → []; Add = _++_} repeat-s = exp {v = typeclass} {- Yields a whole family, which includes: repeat-s0 : {{TermOn (List Char)}} → List Char → ℕ → List Char repeat-s0 c Zero = [] repeat-s0 c (Succ n) = c ++ repeat c n -}
Now that's re-use! One function for many semantically distinct types. Notice that invoking
exp
onListBop
orTermFunctionsSumOn
values is ill-typed since the mechanically verifiable constraintIsConsumer
fails for those variations. Indeed, we may utilise a number of constraints on our package variations, such as the following.data IsConsumer : Variation → Set where Prod : IsConsumer tuples DepProd : IsConsumer Σ Data : IsConsumer datatype Rec : IsConsumer record
When a user defines a variation, they can signal whether it is a consumer or not. Likewise, one can indicate whether a variation should have
Set
-valued operations on not. Note that a default mechanism could be implemented, but the user should continue to have the ability to enforce a particular discipline —c.f., howC#
allows the user to enforce the subtyping variance of a type former.data HasConstructiveRelations : Variation → Set where Prod : HasConstructiveRelations tuples DepProd : HasConstructiveRelations Σ Rec : HasConstructiveRelations record
For example,
data
declarations cannot contain proofs of an arbitrary, but fixed, constructive relation without declaring it as a parameter to the type. Nonetheless, a user may want to be able to express syntactic statements about such proof terms —say for proof automation— and they should have the ability to toggle such a feature.A more important concern is the type of
exp
: The phrasedo τ ← TermP v; τ → ℕ → τ
elaborates to different types according to the value ofv
, whence to defineexp
it seems necessary to actually pattern match on it to obtain a concrete type, which, for example, may contain more arguments. Case analysis on the possible packaging variations is far from ideal —one might as well re-implement the definition only on the cases they want rather than all cases. The aim —to be pursued further in the full thesis effort— is to invert the process: Avoid case analysis in favour of a particularly convenient view.This is clarified best by referring to the current prototype language: Lisp. Since all data and methods in a lisp are essentially lists, when one prescribes how to project a value from a possibly nested datatype, then the same prescription essentially directs how to get to the location of that value and so we obtain generic setters. The following tiny example demonstrates this idea.
(setq xs '("a" nil (x y z) 12)) ;; Heterogenous list of 4 items. (cadar (cdaddr xs)) ;; ⇒ y (setf (cadar (cdaddr xs)) 'woah) ;; xs ⇒ '("a" nil (x woah z) 12))
It is this flexibility that we aim to provide to users. They code not against a generic variation, but rather along one that is the most appropriate task at hand. We would hope that it would not be unrealistic to then mechanically derive the other forms from it. For example, suppose we wish to define retracts on magmas; rather than define the concept for each possible view, we define it once and obtain it for other views.
PackageFormer MagmaP (v : Variation) : Set where _⨾_ : MagmaP v → MagmaP v → MagmaP v MagmaOn = MagmaP typeclass AMagma = MagmaP record
The ubiquity of magmas —literally everywhere— lends itself to recall that working with structure, possibly needless structure, may usurp the goals of proof \parencite{purposes_of_proof}: No mathematician would naturally say let M be an algebra on set C when it suffices to say let M be an algebra; yet it may be convenient to phrase problems more elegantly when the carrier set is mentioned explicitly \parencite{packaging_mathematical_structures}. On the other hand, having the carrier explicit for the sake of typeclass resolution relies on decidable type (non)equality; which may be resonable for a simplly typed language but for a DTL type normalisation generally requires non-trivial, non-constant, computation. Anyhow, as mentioned earlier, bundling data is akin to currying or nesting quantifiers, yet is vastly more expensive since library designers generally commit early to one form or another; in this case \newline
AMagma ≅ Σ C : Set • MagmaOn C
and \newlineMagmaOn C ≅ Σ M : AMagma • M.Carrier ≡ C
.retract : ∀{S T} → (f : S → T) → MagmaOn T → MagmaOn S retract f Tgt = record {_⨾_ = λ x y → f x ⨾ f y} where open MagmaOn Tgt
Since
MagmaOn = MagmaP v
wherev = typeclass
, we would ideally be able to derive the generic form —possibly via case analysis.retract-v : ∀{v} → ∀ {S T} (f : S → T) → do tgt ← MagmaP v; tgt ≡ T -- Intentionally no parens. → (do-Σ src ← MagmaP v; src ≡ S) retract-v = ⋯ -- Unclear at this stage.
The record case could, semi-algorithmically, yield:
retract-v {record} : ∀ {S T} (f : S → T) → ∀ (Tgt : AMagma) → AMagma.Carrier Tgt ≡ T → Σ (Src : AMagma) • AMagma.Carrier Src ≡ S retract-v {record} {S} {T} f Tgt refl = record { Carrier = S ; _⨾_ = λ x y → f x ⨾ f y } , refl where open AMagma Tgt
From a usability perspective the trivial proofs should not be present and so we need to algorithmically rewrite the above type to omit them, as follows. We would like to preserve the argument syntax,
retract f Tgt
, that was originally declared. Unfortunately, for the record case, the type off
must refer to the types of the other magamas if we eliminate the trivial equalities. One possible workaround, as follows, is thus to simply provide a omit the tedious equality proofs since they can be found by instance search.retract-v {record} : ∀ {S T} (f : S → T) → ∀ (Tgt : AMagma) ⦃_ : AMagma.Carrier Tgt ≡ T ⦄ → proj₁ (⦃Σ⦄ Src : AMagma • AMagma.Carrier Src ≡ S) retract-v {record} f Tgt = ⋯ -- “⦃Σ⦄ (x : A) • B x” consists of a pair -- where the second is found by instance search.
Notice that we also project at the end since we do not care about the tedious proof; nor should its existence be forced upon the user.
Before we move on, there is particular reason we have deviated from our
TermP
example to theMagmaP
concept. Thedatatype
variation forMagmaP
does not provide a way to speak of variables of the data type —indeedMagmaP datatype
has no closed terms, whence no terms at all. It is thus appropriate to now introduce a variation for syntactic terms over some variable set which is then utilised by a mechanically derivable semantic function that is freely homomorphic.MagmaTermsOn = MagmaP term-typeclass {- ≅ data MagmaTermsOn (Vars : Set) : Set where Var : Vars → MagmaTermsOn Vars _⨾_ : MagmaTermsOn Vars → MagmaTermsOn Vars → MagmaTermsOn Vars MagmaTermsOn-sem : ∀ {v} {A} → do τ ← MagmaP v; (f : A → τ) → MagmaTermsOn A → τ MagmaTermsOn-sem {record} S f (Var x) = f x MagmaTermsOn-sem {record} S f (l ⨾ r) = ll s⨾ rr where _⨾s_ = AMagma._⨾_ S ll = MagmaTermsOn-sem {record} S f l rr = MagmaTermsOn-sem {record} S f r ⋯ -}
We will return to homomorphisms later on, for now it is important to notice that some variations may be useless —as in the empty datatypes. There is also the opportunity to explore co-inductive datatypes.
- Common Operations on Package Formers
It is rather common in the record variation to have multiple instances being mentioned and it is desirable to refer to them with syntactically distinct yet appealing names —such as using subscripts, primes, or other decoration. Moreover, a notion of homomorphism, structure-preservation, can usually be automatically inferred.
Here we show what such declarations looks like, later we show that such things could be user defined.
PackageFormer TermRelP (v : Variation) : Set where Var : Int → TermRelP v Add : TermRelP v → TermRelP v → TermRelP v Rel : TermRelP v → TermRelP v → Set -- This time we have a relation as well.
Declare PackageFormer TermRelP (v : Variation) decorated (λ x → x ++ "′") {- ≅ PackageFormer TermRelP′ (v : Variation) : Set where Var′ : Int → TermRelP′ v Add′ : TermRelP′ v → TermRelP′ v → TermRelP′ v Rel′ : TermRelP′ v → TermRelP′ v → Set -- Coherence Meta-property: ∀ v, d • TermRelP v decorated d ≅ TermRelP v -}
Declare Homomorphism TermRelP (v : Variation) {- ≅ PackageFormer TermRelP-Homomorphism (v : Variation) : Set where Src : TermRelP v decorated (λ x → x ++ "₁") Tgt : TermRelP v decorated (λ x → x ++ "₂") map : Src → Tgt -- Elaborates to “Carrier Src → Carrier Tgt” in “record” variation. var_preservation : ∀ n → map (Var₁ n) ≡ Var₂ n add_preservation : ∀ x y → map (Add₁ x y) ≡ Add₂ (map x) (map y) rel_preservation : ∀ x y → Rel₁ x y → Rel₂ (map x) (map y) NB: The “decorated” annotations are local to the package. -}
- Inheritance & Defaults for Package Formers
Things get a bit more interesting with multiple packaging, fields making use of dependent types, and of (multiple) default implementations. Besides defaults, a desirable feature of our envisioned system is the ability to lift definitional extensions into fields of the package, say for more efficient implementations.
PackageFormer TermP (v : Variation) : Set where Var : Int → TermP v Add : TermP v → TermP v → TermP v
PackageFormer PreOrderedTermP (v : Variation) : Set inherits-from (TermP v) where Ord : OrderedTermP v → OrderedTermP v → Set Refl : ∀ x → Ord x x Trans : ∀ x y z → Ord x y → Ord y z → Ord x z -- Two default ‘implementations’ default₁ Ord x y = x ≡ y default₁ Refl x = refl default₁ Trans _ _ _ refl refl = refl default₂ Ord x y = ⊤ default₂ Refl x = tt default₂ Trans _ _ _ _ _ = tt
Notice how “free type” formation incorporates this new open-ended construct,
Ord
, as a two-value holder. An alternative interpretation would be to eliminate it altogether from the elaborated data declaration. Anyhow, since we elaborate a relation as a pair former, proofs for such a relation cannot be included —otherwise it's not a “free” type!PreOrderedTermData = PreOrderedTermP data {- ≅ data PreOrderedTermData : Set where Var : Int → OrderedTermData Add : PreOrderedTermData → PreOrderedTermData → PreOrderedTermData Ord : PreOrderedTermData → PreOrderedTermData → PreOrderedTermData -- No reflexitivity axiom on ‘Ord’, nor transitivity! -}
PreOrderedTermData = PreOrderedTermP data with-default₁ {- ≅ data PreOrderedTermData : Set where Var : Int → OrderedTermData Add : PreOrderedTermData → PreOrderedTermData → PreOrderedTermData -- No ‘Ord’ construction, but instead a constructive relation and properties: Ord : PreOrderedTermData → PreOrderedTermData → Set Ord x y = x ≡ y Refl : ∀ x → Ord x x Refl x = refl Trans : ∀ x y z → Ord x y → Ord y z → Ord x z Trans _ _ _ refl refl = refl -}
The naming
Ord, Refl, Trans
could have been altered to refer to the newly declared data type, for simplicity we have avoided such a transformation. Moreover, we could reservewith-default₀
to simply omit constructive relations from being reified as data constructors.PreOrderedTermRecord = PreOrderedTermP record {- ≅ record PreOrderedTermRecord : Set where field Carrier : Set Var : Int → Carrier Add : Carrier → Carrier → Carrier Ord : Carrier → Carrier → Set Refl : ∀ x → Ord x x Trans : ∀ x y z → Ord x y → Ord y z → Ord x z -- Notice that the reflexitivity & transitivity axioms are kept! -}
Moreover, the default implementations means we also have the following declaration, where distinctions are made by the occurenace, or absence, of fields.
{- record PreOrderedTermRecord : Set where field Carrier : Set Var : Int → Carrier Add : Carrier → Carrier → Carrier Ord : Carrier → Carrier → Set Ord x y = x ≡ y Refl : ∀ x → Ord x x Refl _ = refl Trans : ∀ x y z → Ord x y → Ord y z → Ord x z Trans _ _ _ refl refl = refl -}
Here is our first observation of a uniform presentation of packaging, where the “intended use” differs: Whether we want axioms or not?
Not only is the use amicable, but utilities written for the first elaboration effortlessly apply to instances of the second elaboration. Unfortunately, the relationship is not symmetric —e.g., using the additional information provided by the default implementations,
∀ x y → Ord x y → Add x y ≡ Add y x
is provable for the latter but not the former. As such, there is need to be able to mark results applying to a subtype of a package former, or to eliminate such a desirable feature that reduces needless distinctions when applying utilties of the former to the latter. The thesis will provide a solution with a discussion of the alternatives and why they were not adopted. - Package Formers Dispense with The Diamond Problem
Let's consider combining multiple containers.
Package UnitalTermP (v : Variation) : Set inherits-from (TermP v) where unit : UnitalTermP v lid : ∀ x → Add unit x ≡ x rid : ∀ x → Add x unit ≡ x
Package PreOrderedMonoid (v : Variation) : Set inherits-from (UnitalTermP v; PreOrderedTermP v) where associative : ∀ x y z → (Add x y) z ≡ Add x (Add y z) monotone : ∀ x x' y y' → Ord x x' → Ord y y' → Ord (Add x y) (Add x' y')
This package ought to be indistinguishable from the following, whence allowing tremendously flexible declarations and uses. In particular, there is no longer a need to distinguish between a hierarchical and a flattened perspective, since they are considered identical.
Package PreOrderedMonoid (v : Variation) : Set where unitaltermp : UnitalTermP v preorderedtermp : PreOrderedTermP v associative : ∀ x y z → (Add x y) z ≡ Add x (Add y z) monotone : ∀ x x' y y' → Ord x x' → Ord y y' → Ord (Add x y) (Add x' y') -- From which sub-structure does the above “Add” arise? -- -- The “record” and “typeclass” variations elaborate with axioms declaring -- that identical names are indeed identical operations: carrier_coherence : unitaltermp.Carrier ≡ preorderedtermp.Carrier var_coherence : unitaltermp.Var ≡ preorderedtermp.Var add_coherence : unitaltermp.Add ≡ preorderedtermp.Add -- -- They also elaborate with default tedious implementations: carrier_coherence = refl; var_coherence = refl; add_coherence = refl -- Moreover, we can continue the ‘default’ implementation. default₁ monotone _ _ _ _ refl refl = refl default₂ monotone _ _ _ _ _ _ = tt
- Package Formers & Representational Shifts
Let us close this section by demonstrating how this genericity can aid in ubiquitous representational shifts that appear rather often in dependently typed programming. In pedestrian languages, there are usually less ways to accomplish a task in dependently typed languages and so programming style is not of great concern. In contrast, in a DTL, a user could, for example, work over an abstract data type where a particular argument is fixed or where it is allowed to vary. The two approaches are a matter of style, but can lead to awkward situations.
More concretely, we consider the bread and buffer of coding: Graphs. Without dependent types we can only speak about graphs over a given vertex type, with dependent types we can speak about a graph, irrespective of vertex type. The former is tantamount to the context
Vertex ∶ Type ⊢ Edges ∶ Vertex → Vertex → Type
, and an empty assumption context⊢ Vertex ∶ Set, Edges ∶ Vertex → Vertex → Type
for the latter. However, the latter form sometimes leads us into contexts where we have two graphsG
andH
for which we make the tedious constraint \newlineVertex G ≡ Vertex H
. It would be less clumsy to explicitly declare the two graphs to be over the same vertex type.The previous paragraph mentioned a terse dependently-typed presentation of graphs, let us use the classic presentation as it may be more familiar to readers.
PackageFormer GraphP (v : Variation) : Set where Vertex, Edges : Set src, tgt : Edges → Vertex -- The dependently typed notion of edges. derivied _⟶_ : Vertex → Vertex → Set x ⟶ y = Σ e : Edges • src e ≡ x ∧ tgt e ≡ y
AGraph = GraphP record renaming (Carrier to “Vertex”) {- ≅ record AGraph : Set where field Vertex Edges : Set src tgt : Edges → Vertex -} -- NB. The implicitly generated name “Carrier” has been identified with -- the *declared* name “Vertex”. This is acceptable since they have the same type. -- Without the identification, the record elaboration would have provided a -- third type field named “Carrier”.
GraphOver = TermP typeclass renaming (Carrier to “Vertex”) {- ≅ record GraphOver (Vertex : Set) : Set where field Edges : Set src tgt : Edges → Vertex -}
With these in hand, our goal is to replace the following first line with the second. However, since both types
GraphOver
andAGraph
are declared as one liners, such a transition is a cheap as possible.(G H : AGraph) → Vertex G ≡ Vertex H → ⋯ (V : Set) → (G H : GraphOver V) → ⋯
In order to replace a semantic constraint with a syntactic constraint the user simply need to use a variant on packaging. Furthermore, we are ensured \newline
AGraph ≅ Σ V ∶ Set • GraphOver V
.Dependently-typed graphs are an curious structure. With a bit of renaming, and adding a few laws, we obtain a ‘setoid’ –i.e., an undirected graph where every node has a self-loop, and paths correspond are essentially edges.
PackageFormer SetoidP (v : Variation) : Set where -- Graph structure Carrier : Set _≈_ : Carrier → Carrier → Set -- Properties refl : ∀{e} → e ≈ e sym : ∀{d e} → e ≈ d → d ≈ e trans : ∀{c d e} → c ≈ d → d ≈ e → c ≈ d
A non-dependently-typed ‘signature’ of a structure is generally obtained by discarding the relational operators and all properties. For
SetoidP
one would immediately think the signature consists of justCarrier
. However, if we view it instead as undirected graphs with self-loops at each node and edge-transitivity, then one would say the signature is the verticesCarrier
and the edges_≈_
. It is thus not clear when an item,_≈_
or_⟶_
, forms constructive proofs or provides a type family. As such, signature extraction thus requires a parameter identifying which elements constitute ‘proof matter’ —then one simply filters a pacakge-former against this criterion to obtain the associated signature. More generally, this allows us to take anX
structure and obtain may of its the associated views about where knowledge is consolidated \parencite{realms}, including:X = ⟨ Carrier; Operations; Properties ⟩ -- C.f., SetoidP XOver C = ⟨ Operations; Properties ⟩ IsX C Ops = ⟨ Properties ⟩ XSig = ⟨ Carrier; Operations⟩ -- C.f., GraphP
Having the signature in hand, one can easily and mechanically generate many derivied concepts. For example, a ‘homomorphism’ is a family of functions of the underlying sorts such that the given operations are preserved. Likewise, equality of homomorphisms is extensional equality of the underlying maps. One can then generate closed and open terms and their interpretation functions. With this approach to signature extraction, we can use the same algorithms for the production of, say homomorphisms or other constructs, on completely different algebraic structures, whether they be monoids or graphs. Moreover, this implies that concepts generally not considered for a class of algebras can easily be derived and experimented with; likewise for exploring new algebraic theories. These matters are an application, rather than a goal, of our envisioned system.
Sometimes constraints on an item can be derived, leaked by a signature.
E.g., the signature of sets, on a carrier, leaks that the carrier necessary has decidable equality.
The curiosity of graphs is that they are one of the simplest two-sorted structures and one of the most common in computing. Counter to intuition, existing packaging systems, namely canonical structures and typeclasses, are oriented toward having a distinct parameter: They cannot work well with multi-parameters; like classical single-sorted algebra. However, the both aim to solve a usability problem: Having to spell out everything is too tedious. Typeclasses are essentially dictionary look-up, having unicity as an issue. Whereas canonical structures require familiarity with how unifer works –we provide enough information to the unifer to find the desired structure– but, in general, canonical structures do not scale. It is one of the thesis efforts to ensure the the unionised approach scales by a complex example with clear avenues of extension.
It should be clear from these examples that package formers provide expectant generality, including the common uses one is mostly interested in. What about unexpected uses? What if a user wishes to utilise a representation we did not conceive of? They should be able to use the existing language to form it.
3.4.2 Second Observation: Computing Similarity for Containers
By necessity of the first corollary, we are forced to utilise a uniform language
between the varying notions of packaging thereby relegating their treatment
to be a normal aspect of a language's core vernacular, rather than an extra-linguistic feature.
The previous examples hint at possible issues regarding well-definedness of certain constructs.
Moreover, we only elaborated on a few compositional operations,
inherits-from, renaming, decorated
, yet users
may well wish to utilise their own compositional schemes and so it is imperative that we allow
them such a flexibility.
Consequently, users ought to be able to define their own compositional mechanisms, thereby
necessitating that they be able to manipulate package declarations themselves
which in-turn forces the language to be somewhat homoiconic. Moreover, to avoid a hierarchy
of languages, the facility for manipulating package declarations must itself be a part of
the core language, rather than an extra-linguistic feature —c.f., Coq's Ltac.
In our envisioned setup, every PackageFormer
declaration adds a clause to a special
function,
packageInfo : PackageFormer → PackageInfo packageInfo = ⟪compiler defined⟫
Where a PackageInfo
consists of Name
, which is a list of parameter names and types, along with the name of the package former;
and Declarations
, a list of name-type pairs whose last element is the target type.
{- Draft: Lots of string manipulation, not ideal. -} record PackageInfo : Set where field Name : List (String × String) × String Declarations : List (String × List String) -- -- This is just another package, -- it incidentally happens to be the representation of packages!
It is to be noted that there is no commitment to a string-based representation. It is only a prototype and the thesis will likely move to a better typed representation —otherwise, we may run into too many problems of ill-formed package formers.
PackageFormer TermP (v : Variation) : Set where Var : Int → TermP v Add : TermP v → TermP v → TermP v
The above declaration provides, under the hood, the following clause to packageInfo
.
packageInfo TermP = record { Name = ["v", Variation] , "TermP" ; Declarations = [ ("Var", ["Int", "TermP v"]) , ("Add", ["TermP v", "TermP v", "TermP v"]) ] }
We are now in a position to provide the semantics for the keyword Declare
,
from the previous section. It takes a PackageInfo
and declares a PackageFormer
.
There should be a compile-time warning if such declarations are meaningless, ill-formed.
For example, the previous \newline Declare PackageFormer TermRelP (v ∶ Variation) decorated (λ x → x ++ "′")
can thus be obtained by a user by defining decorated
as an operation on packages!
_decorated_ : PackageInfo → (String → String) → PackageInfo pk decorated f = record { Name = bimap id f pk.Name ; Declarations = fmap (bimap f id) pk.Declarations }
To rectify the seemingly wild mixfix notions, we request from the compiler
the following suitably general syntactic sugar.
An operation, call it, altered-by
of the type PackageInfo → List PackageInfo → List X → PackageInfo
automatically obtains the syntactic sugar p altered-by (q0; …; qk) with (f0; ...; fN)
—c.f., the inherits-from
syntax above.
With such terse functional programs for forming composition schemes, there is no need to build much into the compiler.
Users can define other similar operations, such as decorated-rounded
which replaces the first two binary relations' names with ⊆
and ⊂
;
or decorated-square
to make the renamings ⊑
and ⊏
.
Additionally, such renames would propagate into any axioms or derived laws.
Moreover, the flexibility to invoke such operations in complex ways allows for
intricate renamings to be generated at tremendous scale without worry that
future renames would need to be made if the orginal packages included new items.
Numerous examples of such renaming transpire manually in the impressive
RATH \parencite{RATH} development, as well as in Agda's standard library.
When working with multiple values of the same record type, for example,
one encounters a usability problem: Refereeing to the constituents without being verbose.
The simplest solution is to qualify each invocation, as in instance.field
, however this
is rather cumbersome, inelegant, and is awkward for mixfix names. An alternative is to
locally rename the fields according to a scheme reflecting their use. For example, in
a produce construction of 5 items, the field names would be renamed to have a subscript number.
In a setting of two instances, a user may instead prefer a primed and an undecorated version
of field names. Thus far, by hand we have created these tedious subscript and primed renamings,
with our envisioned systems, we need no longer worry about such boilerplate.
In nearly the same fashion, a user could have defined the inherits-from
compositional scheme.
Such a scheme may assume that all identically named items have the same types, and crash otherwise.
A user could define a better scheme that takes a renaming function, or another function to handle
the crash, or simply omitt conflicting names altogether.
The examples suggest that many commonly occurring compositional mechanisms \parencite{tpc}
can be directly provided by a library, rather than by a particular compiler
—this includes the ability to hide fragments, expose the largest well-defined fragment,
and to combine packages along a given substructure.
Rather than select what we think is best, we can simply provide the general mechanism to the library designer and allow them the freedom to provide their own schemes.
3.4.3 Next Steps
Our brief examples demonstrate that the less design decisions about packaging made by language designers, the more general, applicable, and, most importantly, increased homogeneity in the resulting datatype language without becoming unityped but rather thanks to being dependently-typed. As mentioned in the previous section on existing approaches, one formalism for packages is that of theories and theory combinators; below we thus draw on some problems from theory combinators rendered toward packaging systems.
We have mentioned that the record
and typeclass
perspectives solve the common requirement of
structures sharing an identical field. Other than that, we have essentially only
outlined a general mechanism for declaring packages and compositional schemes, but have not
discussed which are the most common and most useful packaging combinators.
It is also desirable to discuss the formal properties of such combinators
—if anything, to ensure they are sensible and behave as expected.
Moreover, which combinators act as a basis for all packaging combinators?
Whence their use ensures the resulting composition is well-formed
and they could be targeted for optimisations.
To make our approach accessible, the generic package operations are brought to the user
rather than baked into the compiler —too great a distance for most users.
The Declare
syntax reifies PackageInfo
's into package declarations, but we have not mentioned
under what constraints it can actually provide compiler-time, or typechecking-time,
errors of ill-formedness. Moreover, how (in)efficient is this process?
Could it be extended to work on variable, runtime provided, declarations
for refying packages? Perhaps there is a constraint that suffices for the most common cases?
Moreover, having observable PackageInfo
's being automatically generated for every package declaration
renders representation hiding nearly moot.
The proposed approach boarders on meta-programming. Can type erasure and other compiler-specific optimisations be brought into the homoiconic-like setting being pursued here? We have mentioned a few ‘built in’ variations for packaging; can such a feature be liberated from the compiler and be bent to the users' will? We would need the ability to explain how a package elaborates.
Tremendous flexibility is demanded from the back-end so as to ignore needless distinctions at the users' level. Whereas the practicality is promising, the feasibility of an implementation for such ambiguous parsing \parencite{ambiguous_parsing} is unclear. It is also unclear what effects identifying syntactically distinct items has on, say, normalisation and propositional equality.
The numerous claims and associaited bookkeeping of details pushes us into using a proof assistant, Agda.
Our examples have been ‘variation’ polymorphic;
we have been even more generic by defining decorated
.
What are the limits of programming genericity provided by our scheme?
It would unsurprising if this approach yields
the next 700 module systems.
4 Approach and Timeline
Packages, modules, classes, (dependent) records, (named) contexts, telescopes, theories, specifications —whatever you wish to call them are essential structuring principles that enable modularity, encapsulation, inheritance, and reuse in formal libraries and programs. Moreover, as we have demonstrated, with the exception of use-cases, there are no significant differences between them in a dependently-typed setting, as \parencite{theories_as_types} present a type theoretic calculus of a variant of record types that corresponds to theories.
4.1 Implementation Matter
We will realise our proposal in an existing compiler and so working with it necessitates our implementations to be more than just ‘research quality’ but actually ready for a broad audience.
Which compiler and for which language?
Since our attention is focused on dependently typed languages within the realm of Type Theory \parencite{lof_constructive_math}, Agda \parencite{agda_web} is a natural candidate.
Agda is currently one of the most used tools for proof and program experimentation
involving dependent types. With its support for mixfix Unicode lexemes, it has
become a strong competitor to Coq \parencite{coq_website,coq_inductive_coc, coq_coc} for both proof construction \parencite{agda_fixpoints, agda_quantifier_elim, agda_nondeterministic, agda_mergesort, agda_type_Safety, agda_aop}
and general program construction \parencite{agda_web, agda_trains, agda_bitcoin, agda_hardware}
—Agda's lack of syntactic distinction between
programs and propositions, along with its pattern matching utilities in-place of
‘tactic sledgehammers’ \parencite{tactics}, it has also become an attractive
language for introducing dependent types and functional programming
\parencite{agda_iowa_book, agda_plf, agda_teaching}. With its syntactic similarity to Haskell, many Agda users treat
their Agda code as if it were lazy with the let
and where
clauses preserving sharing
—which is not the case, since such clauses rewrite to top-level functions
\parencite{agda_docs}.
Instead, Agda's evaluation strategy is normal order: Function definitions
are invoked before arguments are evaluated, but computations of arguments
are not shared. This is a prime location for efficiency issues since type-checking
in a dependently typed language tends to involve evaluation of terms.
Surprisingly this has not stopped users from producing large-scale software
developments \parencite{RATH, agda_trains, agda_web}.
Needless to say, a poor choice of elaboration strategy can lead to a loss of sharing —not that Agda has sharing to begin with—, contain too many undesirable side-effects, hinder efficiency, or forgo compile-time optimisations. For example, Agda, as currently implemented using the Glasgow Haskell Compiler (GHC), is a realisation of Type Theory (MLTT) that is heralded as both a programming language and proof assistant. Unfortunately MLTT, as many other dependent logics —such as the Calculus of Constructions with inductive types, which underlies both the Coq and Lean proof assistants— does not account for modules, thereby leaving these as consistency-preserving hacks thrown onto the implementation. As mentioned earlier, Agda simply rewrites modules into top level functions with module parameters realised as parameters to the resulting functions. This is an implementation detail and has little impact on theory construction, however, code reuse becomes unreasonably slow due to the loss of sharing that happens when module arguments need to be re-normalised in each function-counterpart. Consequently, only a minor subset of the Agda community actually executes their programs. The rest of the community is generally content with type checking only; which does not hinder the reliability of proof.
It is important to note that we employ Agda only as a proof-of-concept for our proposed exploration of first-class structuring-mechanisms in dependently typed languages. Admittedly Agda's support for Unicode mixfix lexemes makes it a pleasure to work in, with mechanised proofs being little work more than their LaTeX renditions.
4.2 Next Steps
The approach we intend to follow consists of the following steps. Notice that feedback loop of practice into theory.
Really study the other mechanisms that already exist.
Exhibiting such a weakness may suggest insufficient preparatory work! Possibly resulting in a fail!
- Survey module systems in theory, in existing DTLs, and in non-DTLs.
- As far as we can tell, besides the MTT \cite{mmt_main_paper, mmt_api} group, no one else is working on actually implementing solutions to the flaws we have identified, such as combination over structures.
- This is promising in terms of novelty, if anything.
- Analyse why there are not multiple implementations of such seemingly immensely useful concepts.
- Distill the true requirements for a solution;
ensure good fit for purpose criteria exists.
- Understand the requirements of `modularity mechanisms' for DTLs.
- Narrow down a design by choosing a set of requirements.
- Identify necessary, and practical, trade-offs. Conflicting feature sets? Usability?
- Ideally we want our implementations to avoid too much overhead, such as creating an entire new language; this may necessitate the weakening of other functionality.
- Deepen understanding of the opportunities given by DTL.
Understand the relationships between modules, records, contexts, telescopes, and signatures.
- Do they have differing `types'?
- As types themselves, do they have differing `values'?
- In the setting of DTLs, are they essentially isomorphic?
- What are the intended uses? What intentions do particular choices communicate?
- E.g., “\(x = y\)” communicates an equality and nothing more, whereas
“\(x\! \iff\! y\)” communicates a Boolean equality: A redundant, particularised, equality symbol serves to succinctly and elegantly communicate more information.
- Formulate basic, draft, semantics for a small set of DTL module primitives.
- What is the type of a package former?
- How does it fit into Agda's existing type hierarchy?
- What are the types of the primitives themselves?
- We wish to avoid metaprogramming after all, and so wish to remain within the language rather than in a metalanguage.
- Prototype some mechanisms; a combination of old, adapted, and novel ones
to demonstrate the power of the system.
- Implement the structuring mechanism combinators discussed earlier
—such as combination over common-substructures.
- Possibly begin with reifying first class grouping mechanisms by representing contexts —i..e, sequences of declarations with optional definitions— as records in Agda with the undefined declarations being fields and the rest being derived or definitional.
- Implement the structuring mechanism combinators discussed earlier
—such as combination over common-substructures.
- Evaluate the mechanisms —using fit-for-criteria.
- Since the realisation would be in Agda, we would keep in touch with the community to ensure that the additions contribute to program design.
- Evaluate the strength of the resulting additions in terms of practical use for library designers as well as in terms of program speed.
- Make sure to have a denotational semantics for the mechanisms.
- Ensure that the additions are minimal, orthogonal, and construct a sound type theory around them.
- Refine 2-6 until elegance, or deadline, is reached, whichever comes first.
Our timeline will discuss how we will carry out this approach in multiple passes and will discuss the conditions of a successful pass.
4.3 Timeline
We shall iterate through the `approach phase' three times, utilising a feedback loop of practice into theory. The phases are discussed below.
As our results will likely need to be re-proven for definitional adjustment, we intend to mechanise all of our proofs in Agda as well —when possible. Therefore, Agda plays multiple roles: A dependently-typed language to experiment with, as well as a proof checker for our results.
4.3.1 The First Pass: May-October 2019
This stage concludes successfully provided the following checkpoints are achieved.
- A thorough understanding of what is being done by others, and how our approach differs, is obtained and documented.
- Understand the Agda compilation ecosystem, provide a report on how to make alterations to it, and actually implement at least one structuring mechanism and provide use cases as well as preliminary efficiency analysis.
- A publication covering existing mechanisms, their features and flaws,
and possibly an explanation of why there is theoretical work on these issues
but little to no implementation on them
—with a focus on practical uses and possible hurdles to use.
- A side-effect of this is to produce an evaluation strategy for the mechanisms.
- Moreover, this necessitates looking into the associated semantics, evaluating them, and proposing semantics for the mechanism we have designed.
- Thesis writing should have begun and nearing completion are sections on introduction and background.
4.3.2 The Middle Pass: November 2019 - February 2020
This stage concluded successfully provided the following checkpoints are achieved.
- The success of the previous stage ensures an understanding of the Agda compilation
ecosystem, as such it should take less time to implement the more mechanisms,
theory combinators. The goal is to have the remaining mechanisms implemented,
with a focus on the combination-over-a-structure mechanism.
- With each implementation, reach-out to the Agda community to solicit feedback regarding improvements and possible use cases.
- Extending the semantics for the newly implemented mechanisms.
- Evaluating which mechanisms are more primitive, which are derived, and which can be used to allow users to make their own using the concrete language itself!
- A publication of case studies utilising these combinators, as well as
a comparison of how these are an improvement over traditional methods.
- Analysing the interactions between features; does the addition of one hinder another.
- Empirical tests for efficiency and utility.
- Thesis writing should have progressed with sections on use cases, semantics, and feature design, having substantial matter if not nearing completion.
4.3.3 The Final Pass: March - April 2020
This stage concluded successfully provided the following checkpoints are achieved.
- Ensure that our implementations are meeting our requirements for a solution.
- Begin mechanisation of proofs authenticating that the denotational semantics has desired, expected, properties; such as soundness and safeness.
4.3.4 Concluding Phase
Wrap up all proof matters and finish the thesis.
Suffice to say life tends to be more hectic than a schedule may permit and as such some times may deviate from the above intentions. Regardless, the goal will be to complete the thesis within 2 years time; in particular before September 2020.
5 Conclusion
As already discussed,
more often than not a module system is an afterthought secondary citizen
whose primary purpose is to act as a namespace delimiter
—e.g., C#'s namespace
construct—
while relatively more effort is given to their abstraction encapsulation
counterpart, e.g., C#'s class
'es.
Some languages' module systems blend both namespace management and
implementation hiding, e.g., as in the Haskell programming language.
Other languages such as OCaml take modules even further: Not only are modules
used for namespace organisation and datatype abstraction, but they can also be
passed around as values for manipulation as if they were nothing special, thereby
collapsing the distinction between record constructs and organisational constructs.
The proposed research is to build upon the existing state of module systems and develop an extension to a compiler to substantiate our claims, and to ultimately discover new semantical relationships between programming language constructs in a dependently typed setting with modules as first-class citizens. This involves redesigning and enhancing existing module systems to take into account dependent types as well as producing rewrite theorems to ensure acceptable performance times.
Intended outcomes include:
- A clean module system for DTLs
- Dependent types blur many distinctions therefore rendering certain traditional programming constructs as inter-derivable and so only a minimal amount need be supported directly, while the rest can be defined within the extended type theory we will be creating. Since modules are records, which are one-field algebraic data types, and we can form sums of modules, it would not be surprising if first-class modules suffice for arbitrary data type definitions.
- Utility Objectives: A variety of use-cases contrasting the resulting system with previous
approaches. In particular, the system should:
- Reduce amount of ‘noise’ necessary for working with grouping mechanisms in a number of ways.
- It should be easy and elegant to use and, possibly, to extend.
- A module system that enables rather than inhibits (or worse) efficiency.
- Currently Agda modules, for example, are sugar for extra functional parameters and so all implicit sharing in modules is lost at compilation time.
- Deeply nested, deeply tagged, operations could be costly and so being apply to soundly flatten modules and soundly extract operations and results is a necessity when speed is concerned —moreover, this needs to be mechanical and succinct if it is to be useful.
- Demonstrate that module features usually requiring meta-programming can be brought
to the data-value level.
- Names and types, for example, in a module should be accessible and alterable. For example, we can obtain a rig by combining two instances of a monoid module where we would rename the fields of one, or both, of them.
- Thereby relegating abstract syntax tree and programs-as-strings manipulations to the edges of the computing environment.
Most importantly, we intend to implement our theory to obtain validation that it “works”!