[HN Gopher] Exotic Programming Ideas, Part 3: Effect Systems
___________________________________________________________________
Exotic Programming Ideas, Part 3: Effect Systems
Author : psibi
Score : 180 points
Date : 2020-11-22 15:56 UTC (7 hours ago)
(HTM) web link (www.stephendiehl.com)
(TXT) w3m dump (www.stephendiehl.com)
| siraben wrote:
| I highly recommend Oleg Kiselyov's talk titled "Having an
| Effect"[0] in which he talks about
|
| - purely functional model of computation and its pitfalls
|
| - Actor model, effectful programming with requests and responses
| and an implementation in Haskell.
|
| - denotational semantics and combining effects. Once you have a
| model of your language, what if you want to extend it by adding
| another effect? It forces you to rewrite the semantics (and thus
| any interpreter of your language) completely. Taking using the
| effects-as-requests viewpoint, only the request and handler for
| an effect needs to be added or changed, and the rest untouched.
| This is known as "stable denotations".
|
| - really evaluating what it means for an expression to be pure or
| effectful. Even variable reference should be considered an
| effect.
|
| - different scoping rules in lambda calculus can be expressed in
| terms of effects! Creating a dynamic closure is not effectful,
| though applying it usually is, OTOH, creating a lexical closure
| is effectful but using it is not.
|
| I think Haskell provides a good example of how a purely
| functional language can still express effectful computation.
| through a monadic interface. Though monad transformers have their
| share of problems when heavily nested (n^2 instances,
| performance), various effect system libraries are gaining
| traction.[2] On the bleeding edge of research there's languages
| like Frank[1] where the effect system is pervasive throughout the
| language.
|
| [0] https://www.youtube.com/watch?v=GhERMBT7u4w
|
| [1] https://github.com/frank-lang/frank
|
| [2] Implementing free monads from scratch,
| https://siraben.github.io/2020/02/20/free-monads.html
| chrisdone wrote:
| The recent Unison language uses the effect system described in
| the Frank language https://www.unisonweb.org/
| cultus wrote:
| Also see Oleg's "Effects without Monads: Non-determinism --
| Back to the Meta-Language"
|
| https://arxiv.org/abs/1905.06544
| merelydev wrote:
| Source:
| https://www.reddit.com/r/programming/comments/7wbtg/who_is_o...
| - Oleg eats lambdas for breakfast - The Y
| combinator fears Oleg - Oleg knows all the programs
| that halt on a Turing machine - Oleg is the guy
| that Chuck Norris goes to when he has an algorithm complexity
| question - Oleg reprograms his own DNA with Scheme
| macros - All of Oleg's Haskell programs are well-
| typed by definition - Oleg can read C++ compiler
| error messages. - Oleg built his house out of
| Prolog relations - Oleg speaks machine lanugage
| - Oleg once turned a zero into a one. - Emacs? Vi?
| Oleg wills files into existance - Oleg has the
| Haskell98 Report memorized. In Binary. In UTF-EBCDIC
| - Oleg can write unhygienic syntax-rules macros. -
| Sometimes Recursion gets confused when Oleg uses it.
| patrec wrote:
| > Oleg can write unhygienic syntax-rules macros.
|
| Not only can he do it, he even wrote a paper about it: https:
| //citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36...
| siraben wrote:
| IMO implementing hygienic macros properly is one of the
| hardest tasks in programming languages, especially since
| variable capture can cause subtle bugs.
| patrec wrote:
| Well, certainly no one seems to understand how e.g.
| syntax-case works. But my impression is that macro
| hygiene in itself is a solution looking for a problem.
| The key advantage e.g. racket's macro system has over
| clojure or common lisp is not hygiene but being
| sufficiently well structured and rich to allow proper
| tooling. Good error messages with accurate locations >>
| macro hygiene.
| kazinator wrote:
| Macro hygiene is a solution to the problem of functions
| being in the same namespace as variables, together with
| standard, oft-needed library functions having short names
| that are easily chosen as variable names.
| akiselev wrote:
| I think in theory they're orthogonal but in practice the
| two go together. It's all fine and dandy when you've got
| a restricted set of battle tested macros from a single
| library interacting in real world code, but it rapidly
| breaks down when you've got application authors of
| various skill sets all contributing their own macros
| because the dare not touch the ones that came before.
| Macro hygiene provides the equivalent of type level
| guarantees to metaprogramming scope.
| mpweiher wrote:
| And maybe Macros aren't the right kind of metaprogramming
| mechanism...
| deckard1 wrote:
| > macro hygiene in itself is a solution looking for a
| problem
|
| No. Unless you're not familiar with Lisp-1 vs Lisp-2. In
| Scheme, you would have to GENSYM every variable in
| addition to every function you call within a macro.
| Whereas in Common Lisp you just need to GENSYM the
| variables. That's the real reason Scheme doesn't use
| DEFMACRO.
|
| I'm not personally a fan of any hygienic macro system
| because learning a new language defeats the purpose and
| elegance of Lisp macros in the first place. But then
| again, outside of personal projects and academic
| exercises, no one should be using macros. Messing with
| fundamental semantics of a language while other
| developers are working on the same project will certainly
| make you a ton more enemies than friends. I still have a
| grudge against the guy that used Ruby's method_missing
| and I spent an entire day hunting down a method that
| didn't exist. When I figured it out, I don't think I've
| ever been so pissed at someone before.
| fiddlerwoaroof wrote:
| The problem with Ruby's method missing is mostly that
| Ruby development generally doesn't happen in an
| environment where discovering the existence of that
| method is easy. Macros are even better and tools like the
| slime macrostep expander make them relatively easy to
| deal with.
| The_rationalist wrote:
| Arrow Fx implement this idea for Kotlin -> https://arrow-
| kt.io/docs/fx/
| ianbicking wrote:
| 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).
| andrewflnr wrote:
| I don't even see anything essentially type-based in effect
| systems. You could totally have effect-style APIs in dynamic
| languages, they just wouldn't be tracked and checked up front.
| I expect this has already been done a few times in Scheme.
| marcosdumay wrote:
| > E.g., if your effect is writing to stdout, you could rewrite
| all those changes
|
| Could you? Once you write something into stdout, as far as your
| program knows it could already be sent across the world and
| turned into a set of bank transactions, or missiles fired.
| transfire wrote:
| I believe Kitten is another language exploring this area.
| PaulHoule wrote:
| "Non-termination is an Effect"
| SomeHacker44 wrote:
| ...that cannot be determined by the system (and must be
| specified by the user).
| daanx wrote:
| 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.
| daanx wrote:
| (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<h>
| 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)
| skybrian wrote:
| I'm wondering if you've found it useful in practice to
| distinguish between total and possibly-diverging functions?
|
| It seems like it's the sort of thing that's useful in
| something like Agda, where you use the existence of a
| function (without running it) to prove that its result
| exists. (The type is inhabited.) Or so I've read; I haven't
| used it.
|
| But if you're going to run the program, you typically want to
| know if a function will return promptly, and a total function
| could still spin for a million years calculating something,
| in a way that's indistinguishable in practice from diverging.
| opnitro wrote:
| I have found total checks in languages like idris helpful,
| but really only for catching small mistakes that I've made
| (for example, recursing on the original argument)
| daanx wrote:
| _In practice_ , I have not (yet) found many great use cases
| for the distinction in Koka. It is nice to have "total"
| functions, but "pure" (exceptions+divergence) is still a
| good thing (and what Haskell gives you). And like you say,
| in practice we can easily have functions that just take a
| long long time to compute.
|
| Still, it is a good extra check and I can see more use for
| the `div` effect for future verification tools where total
| functions can be used as a predicates (but non-terminating
| ones cannot).
| skybrian wrote:
| Good to know. At compile or verification time, it seems
| like you could get the same problem again, though? We
| want our compiles to finish promptly, and a slow, total
| predicate could hang.
|
| Which is to say, a possibly-diverging function seems okay
| to use even by a verification tool, so long as it
| finishes quickly in practice. Having some notion of
| analysis-time-safe predicates seems useful but it doesn't
| seem to map cleanly to being able to prove termination?
| tomp wrote:
| I never understood this one. I mean obviously a kind compiler
| should warn you against using while true { }
|
| and while i < 5 { 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.
| creata wrote:
| 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.
| aozgaa wrote:
| > 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
| klodolph wrote:
| There's some interesting research and ideas here, but it does
| seem like monads "ate everything for lunch" back in the late
| 1990s and 2000s when it comes to encoding effects, probably
| because monads are a bit more ergonomic (which seems like a weird
| thing to say, given the reputation monads have for being abstract
| nonsense). So effect systems didn't get as much research as
| everyone was interested in monads, and now that monads have dried
| up a bit as a field of research for encoding effects, I'm
| interested to see what other systems people invent.
| smegma2 wrote:
| I was curious about this function: fun addRefs(
| a : forall<h> ref<h,int>, b : forall<h> ref<h,int>
| ) : total () { a := 10; b := 20;
| return (!a + !b); }
|
| Why is it total instead of st<h>? Won't this have a side effect
| of setting the references?
| daanx wrote:
| Ah, I think Stephen meant to write the following:
| fun add-refs( a : ref<h,int>, b : ref<h,int> ) : st<h> int {
| a := 10 b := 20 (!a + !b) }
|
| where indeed the effect is `st<h>` 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 :-)
| skybrian wrote:
| 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
| declare effects that you might need (but currently don't use),
| just in case you will need them later.
|
| It's not that easy even to distinguish functions that can fail
| from those that can't, if you're trying to anticipate how a
| system will evolve. Something that's in-memory now might change
| to being done over the network later.
| lambda_obrien wrote:
| 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.
| skybrian wrote:
| Refactoring tools are nice so long as you are in a closed-
| world environment where you can see all the code and make
| whatever changes are needed. They don't help nearly as much
| in an open environment where there are many code owners and
| not all code is visible to you. When you publish a library, a
| refactoring tool isn't going to tell you everyone who uses
| your library, and you don't have permission to change the
| call sites anyway.
|
| The only thing for it is to push a new, incompatible version
| and other people will have to migrate. So you're pushing off
| the work onto them.
|
| I don't see how an effects system helps with this much? It
| might help you better understand how you painted yourself in
| a corner, but I don't see how it helps you get out of it.
| Quekid5 wrote:
| I mean... if you're fixing a broken API, you're going to
| have to bite the bullet _either way_ -- papering over it
| isn 't going to fix anything... it just hides the problems.
|
| With a type system which understands effects, at least the
| compiler can give you very accurate help in fixing call
| sites.
| skybrian wrote:
| It does help by telling you what's wrong. But in a way,
| increased precision makes the problem worse.
|
| Suppose you have have a language with two categories of
| functions, those that can fail (returning an error) and
| those that can't.
|
| It's nice that within the "functions that can fail"
| category, you don't have to worry about what kind of
| error it might be. Error propagation can happen in a
| generic way. Adding a new kind of error doesn't change
| any API's.
|
| If instead, you have different kinds of errors and
| _declare_ them everywhere, you end up with a situation
| like Java 's checked exceptions. The problem is being
| _too precise_ , which doesn't leave room for changes
| later.
|
| Similarly, we could be very generic about effects. Maybe
| we could just say "this function has effects" and treat
| them all the same? By not being precise about what the
| effects might be, we aren't promising too much, so we
| allow ourselves room for change.
|
| The downside is that the caller has to assume any effect
| is possible. This is a fundamental tradeoff between
| caller and callee convenience. You need to be specific
| enough for the caller to be able to deal effectively with
| the effects you declare, but not too specific, or you're
| painting yourself in a corner.
| jahewson wrote:
| I always found IOException in Java to suffer from this problem.
| AaronFriel wrote:
| A properly done effects system with type-level annotation of
| the "color" of functions helps this, rather than hurts as you
| might surmise.
|
| Take for example logging or tracing - we almost always in a
| modern backend application want an ambient trace or span ID and
| a log destination. What we don't want is to have to add those
| as parameters to _every function_.
|
| So we want to paint these functions with the "logger" and
| "traced" colors, which respectively allow a function to send
| messages to an ambient logger via log(message: str) and to get
| the current trace context via getTraceContext() each with no
| other arguments.
|
| The compiler will tell us if we call these functions from an
| unlogged, untraced function, so at a very high level - say at
| the RPC request level, we paint them early on. In Haskell we
| might even be able to do something like
| handleReq req = withTraceSpan (...) .
| withLogging (...) $ handleReqInner req
|
| Where handleReqInner requires these "colors".
|
| Having too many effect handlers is never a problem either - you
| can always call an untraced function from a traced function.
| The "trace" effect handler just falls off at that call. Or in
| other words: you can always call a function whose colors are a
| subset of the call-site's.
|
| This is somewhat a foreign concept to people who haven't worked
| with type systems like this and whose only concept of the color
| of function is purely binary - either async or not. In a good
| typed effect system, the compiler will assist you in knowing
| where you're missing an effect handler, and it will be easy to
| add those effect handlers sufficiently far from the business
| logic that you won't have to think about it.
| skybrian wrote:
| You're saying it's not a problem, but let's say you didn't
| think ahead and want to add tracing later, and there are many
| intermediate function calls between top level and the place
| where you want to trace. You still have to change every
| function signature to add the colors, right?
| AaronFriel wrote:
| In a language and type system where the compiler infers all
| of the intermediate types, no.
|
| The way effect systems are typically added to languages
| without this level of type system is that the effect
| "fails". Like making a database call in Python without
| "with use_database(...):" that provides the database
| context. In those languages and with those effects,
| typically the default behavior is the effect's methods are
| always available, but may either be a no-op/return a
| nullish value or throw an exception.
|
| As an example, the way tracing works on Node.js is that you
| have to explicitly declare a span (or use a plugin for a
| framework which does that for you) and inside that span,
| you can do something like getSpanId() and it'll return a
| value. Outside a span, it returns null.
|
| The worst case scenario is you have a language and
| framework where it's both difficult to annotate the types
| and difficult to provide some ambient context. In those
| cases, you're back to (essentially) passing your trace
| span, your logger, etc as arguments to every function
| again. Not ideal.
| dan-robertson wrote:
| In every language I've used where types can be inferred,
| almost everyone writes down the types of their top level
| functions (or at least the functions that are exposed to
| clients). I don't think this is really a good counter
| argument.
|
| The only ways I know of to reliably make this kind of
| change (or just about any nontrivial change) to an
| interface are increasing version numbers and letting
| clients suffer or having a monorepo and fixing all the
| clients yourself
| Quekid5 wrote:
| Yes, you do... which is as it should be. What else would
| you expect?
|
| If a function needs capability X then it must require that
| capability. Simple as that.
| shthrow wrote:
| No, think of it like checked exceptions, you only need to
| handle the effect _at most once_ before it reaches the top
| (it's up to you to let it keep getting passed up or handle
| it immediately), otherwise the compiler will automatically
| infer the effect types in the layers between.
| skybrian wrote:
| Okay, so type _inference_ is the vital feature here.
|
| It can help in a closed code base. In an open code base,
| you could inadvertently change a public API, breaking
| callers that are unknown to you, if the type signature of
| something public is inferred.
| lalaithion wrote:
| The "what color is my function" problem is insurmountable in
| Javascript, because the runtime does not allow you to call an
| async function from a non-async one. However, most effects
| aren't like this. If you say "this function needs randomness"
| then you can create a pure PRNG and call the function with the
| PRNG providing randomness. If you say "this function needs
| logging" you can tell it to log to a string and parse/ignore
| the string. If it throws an exception, you can catch the
| exception. Haskell even provides `unsafePerformIO`, which lets
| you run arbitrary computations as if they were pure.
| skybrian wrote:
| There is the specific issue with async functions, but that's
| only one example of a general problem, what I'm calling
| "function coloring." Workarounds are often possible, but they
| are still workarounds and often result in bad code.
|
| We've been there with Java. An API takes a Runnable. You need
| to do something that does IO, so you catch the exception...
| and then what? Log and suppress it? This is how bad code
| happens. At best you get chained exceptions.
|
| With Callable, they got smarter and declared it to throw
| Exception, which means it can only be easily propagated by
| other methods that declare they throw Exception. So it's a
| viral declaration, unless you engage in workarounds like
| exception wrapping.
|
| You don't need an effect system for this to happen, though.
| In Go, you don't have the problem with different kinds of
| errors, but you can still classify functions into two
| categories: those that may return an error, and those that
| (apparently) always succeed. If you need to fix the API, you
| might end up with lots of refactoring [1].
|
| Mistakes at the API level can be hard to fix without touching
| lots of API's. This is unsolvable in general. The only way to
| avoid workarounds (via escape hatches or by mocking things
| out) is to standardize whatever you can so it works together.
|
| [1] https://www.dolthub.com/blog/2020-11-16-panics-to-errors/
| lalaithion wrote:
| Nothing prevents having a type system capable of dealing
| with those problems. Yes, Java and Golang make this
| difficult, but if you have a language that supports it,
| there's nothing which prevents writing an API that says
| "Whatever the effects of the Callable you passed me are, I
| also perform those effects".
| skybrian wrote:
| Introducing generic types doesn't make the function-
| coloring problem go away.
|
| Now, instead of having a single function that has some
| effects, you have a family of closely-related functions,
| each with different effects. These functions are
| incompatible with each other. The function-coloring
| problem has gotten worse! :)
|
| (Generic types are still useful though.)
| no_wizard wrote:
| I think the reactive/rx/observer patter might be an
| acceptable solution around the _what color is my function_
| problem and it tends to be very popular with the functional
| programming wing of the JS community from what I've seen.
|
| Never understood why the browser didn't ship a full access to
| something like an EventEmitter. Since you can dispatch events
| on window document DOM elements etc seems like being able to
| subscribe to events in a more arbitrary fashion that worked
| in parallel to the other events would have been useful and
| solved callback hell all the same
___________________________________________________________________
(page generated 2020-11-22 23:00 UTC)