Mastodawn

I've been thinking about the weird status referential transparency (RT onwards) has in some FP communities - where the statement "this loses RT" is seen by many as a slam dunk argument that cannot be refuted.

This is something I'm particularly interested in because I've been looking at modern solutions for direct-style - which loses RT, and that's pretty much where the discussion ends, most of the time. If it's not RT, it's not worth considering.

So I'd like to share my thoughts on RT, why I don't feel it deserves its sacrosanct status, in the hope of learning a bit more. Why is something not worth considering if it's not RT?

The rest of this thread is probably going to sound like I'm stating facts - I'm not. Everything from this point is opinions and, basically, me lining up my thoughts to try them out with real people - you, hopefully, unless you're some GenAI crawler, in which case you can sod off.

Show thread

Nicolas Rinaudo Jun 3

There are, to the best of my knowledge, two main advantages to RT:
- it lets one use the substitution model, which is really a fancy way of saying "you can swap an expression and its name".
- it's easier to reason about or, I think equivalently, it enables local reasoning.

First, before I dig into these, I'd quite like to know if I'm missing anything / mis-representing anything. Please let know if I am!

Show thread

Nicolas Rinaudo Jun 3

"RT enables the substition model". This basically tells us that the two following programs are equivalent:

P1:
```
f e e
```

P2:
```
let e2 = e in
f e2 e2
```

This is undeniably nice - it's a cool little refactoring we can confidently perform if we know `e` is RT, and that works for any `f`.

But it's also just that: a cool refactoring. A little cognitive load off our shoulders, because in a context where RT is not guaranteed, we need to think a little to decide whether it's a valid transformation to make - the compiler won't catch it for us if it's not.

All other things being equal, this is a nice property to have. But not, I think, at any cost.

Show thread

Nicolas Rinaudo Jun 3

"Easier to reason about" is a little more nebulous and ill defined. I understand it to mean that with RT, you don't need to build and maintain such a complex mental model of all the states in your program and their potential interactions. This has a massive cognitive cost, and we often get it subtly wrong and write really painful bugs to figure out.

This is an important tenet of the functional style: if you favour immutability, you have much less state to consider, and life is generally better. I can quite happily agree with this perspective.

Show thread

Nicolas Rinaudo Jun 3

I don't think it applies in the context of this thread, though - when comparing direct-style to alternatives. And, to be quite precise, I'm comparing it to monadic-style here, which I mostly use to mean `IO`. Yes, that is a bold simplification to make, but one which I think is correct at least in the communities I'm part of.

There's quite an important subtlety here, one which I think is often overlooked: `IO` makes effectful computation *declarations* RT. Not their execution.

So yes, an `IO` that prints something to stdout is RT. And you can compose it with other `IO`s to build a large program, and the *building* of that large program is RT.

But the complex state interactions still happen at runtime. Your `IO`s, when executed, mutate state - that's the entire point, isn't it? You print to stdout and connect to databases and read files and... and all these stateful actions may interact in weird and wonderful ways, and ultimately produce a useful result. Because without the ability to mutate some state, your programs might compute the most beautiful values in the universe in the most elegant way possible, but they wouldn't be able to communicate them to you.

Show thread

Nicolas Rinaudo Jun 3

And so I actually don't think "easier to reason about" applies in the context of direct-style vs monadic-style.

We're still left with the substitution model, which is definitely nice, but I don't think quite nice enough to justify discarding direct-style out of hand.

I am not, however, saying "RT is not all it's cracked up to be so let's ditch monadic-style". My point is more nuanced: RT obtained via monads is nice, but it has a cost. Is the cost worth it? And I don't think there's a universal answer to this question. My opinion is that no, it's not worth it in most scenarios. But that is really just an opinion, and one which I may very well revisit and disavow in the future.

Show thread

noelwelsh

@NicolasRinaudo

A few thoughts:

There are several definitions of "direct-style". Ox calls itself direct-style, but doesn't have a separation between description and action. This means it isn't compositional in a useful sense (alternatively, you have to be more careful than you should to make it compositional). Taking the first example from the home page, you cannot refactor

```scala
def computation1: Int = { sleep(2.seconds); 1 }
def computation2: String = { sleep(1.second); "2" }
val result1: (Int, String) = par(computation1, computation2)
```

