11

There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of structure and behavior in a synthetic manner. The most apparent work I am aware of is the categorical semantics of UML, which is admittedly different from OOP ...


9

The way I understand the difference is that ownership types constrain the shape of the object graph, and substructural systems (like separation logic) manage permissions to access the heap. In the original work on ownership types, the idea is to maintain the invariant of owners as dominators. An object $o$ is dominated by an object $d$, if every path from ...


7

For a better understanding I would recommend Stepanov's book , Mike Stay's article, and his more recent blog on Category Theory in Javascript. Use composition not inheritance. Use sum types like enums to shrink the state space of your variables. Use product types (tuples) like std::pair in C++. If you have a function like A someFunc(A a, B b, C c); the ...


7

I recently finished writing a survey of Ownership Types and found very little that discusses the relationship between the two topics. The three closest papers I came across are the following, which curiously come from the same conference: Yang Zhao and John Boyland. A fundamental permission interpretation for ownership types. In Second IEEE/IFIP ...


6

Core calculi for Java typically take the classes-as-types approach. Two well-known examples are Featherweight Java and Classic Java.


5

What you are looking for are called "self types", and have been studied theoretically for ~20 years or so. For example, see Safe Type Checking in a Statically-Typed Object-Oriented Programming Language by Kim B. Bruce, in the 1993 POPL (Principles of Programming Languages), pp. 285-298. Off the top of my head, John Mitchell and Kathleen Fisher have also ...


4

Final Algebra semantics was introduced by Mitch Wand in his paper "Final Algebra Semantics and Data Type Extensions", see this freely available tech report: https://www.cs.indiana.edu/ftp/techreports/TR65.pdf . It does not mean final coalgebra semantics, which is a very different idea. The wrinkle is that the algebra is not final in the same category that ...


4

Bart Jacobs tackled this problem at one point. In his view, classes can be considered as coalgebras. Roughly, we have a polynomial endofunctor $F : \mathbf{Sets} \to \mathbf{Sets}$ which gives the class's type signature. A pair of a carrier set $X$ and an arrow $X \to FX$ is then used to "implement" the class. For example, consider a class representing ...


4

Perhaps you are looking for modules. For example, the following code uses OCaml's module system to define a signature for monoids and two implementations: module type Monoid = sig type t val identity : t val oper : t -> t -> t end module IntSum : Monoid = struct type t = int let identity = 0 let oper x y = x + y end module IntProd : ...


3

The answers to these questions vary with the specific OO language. Here are some fairly generic answers. Can methods contain free variables? In general yes. Are free variables statically-scoped? It's complicated. As a general rule (with many exceptions), most variables are lexically-scoped, except that the self reference (e.g., this in Java) is an ...


2

In Scala you can use parametric polymorphism for this, e.g. like so: trait A [ T ] { def f ( t : T ) : T def g ( t : T ) : T = t } class AImpl () extends A [ AImpl ] { def f ( t : AImpl ) : AImpl = t } (Traits are a generalisation of Java interfaces). This can be resolved at compile-time, although I don't know how the Scala compiler and the JVM ...


1

I took a brief look at the first paper you cite, and I think Max New's answer does have some relevance to it. The purpose of this answer is to explain how I think the 'finally tagless' stuff gets a bit confused itself about the idea. The paper starts with a simple algebraic signature for a language with literal numbers, addition and negation. It says that ...


Only top voted, non community-wiki answers of a minimum length are eligible