Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Exotic Programming Ideas, Part 3: Effect Systems

stephendiehl.com

Post reply on HN
Print view View original

11–20 of 95 posts

Re: Exotic Programming Ideas, Part 3: Effect Systems

#11

Post by lambda_obrien »

skybrian wrote: post #6

I expect that, as with any other type system extension, the more granular your effects are, the more likely you are to run into a “what color is my function” problem. If you have a public API that declares certain effects, you’re stuck with those unless you break backward compatibility. In a practical system, when writing a library and especially an abstract interface, you’d want to be careful what you promise and de…

An effects system like this is more about controlling your own code and allowing for switching off implementations easily versus declaring what effects it has. Your declaration of effects on your function is saying, for example, "I need to output some text," and then in the caller of that function you have to do some action to "consume" that effect. For instance, your example might be an effect called "WriteState" and then you could call that function in a small unit test with a thin layer over a Map, in dev you could call it with a local sqlite db, and in prod you'd call it with your postgres or whatever. Each implementation shares a common interface, but does something different with the data. If you were writing a library, you'd give your public API as the base monad of your library, or as IO maybe, or even give a pure API. You should be dealing with the possible failures under that base context and then the user doesn't need to know about the inner failures.

The effects system effectively acts as an abstraction for some side effect, like an interface, and gets ride of a lot of the boilerplate code needed for mtl or custom transformer stacks.

Also, in strict typing it's pretty easy to refactor with modern linters and such, it actually makes refactoring an API change delightfully simple, just get rid of the red squiggle lines telling you you types are wrong.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#12

Post by creata »

tomp wrote: post #9
PaulHoule wrote: post #2

"Non-termination is an Effect"

I never understood this one. I mean obviously a kind compiler should warn you against using while true { } and while i but in general, I don’t find distinction between “this infinite loop terminates” (e.g. an event loop) and “this code obviously terminates but not in the lifetime of this universe” (e.g. computing Ackermann(5)) to be that useful.

It's primarily useful for theorem proving, where a nonterminating argument corresponds to circular or otherwise unfounded reasoning.

It's also useful because, in practice, we don't accidentally write code that "obviously terminates but not in the lifetime of this universe" as often as we accidentally write nonterminating code, so a lot of mistakes can still be caught by termination checking.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#14

Post by daanx »

PaulHoule wrote: post #2

"Non-termination is an Effect"

(Daan here, creator of [Koka](https://github.com/koka-lang/koka)

This is an interesting point and comes down to the question -- what is an effect really? I argue that effect types tell you the type signature of the mathematical function that models your program (the denotational semantics). For example, the function

  fun sqr(x : int) : total int { x*x }
has no effect at all. The math function that gives semantics to `sqr` would have a type signature that can be directly derived from the effect type:

  [[int -> total int]]  = Z -> Z
(with Z the set of integers). Now, for a function that raises an exception, it would be:

  [[int -> exn int]] = Z -> (Z + 1)
That is, either an integer (Z), or (+), a unit value (1) if an exception is raised. Similarly, a function that modifies a global heap h, would look like:

  [[int -> st int]] =  (H,Z) -> (H,Z)
that is, it takes an initial heap H (besides the integer) and returns an updated heap with the result.

Now, non-termination as an effect makes sense: a function like "turing-machine" may diverge, so:

  [[int -> div int]] = Z -> Z_\bot
That is, its mathematical result is the set of integers (Z) together with an injected bottom value that represents non-termination. (note: We don't use "Z + \bot" here since we cannot distinguish if a function is not terminating or not (in contrast to exceptions)).

In a language like Haskell every value may not terminate or cause an exception -- that is a value `x :: Int` really has type `Int_\bot`, and we cannot replace for example `x*0` with `0` in Haskell.

Note that in almost all other languages, the semantic function is very complex with a global heap etc, any function `[[int -> int]]` becomes something like `(H,Z_32) -> (H,(Z_32 + 1))_\bot`. This is the essence of why it much harder for compilers and humans to reason about such functions (and why effect types can really help both programmers and compilers to do effective local reasoning)

Re: Exotic Programming Ideas, Part 3: Effect Systems

#15

Post by jahewson »

skybrian wrote: post #6

I expect that, as with any other type system extension, the more granular your effects are, the more likely you are to run into a “what color is my function” problem. If you have a public API that declares certain effects, you’re stuck with those unless you break backward compatibility. In a practical system, when writing a library and especially an abstract interface, you’d want to be careful what you promise and de…

I always found IOException in Java to suffer from this problem.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#17

Post by daanx »

smegma2 wrote: post #16

I was curious about this function: fun addRefs( a : forall ref , b : forall ref ) : total () { a := 10; b := 20; return (!a + !b); } Why is it total instead of st ? Won't this have a side effect of setting the references?

Ah, I think Stephen meant to write the following:

  fun add-refs( a : ref, b : ref ) : st int {
    a := 10
    b := 20
    (!a + !b)
  }
where indeed the effect is `st` as the updates are observable. How the function was written before, the two arguments use a "rank-2" polymorphic type and the heaps are fully abstract -- in that case it would be unobservable but you cannot create such values :-)

Re: Exotic Programming Ideas, Part 3: Effect Systems

#18

Post by ianbicking »

I've had this idea of "dynamic returns" (akin to dynamic scope) in my head for a while. Reading this, it feels like a dynamically typed companion to effect systems.

The idea of a dynamic return is just to give a formal way to accumulate things during a set of function calls, without having every function to be aware of what might be happening. In Python context managers are often used for this (e.g., contextlib.redirect_stdout to capture stdout), but thinking about it as another kind of return value instead of "capturing" would be an improvement IMHO. (You have to "capture" when hardcoded imperative code later needs to be retrofitted, but as it is retrofitting is all we have.)

But dynamic returns aren't quite like an effect system unless you also create something more-or-less like a transaction or a changeset. We usually think about transactions as simply a way to rollback in case of an error, but as a changeset there's all kinds of interesting auditing and logging and debugging possibilities. E.g., if your effect is writing to stdout, you could rewrite all those changes (e.g., apply a filter, or add a text prefix to each line).

Re: Exotic Programming Ideas, Part 3: Effect Systems

#19

Post by daanx »

SomeHacker44 wrote: post #8
PaulHoule wrote: post #2

"Non-termination is an Effect"

...that cannot be determined by the system (and must be specified by the user).

Just to add to this: Koka can (obviously :-)) not always determine if a function will terminate or not so it generally adds a `div` effect whenever there is the possibility of infinite recursion.

However, since most data types in Koka are inductive, any recursion over such inductive data types are still inferred to be always terminating.

In practice, it looks like about 70% of a typical program can usually be `total`, with 20% being `pure` (which is exceptions + divergence as in Haskell), and the final 10% being arbitrary side effects in the `io` effect.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#20

Post by aozgaa »

> As far as I can tell no one uses this language [Koka] for anything, however it is downloadable and quite usable to explore these ideas.

I believe the typesetting tool Madoko[1] is implemented in Koka, though in fairness Daan Leijen developed both Koka and Madoko.

[1] https://github.com/koka-lang/madoko

Post reply on HN