```scala
def computation1: Int = { sleep(2.seconds); 1 }
def computation2: String = { sleep(1.second); "2" }

val c1 = computation1
val c2 = computation2
val result1: (Int, String) = par(c1, c2)
```

and have it work as you'd expect under RT. I think this loss of local reasoning is actually very important. It's really fricking hard to ensure you don't run `Futures` (or Ox computations; they have the same model of executing immediately) at the wrong time in a large code base.

The corollary of this is that I think you undervalue the ability to compose `IO`. When you write code to, say, handle errors or run stuff in parallel or race multiple fibers, you can be sure it will actually happen the way you write it, not that some bullshit like "oh this already ran before we got here" will change the semantics.

OTOH, there are other formulations of direct-style where the unit of composition changes from `A => F[B]` (i.e. monadic) to `F[A] => B` (direct-style, where `F` is required "capabilities"). Now that effects have an explicit representation in the type system you can still leverage types to help you (cf Ox where a computation has no types AFAIK) and it's still composable because nothing runs until you provide the capabilities.

Show thread

Nicolas Rinaudo Jun 3

@noelwelsh
There are a few things I'd like to pick at here but are probably not worth getting into - I would nitpick that "direct-style" doesn't have multiple definitions (whether it has one is up for debate, but certainly not more than one), but that there are multiple ways of achieving it, for example. But it's not all that interesting.

I'll try to (heavily) rephrase your point to make sure I get it - and if I do, I think you've hit the nail on the head and there's a longer, quite interesting discussion to be had.

Monadic style forces a very strong separation between operations ("effectful computations") and values (everything else). You cannot possibly find yourself running an operation without meaning to, because that's a compile error. For example:

```
val line: IO[String] = ???

line ++ line
```

The compiler forces you to make it very clear whether you want to run `line` once or twice here.

Direct style weakens that separation. It still exists, but running a computation when you don't mean to is no longer a compile error.
For example (using capabilities because I need to use something):

```
val line: Tty ?=> String = ???

line ++ line
```

The compiler understands this to mean you want to run `line` twice.

This is quite related to my point on RT. In the direct-style version, `line` is not RT, and you, as a developer, need to keep track of that.

Ox doesn't give you this information at the type level.

Capabilities do, but they also make no syntactic difference between running an operation or reading a value. Better, but not great.

Some languages have a clear syntax for running an operation. Eff, for example, has you go `perform YourOperation`.

There's a fairly large design space, and not all languages are equal. But I think that in Eff for example, you lose the RT aspect, and it doesn't really matter for the properties we care about (ease of reasoning in particular).

Show thread

ppurang Jun 3

@NicolasRinaudo @noelwelsh to me the main issue was always RT given non-determinism and while researching this a bit, also found about definiteness and unfoldability. Maybe this detracts or perhaps it is absolutely pertinent to this discussion: https://www.itu.dk/~sestoft/papers/SondergaardSestoft1990.pdf

Show thread

Nicolas Rinaudo Jun 3

@ppurang @noelwelsh oh GREAT, yet another paper to add to the pile.

You're probably wondering if I'm being sarcastic, and honestly, I don't know myself. This looks like quite an interesting read, but the list is already soooooo long...

Thank you though, I appreciate the link!

Show thread

noelwelsh Jun 3

@NicolasRinaudo

On direct-style, yes I was being imprecise. I meant direct-style effect systems, aka effect handlers or algebraic effects (which all mean slightly different things but are often used to refer to the same broad area).

> Capabilities do, but they also make no syntactic difference between running an operation or reading a value.

Isn't this just a quirk of Scala's implementation using context functions? In Effekt I think you need to use the `do` keyword to use a capability.

Show thread

Nicolas Rinaudo Jun 3

@noelwelsh it is a quirk of capabilities, absolutely. But also, I think, a poor design decision. I would prefer syntax that makes the difference between "being" and "doing" clear, and Scala decided to hide it.

It's not even only due to context functions. For example, in the following code, how many times is `readLine` called?

```
foo(readLine())
```

There's no way to know unless you check the type signature of `foo`. Does it take a `line: String` or a `line: => String` ?