Comment by djha-skin | Hacker News Reader

Comment by djha-skin | Hacker News Reader

> Koka tracks the (side) effects of every function in its type, where pure and effectful computations are distinguished. The precise effect typing gives Koka rock-solid semantics backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers.

Pretty comical to hear the words "easy to reason about" and "category theory" in the same sentence.

With apologies to the Haskellers, any time "category theory" is mentioned I feel myself shying away, prior experience teaching me that those words mean "you will spend the majority of your time working around the type system "; and, "we have more data types than individual bits of data that those types describe".

A little type system goes a long way, and there's such a thing as too much in my opinion.

I was initially interested because of algebraic effects in the language because I'm told they're basically the same as common lisp conditions. I really liked learning about conditions and I wish they were in more languages. I must confess I am less interested now.

Category theory is not the headline news here, it's safety without sacrificing performance by using a new technique to compile to binaries without a runtime or garbage collector, with potentially better deallocation performance than Rust, and functional-looking code like `array.map(func)` which performs as fast as a for-loop thanks to advanced analysis.

thanks for this, it wasn't immediately obvious to me why the headline example was traversing a list but doing that fast without GC is cool

So this means we have benefits of Rust but in a nicer, functional syntax?

Yes, essentially. Theoretically it could outperform Rust since it has aggressive local reuse of to-be-freed memory. Several papers have shown that it gets close to or outperforms C in some benchmarks. Whether this holds in practice is up for debate, but if you don't have to annotate lifetimes and don't have to manually manage memory, are you really going to care if you are 5% slower than C? There is a lot of performance optimizations still available for Koka to target as well. So far they've just taken the lowest hanging fruit (memory management).

How does it achieve better deallocation performance?

They have created a new precise reference-counting algorithm, called Perceus: https://www.microsoft.com/en-us/research/uploads/prod/2020/1...

Its innovation (they claim) is that it deallocates objects immediately as soon as it can prove that the object is not referenced any more. Not at the end of a lexical scope, like C++ smart pointers and Rust, but immediately after the last use of the object.

Interestingly, in Rust, we thought about doing this. "early drop" was the term folks talked about https://github.com/rust-lang/rfcs/pull/239

One big concern was that there's a lot of pre-existing unsafe code that could rely on the drop being at the end of the scope, and not earlier. And you could imagine where, in a world with early drop, maybe you write some unsafe that's sound, but then the safe code changes, something gets dropped earlier, and now it's not sound anymore.

This doesn't mean that this affects Koka, I haven't spent any time with it yet and so I don't mean to imply this is the wrong decision, just showing some related work.

> A little type system goes a long way, and there's such a thing as too much in my opinion.

Agreed.

The purpose of "types" is to make the program easier to understand, because the invariants expressed as type-declarations hold at all times of the program execution. That makes it EASIER to reason about the program, in other words makes it easier to understand your program and what it is doing, by understanding what it cannot be doing, meaning violating its type-constraints.

But now IF the type-declarations-language becomes highly advanced and thus complex and difficult to understand, that potentially makes your program more DIFFICULT to understand.

So it's good to keep the purpose of type-systems in mind while thinking about their benefits. We declare types only so that we and others can better understand what our programs are doing.

Of course if the program is small, it is typically easy to understand and may be even easier to understand without them.

You have to distinguish between "understanding" and "reasoning". Understanding means "understanding what ... does", where as reasoning (in "functional" jargon) means (more like) "proving what ... does".

While it's quite easy to understand what e.g. `c = a + b;` in C does, reasoning about it is comparably hard, as there can be UB (overflow of a signed integer type) involved.

In the extreme, when you have an actual proof (in a dependently typed language), you only have to understand it, but no need to reason about it as the proof is already there ;)

[insert some dependently typed vector example here :D]

> So it's good to keep the purpose of type-systems in mind while thinking about their benefits. We declare types only so that we and others can better understand what our programs are doing.

I don't agree with this. Part of the benefit of static types is to make it easier for programmers to reason about programs. But part is also to make it easier for compilers to reason about programs. By encoding more invariants in the type system it is possible to turn a larger class of bugs into compiler errors.

I would even go as far as arguing that in languages with manual memory management like C, types are primarily a means to tell the compiler how to treat & manipulate a given piece of memory. Type safety and making it easier for us to reason about code can be a side effect of that but it's not a given.

Algebraic effects are not basically the same as Common Lisp conditions.

I hadn't heard of Common Lisp Conditions before reading this thread, but I looked them up in response to it, and I have to ask -- what is the fundamental difference?

Granted Common Lisp is not statically typed and the type system support for effects is a major part of the utility of algebraic effects in Koka, but otherwise they do look remarkably similar to me, both offering a form of delimited continuation that allows you to write code that can call out to a non-local handler that is set up the call stack, and which can itself return control to the caller.

> what is the fundamental difference

CL's condition system is one of the (possible) applications of an algebraic effect system (implemented using delimited continuations). Schemes have dynamically typed (delimited) continuations, for example.

But going in the opposite direction, could you not also implement arbitrary effects using conditions? (Or delimited continuations in schemes)

I am not sure about conditions (I don't know enough about CL), but the effect system of Koka (and OCaml) uses delimited continuations. So it is doable in Scheme, with shift/reset or prompt/control or whatever primitives are defined.

You don't need to know category theory to use a statically typed functional language. It just happens that people interested in research languages also happens to be mathematically inclined. You also don't need to be a type astronaut to use Haskell, you can write perfectly simple and pragmatic code in it.

I mean people cope with the horrible complexity of TypeScript just fine and that system doesn't even give you the benefit of being sound.

> that system doesn't even give you the benefit of being sound

I have hated parts of the TS type system with passion but this is the first time I'm hearing about unsoundness. Would you mind elaborating?

https://www.typescriptlang.org/docs/handbook/type-compatibil...

For example: https://www.typescriptlang.org/docs/handbook/type-compatibil...

https://www.typescriptlang.org/docs/handbook/type-compatibil...

Or the type of an array and its elements:

    const arr :  number[] = [1]

but

   const this_is_actually_undefined : number = arr[456]

so it should be

    const correct_type : number | undefined = arr[idx]

And there are way more, I'm too lazy to search for them or think about them.

Ah, yes, I've stumbled about plenty of such cases – TIL that "unsoundness" is an established term for them.

Thanks so much!

Reply on news.ycombinator.com