Platonic C# - Managing Referential Transparency through Unique Types

The idea of Platonic C# is to enforce referential transparency within the context of C#, by enforcing a set of rules around defaulting to immutability of data structures and requiring uniqueness of instances of mutable types.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Any other similar approaches?

Anyone aware of recent work being done with uniqueness type systems? On the surface, it seems like an effective way to patch referential transparency onto an imperative object-oriented language. I wonder if the stated rules are complete enough to enforce referential transparency and safety, and whether a static analyzer can enforce them sufficiently.

Capabilities for Uniqueness and Borrowing

There is a presentation from 2010 by by Philipp Haller and Martin Odersky: "Capabilities for Uniqueness
and Borrowing

The Pony language may have something similar. They have a paper: "Deny Capabilities for Safe, Fast Actors".


I appreciate you sharing the links. The Pony language concept of deny capabilities does seem related. For the record I have started submitting code to the repo that uses Roslyn to detected whether C# code is "Platonic", and I made some updates to the rules.

An interesting observation is that while pure methods are easily identified and classified, there are two types of non-referentially transparent methods (those with side-effects) that can still be considered Platonic. Those that update the "this" instance, and those that accept an argument of a type that is considered "immutable".

I'm not sure at this point what to call the two categories of effectful methods.

Commands, Queries, and Responsibilities

Recall that Command-query separation (CQS) was devised by Bertrand Meyer to segregate those methods that are idempotent and side-effect free from those that have side-effects.

There is also something called Command-Responsibility Separation (CRS) that I think was introduced by Vaughn Vernon in one of his books. That approach suggests that command methods should only modify the state of the target object and not have any side effects beyond it.

I think the 3rd category you mention: side-effects beyond the target object actually implies a 4th category of methods:

otherProxy Query?Proxy Command?

But if we take a step back and recall the Single Responsibility Principle (SRP) then the answer here would be: "Don't do that". If your language was able to enforce the SRP, what would that look like?

Great point.

Thanks for the table, and the pointer to Meyer and Vernon's work.

So in the proposed

So in the proposed terminology for Platonic C# we have two attributes:

[ImpureWrite] => updates (mutates) self
[ImpureEffect] => uses a type which can be mutated

As you suggest we could have a function that does neither (is Pure) and a function that does both.

Preventing a user from combining both in a single function is exactly what I was planning to do. I can see no ill-effect from it. If some-one wants to do both things, they have to make two separate method invocations. Which is probably a "good thing".