mmmodularity!

» by Scott Kilpatrick

Does anyone know of any efforts to develop a form of intuitionism wherein “proof” is actually a trust network that establishes, under some threshold, the truth of a proposition? I suppose such a system would resemble access control logics, where $p~\mathsf{says}~\phi$ is a formula meaning that principal $p$ has stipulated the truth of formula $\phi$. In my head, a proof term is now an entire network of principals and their relative trust in each other, paired with a traversal of that network that establishes the fact.

This is a half-baked (or rather, 1/16-baked) idea for my long-term research goal of designing a formal language of reasoning for use in journalism.

Update at the bottom!

In the last post I described Haskell’s current, limited notion of module identity. (It was none too exciting.) Now I’ll expand on that notion in our new package language. With a richer, more careful semantics of identity, we grant packages with the power of generic reusability!

Read More

In first-order module languages such as Haskell’s, the identity of a module is given solely by its programmer-written name, e.g. Http. When dealing with packages, the identity is augmented with that of its defining package, e.g. httplib-4.1:Http. These names induce a straightforward equivalence relation on modules: modules P1:M1 and P2:M2 are equivalent iff P1=P2 and M1=M2.

Why does module identity matter? Because type equivalence is a direct consequence of module equivalence. Two type constructors T1 and T2 are equivalent iff their original, defining modules are equivalent (and T1 and T2 are syntactically the same type constructor). Note that, e.g., the type constructors http-4.1:Http.Request and http-4.2:Http.Request are *not* equivalent since the two defining module identities are (slightly) distinct.

Read More

What’s the difference between a “package” and a “module”?  Though modules have evolved beyond their low-level origins into richly composable, type-based abstractions, packages are largely stuck in a Linux-like land of version ranges and imprecise specifications.

How can we bring packages up to speed with contemporary module systems?  For my first big project, I’m investigating this question in the context of GHC Haskell and its package management system, Hackage/Cabal.

Read More

Ben Delaware is thinking about mixin modules for Coq as a means of modularly extending data types, theorems, and proofs. (This is a dramatic departure from the mixin modules of (Dreyer and Rossberg, 2008), where (inductive data) types may not be extended once defined. In MixML two type exports only link together if one is a subtype of the other, according to some notion of core subtyping.)

Here’s an example of Ben’s idea. (Please correct me if I’m wrong, Ben.) Consider a Coq module $M$ containing an $\mathtt{Inductive}$ definition of some object $T$, as well as a theorem $\phi$ about $T$ with corresponding proof term, $p : \phi : \mathrm{Prop}$. Another module ${\delta}M$ would be mixed in to $M$, providing extensions (i.e. new or modified constructors) of $T$, $\phi$, and $p$, resulting in a new module $M’$ that contains the fully extended type, theorem, and proof.

As Ben explained this to me, my mind immediately jumped to category theory, due to my recent exploration of inductive definitions. If inductive data types are least fixed points of functors, what are these extensions? Maybe natural transformations? Gil and I talked it through, and the natural transformation interpretation seemed plausible. I hope to investigate this idea more soon.

While Ben is attempting to flesh out his full-featured idea for Coq, I’m thinking about this category theory interpretation in the context of a simpler, HM-like type system. The specific case of extensible data types in FP, from a practical standpoint, has been tackled before, e.g., as polymorphic sum types and first-class cases (Blume et al., 2006). To my knowledge, however, there is no foundational story for this kind of extensibility in the language of category theory.

* * *

OOP aside: This kind of extensibility should seem familiar to OOPers since, essentially, that’s what classes and inheritance do. Extending a data type with new constructors is like adding new subclasses; extending a term with new cases is like adding new methods; and all the while the programmer only writes the new stuff in these extensions. In the code, each $\mathtt{instanceof}$ + downcast on an object of class $C_T$ in OOP corresponds to an elimination of (i.e. pattern match on) a term of $\mathtt{Inductive}$ type $T$ in FP. A key distinction is that such eliminating code presupposes an “open world” of subclasses in OOP but a “closed world” of constructors in FP. In more concrete terms, the FP pattern match would be ill-typed without explicitly handling any new, mixed-in constructors of the type, whereas the OOP downcast would still be well-typed.

In MixML $\mathtt{let}$ binding of one module inside another is defined as syntactic sugar:

This definition highlights the minimalism of MixML (along with other definitions): one can express the entire ML module system in it. Unfortunately, the compactness of the language can hinder one’s understanding of these “macro-expressible” constructs. For my own benefit I wrote out the explicit elaboration rule for $\mathtt{let}$, so why not post it here:

In the last post I discussed the ambiguity and incompleteness of the Hindley-Milner type system with type classes. I also mentioned that I would follow it up with an idea I was pursuing, which, as it turns out, I’m no longer pursuing. This time I’ll motivate the idea by explaining why I was led to it in the first place. The last post describes, really, the post hoc motivation for it, whereas this post describes the actual motivation. 

Read More

Update: Now using MathJax to render mathy things nicely.

$\newcommand{\int}{\mathrm{int}}\newcommand{\bool}{\mathrm{bool}}\newcommand{\string}{\mathrm{string}}$In this post I provide background information on an idea that I’ll explain in the next post. People familiar with Hindley-Milner and type classes won’t get much out of this, except maybe the last part.

Hindley-Milner: the sacrosanct type system for functional programming

The Hindley-Milner type system (HM) comes in two flavors, declarative and algorithmic. The former axiomatizes (as a hypothetical judgment defined by inference rules) the notion of “well-typed” programs while the latter — known as “Algorithm W”, and also referred to as “type inference” — describes a mechanical process for computing the (principal) type of a program. Their coexistence is not superfluous: unlike the algorithm, the declarative system serves as a minimal, human-readable (and machine-provable) specification of the types of programs. 

Read More

Thanks again to Aaron for correcting a misconception I had about the (perhaps most general) principle of coinduction in the comments of the last post. He pointed out that a mixture of inductive and coinductive rules in an inference system gives rise to mixed fixed points, which come up in the mu calculus, for example.

At this point, though, I am ready to retire my pursuit.

It all started with the Henglein and Nielsen POPL paper I shared a while back. In it they define an inference system to prove regular expression containment and claim that it constitutes a “coinductive axiomatization,” on account of a “coinduction rule,” in their words.

They point out that this rule would be wholly unsound without some restriction on its applicability. For example, if the premise is proved with an application of the hypothesis rule, then E <= F can be proved for all E and F. One of their primary contributions is a “semantic side condition” on this rule: the derivation in the conclusion of this rule must have a certain form, and that form guarantees that the resulting proof term `fix f.c` — which they interpret as a coercion from a thing for E to a thing for F — is a total computation. (A major result of their paper asserts that if c is a total function from E-things to F-things then the regexp E is contained in the regexp F.) So, equipped with that semantic side condition, a derivation of `|- c : E <= F` involving the coinduction rule yields a recursive, but total, coercion.

Henglein uses a similar trick in his 1997 paper with Brandt, Coinductive Axiomatization of Recursive Type Equality and Subtyping (CiteSeerX). In that system, the “coinduction” is manifested in the subtyping rule for arrows, presented below.

Here they avoid the possibility of an immediate, unsound use of the hypothesis by specializing it to the arrow case: recursive use of the hypothesis-embedded conclusion in each premise does not actually gain anything.

As far as I can tell, these “coinduction” rules do not imply a coinductive interpretation of either set of inference rules, fully or mixed. Instead, the semantic side condition on the (regular expression) coinduction rule proves that the usual, inductive interpretation of the inference rules — which allows for typical proofs by induction on the structure of derivations* — is sound. Both of their inference systems are coinductive in spirit only, due to the recursive style of moving the conclusion into the hypotheses of the premises.

* In a comment after the last post I stated that I had thought they used “rule induction” in some proofs but then couldn’t find them upon later inspection. My original thought was correct: proofs by rule induction (on derivations of the allegedly coinductive judgments) are indeed present in both papers.

EDIT: Just now, I read in the notes at the end of Pierce’s chapter on recursive types and (co)induction in TAPL that he describes their earlier inference system as inductive! On pp. 312:

Brandt and Henglein (1997) laid bare the underlying coinductive nature of Amadio and Cardelli’s system, giving a new inductive axiomatization of the subtype relation […]. The so-called ARROW/FIX rule of the axiomatization embodies the coinductiveness of the system. The paper describes a general method for deriving an inductive axiomatization for relations that are naturally defined by coinduction […].

CASE CLOSED.

EDIT #2. Fritz Henglein has kindly weighed in on this discussion in the comments below! I retract my statement that his systems are “coinductive in spirit only,” not because he caught me but because his explanation below really does make it clear. In particular, he points to the revised version of the earlier paper (pdf), appearing in Fundamenta Informaticae 1998, in which they discuss this very issue (Section 4).