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

31–40 of 95 posts

Re: Exotic Programming Ideas, Part 3: Effect Systems

#31

Post by mpweiher »

akiselev wrote: post #29
patrec wrote: post #22

Earlier quoted context omitted.

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.

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…

And maybe Macros aren't the right kind of metaprogramming mechanism...

Re: Exotic Programming Ideas, Part 3: Effect Systems

#32

Post by Quekid5 »

skybrian wrote: post #28
AaronFriel wrote: post #21

Earlier quoted context omitted.

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 "tr…

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?

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.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#33

Post by shthrow »

skybrian wrote: post #28
AaronFriel wrote: post #21

Earlier quoted context omitted.

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 "tr…

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?

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.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#34

Post by Quekid5 »

skybrian wrote: post #30
lambda_obrien wrote: post #11

Earlier quoted context omitted.

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" an…

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…

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.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#35

Post by skybrian »

daanx wrote: post #14
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…

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.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#36

Post by kazinator »

patrec wrote: post #22
siraben wrote: post #10

Earlier quoted context omitted.

IMO implementing hygienic macros properly is one of the hardest tasks in programming languages, especially since variable capture can cause subtle bugs.

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.

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.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#37

Post by daanx »

skybrian wrote: post #35
daanx wrote: post #14

Earlier quoted context omitted.

(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…

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 f…

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).

Re: Exotic Programming Ideas, Part 3: Effect Systems

#38

Post by deckard1 »

patrec wrote: post #22
siraben wrote: post #10

Earlier quoted context omitted.

IMO implementing hygienic macros properly is one of the hardest tasks in programming languages, especially since variable capture can cause subtle bugs.

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.

> 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.

Re: Exotic Programming Ideas, Part 3: Effect Systems

#39

Post by lalaithion »

skybrian wrote: post #27
lalaithion wrote: post #25

Earlier quoted context omitted.

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/…

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. A…

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".

Re: Exotic Programming Ideas, Part 3: Effect Systems

#40

Post by opnitro »

skybrian wrote: post #35
daanx wrote: post #14

Earlier quoted context omitted.

(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…

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 f…

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)
Post reply on HN