Flix polymorphic effects

(The older thread has being closed so I've written a new one).

A new language implemented in Scala for the JavaVM is named Flix: https://flix.dev/

It has three interesting features, one of the three is that its type system tracks the effects of functions (I think for now it only tracks function purity, but there's interest to track other effects too later). Pure functions aren't a subtype of impure functions (invariant), so to a function that accepts an impure function as argument you can't give a pure function. The "Pure" annotation for functions is the default and you can omit it. An usage example of such polymorphic effects:

/// Assume we have some pure and impure functions: def inc1(x: Int): Int & Pure = x + 1 def inc2(x: Int): Int & Impure = Console.printLine("Hello"); x + 1

/// We can write functions that expect pure or impure functions: def twice1(f: Int -> Int & Pure, x: Int): Int & Pure = f(f(x)) def twice2(f: Int -> Int & Impure, x: Int): Int & Impure = f(f(x))

/// But we can also write effect polymorphic functions: def twice3(f: Int -> Int & e, x: Int): Int & e = f(f(x))

/// We can use twice3 with both pure and impure functions: def main(): Int & Impure = twice3(inc1, 0) + twice3(inc2, 0)

The explanation of how such polymorphic effects work:

The & symbol is used to attach an effect to the signature of a function. Such syntax is not beautiful, in my opinion, but it works. An example usage of such polymorphic effects to implement a map:

def map(f: a -> b & e, xs: List [a]): List [b] & e = ...

A more complex example of polymorphic effects to implement an >> operator that performs function composition, it specifies that >> is impure if at least one of the two functions is impure (in this system Pure equals to a true boolean value, and Impure is a false value):

def >>(f: a -> b & e1, g: b -> c & e2): a -> c & (e1 and e2) = x -> g(f(x))

But in Flix you can do even bette, this specifies that at most one of the two input functions is impure:

def mapCompose(f: a -> b & e1, g: b -> c & (not e1 or e2), l: List [a]): List [c] & (e1 and e2) = ...

All this stuff is orthogonal to the current Rust type system, so I think it can be added. In practice it can't be added because it's a breaking change because on default functions must be pure. Rust used to have the "pure" annotation, but it was removed because it was implemented naively. A polymorphic effects design similar to Flix is more useful and reasonable. Still, I am not sure why/how this feature could (even in theory) improve the practice of Rust programming.

From my older thread about the same topic:

At this point, the annotation becomes redundant,<

I have no proof of this. I think coding in Flix for few years will answer this.

1 Like

Alright, it sounds like it's possible, but why do we want this, what is the motivation?

Not sure if it's worth the effort for Rust, but it seems this could be used to distignuish between (C++) consteval, constexpr and constinit in a more elegant way.

Distinguishing between Pure and Impure could be used to decide whether the results of a passed-in closure can be memoized or not.

There is a lot of motivation, actually. We could avoid a whole layer of problems if we had an effect system. Reasons are simple: we principally have three ways of involving side effects: using statics, doing syscalls and calling effectful functions - everything else is, actually, pure (there no another way of getting information from environment in scope of function).

Abstracting over above (e.g. do we do syscalls? do we use statics, etc.) instantly enables sound CTFE. Allowing functions to be polymorphic over both performed syscalls and used statics enables a new level of abstractions in API.

Even more can be achieved if we allow effects to include each other: filesystem includes file_open, which means that any function which has a file_open effect also has a filesystem effect, but not vice versa.

The most interesting case is data transmission via effects, as in Effekt Language, this is our Try (without from conversion, and with ! resume type), Generator, async (which we could implement via such effects). However, all of these features have their specialized and nearly perfect designs now, so we don't have much motivation besides better APIs.

And the drawback of such system is that everything have to somehow be resumed on data effects - this turns everything into classic coroutines which raise a lot of questions.

2 Likes

I visited previous threads. Syntax of such a feature is definitely important, also we now have backward compatibility hazards, so if it will be added someday, we should avoid requiring any bounds on existing fn's - this way we cannot enforce anything, due to that our functions currently are impure in all possible ways: they can do any syscalls, use any statics and invoke assembly. We only can invent some mechanism to forbid parts of the impurity, like "no access to statics (which are not freeze or mut)" or "no inline assembly", etc. Unsafe should allow to break this guarantees, but to certain degree.

How is that different from const fn, and how is const fn considered unsound?

Statics are only relevant when they are mutable, which they basically shouldn't ever be (I've recently seen an idea for deprecating static mut, because there is always a better alternative). As for syscalls, you still didn't provide a specific use case, only a very abstract argument.

Sure, abstracting over stuff can be useful. But since effects add a completely new dimension to the type system, this should not be taken lightly.

E.g. in Swift, exception handling is effectful, and that design makes life a lot difficult, for basically no return. Developers have to annotate every higher-order function with rethrows if they don't want to unintentionally disallow calling it with a throwing or non-throwing functional argument. At this point, it becomes redundant, and an annoying thing to remember, that proliferates through each and every functional-style API.

Doing the equivalent with syscalls would be a similarly massive pain. Want a &mut io::Writer? Good luck using it with File if the author of the API forgot to declare that it must also allow the write syscall.

Hi there! :slight_smile: I no less than love your write up and I do believe effects are an extremely lucrative opportunity for development of programming languages.

However isn't this view of Rust a bit too optimistic? An fn using &mut/Cell to modify an argument is having an effect. Isn't it very difficult to precisely capture in a type system?

Imagine I took fn foo() -> S {} where S is a struct and did RVO manually: fn foo(retBuf : &mut ...) {} It's a shame this fn is now impure since it almost didn't change at all! I have also lost my ability to describe its behavior via it's type in sufficient detail.. Maybe retBuf was uninit before but is definitely init after foo has returned. Doing fn foo(retBuf : &mut Option<S>) is a waste, there's no need to pass that option tag around nor to check it after foo has returned.

Now imagine an fn modified a struct reachable from one of its arguments after traversing 5-6 box and/or & pointers... I wish this effect could be described by fn type more precisely than just "modifies something somewhere and is thus impure"..

Hmm... wouldn't there be a way to mitigate this somewhat at language design level? Say automatically assume fn f(g : Fn..) to have all the same effects as g unless the author of f has used a special syntax to declare they are not "passed through" from g to f? Smth like fn f(g : Fn..) no_throw_from(g) {.. I'm talking of blocking at fn signature level not implementation of course.

It's true that g can be buried somewhere deeper within the structs passed as arguments to f. I'm thinking along the lines of "if the compiler can 'see' an effectful function anywhere at all in arguments of fn foo it automatically 'passes through' the effects, unless the author of fn foo has taken effort to block them in foo's signature".

1 Like

I hope so, although I haven't though much about how. The reason for that is that I've barely seen anything else in the wild, other than exception handling, that would in practice benefit from tracking effects, and at that point it feels like we're trying to solve a problem that we shouldn't even have had.

This is an interesting idea, I'd be curious how much locality the code would lose though. The immediate naive implementation would, I think at first glance, have the same problem as generic #[derive] has today: just because a function or function type is in the parameter list, it doesn't mean that function is going to be called at that point (just like how having a generic type parameter in the parameter list doesn't mean that the outer type contains the inner, generic one as a member).

1 Like

I edited later.. my idea was to suppress effects "pass-through" at fn signature level; so code locality should not suffer.

Just to clarify you're saying Result is generally sufficient and exceptions can be avoided, right?

Side note: the alternatives include static with interior mutability. Without that, removing static mut would not be a serious proposal. So this really isn't relevant to this discussion.

I've seen at least a few libraries already that assume purity GitHub - nikomatsakis/mutable: Tinkering with a more ergonomic cell abstraction and GitHub - salsa-rs/salsa: A generic framework for on-demand, incrementalized computation. Inspired by adapton, glimmer, and rustc's query system.

from the README of the first,

"Pure" operations

A key assumption of the library is that operations like Clone, Hash, and Eq are, in practice, "pure" -- meaning that they do not mutate any mutable cells. We can't actually know that this is true, however, so we enforce the constraint with a light-weight dynamic check. Thus, if you write a Clone impl which mutates the data in one of the types from this library (e.g., a Mut<T> or MutVec<T> ), you will get panics. Reading data from a Mut<T> etc should be fine though.

Yes, exactly.

Isn't Rust is a bit ironically conflicted?.. Both Result and catch_unwind.. :slight_smile:

This talk from RustConf 2020 helps paint the difference here: https://youtu.be/rAF8mLI0naQ

Result is for any error that could reasonably ever be delt with (by something other than halting the program/thread/task and retrying). panic! is for unrecoverable errors, typically programmer error/invalid state, where execution cannot reasonably be continued.

catch_unwind isn't a way to recover from panic! errors. It's a way to discard panic! errors and allowing you to try again, without taking down the hole process down with you.

1 Like

... and an effect handler if we have ever seen one :slight_smile:

No. catch_unwind is not meant for regular error handling. It's a low-level, last resort utility for when you must absolutely catch a panic. Result is always preferred over panicking and catching.

1 Like

So Flix doesn't have mutable variables? That certainly removes one effect that would be abundantly plentiful in Rust

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.