[marcosdumay]

> this could only happen if you passed a `Network` object to the logger

Yeah, this is not only an effects type system, it's a static effects type system.

[justinpombrio]

No it's not. I'd guess you're imagining a type signature like this one?

    void effect:Network my_function_to_connect_to_server() {
        ...
    }

I mean a type signature like this one:

    void my_function_to_connect_to_server(Network network) {
        ...
    }

Where there's absolutely nothing special about the Network type, except that (i) it has no constructor, and (ii) nothing in the Java language lets you talk to a network without it. All of this is expressible with Java's type system today.

[marcosdumay]

> void my_function_to_connect_to_server(Network network)

See how there's the Network right there on the type?

[justinpombrio]

That's an ordinary argument type. Like:

    void my_function_to_connect_to_server(
        Network network,
        int port,
        String server_name
    )

It's not categorically different than the other arguments, and doesn't require an effect type system.

At this point I'm not sure if you're misunderstanding what I'm proposing, or if you don't know what an effect system is. If you care to communicate, you'll need to say something more substantial. Walk me through what you're trying to say.

[marcosdumay]

Make it generic, with some kind of Resource interface that Network is one of the implementations¹, and you get a dynamic effect system.

But that thing you wrote is a static effect system. Having a singleton that you need to carry with the type doesn't make it not part of the type system.

1 - Or actually use Resource as a class. But Java wouldn't do this.

[yencabulator]

I think you're talking about what power a type system needs to say that this function doesn't have undesirable side effects, while Justin is saying if you can't just "import std.net" and access the network by side effects (and can't make raw syscalls either, or poke around in raw memory), and nothing hands you a Network value, a plain old boring type system is enough.

[justinpombrio]

Thank you for the clarity.

> But that thing you wrote is a static effect system.

The thing I wrote is expressible in Java's type system as it is today. So you're saying that Java has a static effect system?