Table Of Links Table Of Links ABSTRACT ABSTRACT ABSTRACT 1 INTRODUCTION 1 INTRODUCTION 1 INTRODUCTION 2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING 2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING 2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING 3 CASE STUDY 3 CASE STUDY 3 CASE STUDY 4 DESIGN CONSTRAINTS AND SOLUTIONS 4 DESIGN CONSTRAINTS AND SOLUTIONS 4 DESIGN CONSTRAINTS AND SOLUTIONS 5 FORMALIZATION 5 FORMALIZATION 5 FORMALIZATION 6 DE/REFUNCTIONALIZATION 6 DE/REFUNCTIONALIZATION 6 DE/REFUNCTIONALIZATION 7 FUTURE WORK 7 FUTURE WORK 7 FUTURE WORK 8 RELATED WORK 8 RELATED WORK 8 RELATED WORK 9 CONCLUSION AND REFERENCES 9 9 CONCLUSION AND REFERENCES 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 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 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 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 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. Authors:

David Binder
Ingo Skupin
Tim Süberkrüb
Klaus Ostermann Authors: Authors: David Binder
Ingo Skupin
Tim Süberkrüb
Klaus Ostermann David Binder David Binder Ingo Skupin Ingo Skupin Tim Süberkrüb Tim Süberkrüb Klaus Ostermann Klaus Ostermann This paper is available on arxiv under CC 4.0 license. This paper is available on arxiv under CC 4.0 license. available on arxiv xiv

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

The Proof Expression Problem, Reimagined Through Object-Oriented Lenses

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Concatenated Masked Autoencoders as Spatial-Temporal Learner: Abstract & Intro

Deriving Dependently-Typed OOP from First Principles

Rethinking OOP Through Dependent Types and Codata

Why Judgmental Equality Fails Under Defunctionalization

105 Stories To Learn About Functional Programming

100 Days of Code: Death of Summer on the Island of NixOS

Concatenated Masked Autoencoders as Spatial-Temporal Learner: Abstract & Intro

Deriving Dependently-Typed OOP from First Principles

Rethinking OOP Through Dependent Types and Codata

Why Judgmental Equality Fails Under Defunctionalization

105 Stories To Learn About Functional Programming

100 Days of Code: Death of Summer on the Island of NixOS

Light-Mode

Classic

Newspaper

Minty

Dark-Mode

Neon Noir

Minty

HN StartUps