The Proof Expression Problem, Reimagined Through Object-Oriented Lenses

Table Of Links

ABSTRACT

1 INTRODUCTION

2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING

3 CASE STUDY

4 DESIGN CONSTRAINTS AND SOLUTIONS

5 FORMALIZATION

6 DE/REFUNCTIONALIZATION

7 FUTURE WORK

8 RELATED WORK

9 CONCLUSION AND REFERENCES

CASE STUDY

We will now further illustrate the benefits of dependently typed object-oriented programming in a small case study. For this, we create a mockup of a dependently typed web server. We will observe that we can conveniently extend both the supported routes of the web server and the supported methods to access these routes. We will also see how we can conveniently state and enforce properties in intrinsic as well as in extrinsic style.

3.1 A Functional Web Server

We start in the familiar realm of functional programming. For the purpose of this demonstration, we will create a simple web server that allows all users to read, but only authenticated users to increment a counter. For this, we track user sessions using the State type shown below. As an instance of intrinsic verification, we track on the type level whether the user is authenticated. Possible responses from the server are specified by the Response type.

Our web server should accept a couple of HTTP request methods (get, post, …) for a set of routes (Index, Admin, …).

Adding support for a new request method is as simple as adding a function. For instance, we want to handle post requests, even though we forbid them for the Index route:

3.2 Adding New Routes in Object-Oriented Style

While adding new methods is a local change, adding a new route in the functional representation requires touching all pattern matches on Route in the program. Therefore, before adding a route to increment the counter on a POST request, let us refunctionalize Route to its object-oriented decomposition:

In the object-oriented decomposition, adding the following Admin route is now a local change. Note that the rearrangement works both ways: we could transpose the program back into functional decomposition to add another method.

Similar problems of modularity appear in many applications. Functional languages force us to always choose the same extensibility dimension for every type: We can extend data types with new observations, but we cannot easily extend types with new constructors. If the programming language would support both programming paradigms equally well, this choice would not be forced on the programmer by the language, but the programmer would have the choice for each type.

3.3 Verifying Properties on Routes

In addition to the ability to increment the counter by sending a POST request to the Admin route, we may also want to allow explicitly setting a counter value. Updating the counter to a value should be idempotent, i.e. calling the route more than once should have the same effect. The HTTP PUT method is supposed to capture this behavior, but how can we enforce it in our code? This leads us to another benefit of the object-oriented style in that we can express such properties extrinsically but still as part of the interface (compare 2.2):

3.4 The Proof Expression Problem

The classical example of the expression problem [Wadler 1998] concerns extending implementations of term languages by new constructors as well as functions on expressions like print or eval. Very similar problems arise when formalizing programming languages in proof assistants, where one might want to extend the formalization both by new syntax and by new theorems. In Appendix C, we explore how the proof expression problem manifests differently in an object-oriented proof assistant as opposed to a functional one.

:::info
Authors: