4 ms·

> Koka tracks the (side) effects of every function in its type, where pure and effectful computations are distinguished. The precise effect typing gives Koka ro

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

yawaramin 3y ago
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.
- djtango 3y ago
  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
- galaxyLogic 3y ago
  So this means we have benefits of Rust but in a nicer, functional syntax?
  - whitim 3y ago
    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).
- bobbylarrybobby 3y ago
  How does it achieve better deallocation performance?
  - yawaramin 3y ago
    They have created a new precise reference-counting algorithm, called Perceus: https://www.microsoft.com/en-us/research/uploads/prod/2020/11/perceus-tr-v1.pdf 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.
    - steveklabnik 3y ago
      Interestingly, in Rust, we thought about doing this. "early drop" was the term folks talked about https://github.com/rust-lang/rfcs/pull/239 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.
nesarkvechnep 3y ago
Algebraic effects are not basically the same as Common Lisp conditions.
- asQuirreL 3y ago
  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.
  - ReleaseCandidat 3y ago
    > 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.
    - asQuirreL 3y ago
      But going in the opposite direction, could you not also implement arbitrary effects using conditions? (Or delimited continuations in schemes)
      - ReleaseCandidat 3y ago
        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.
galaxyLogic 3y ago
> 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.
- ReleaseCandidat 3y ago
  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]
- thinkharderdev 3y ago
  > 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.
  - codethief 3y ago
cardanome 3y ago
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.
- codethief 3y ago
  > 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?
  - ReleaseCandidat 3y ago
    https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness https://www.typescriptlang.org/docs/handbook/type-compatibil... For example: https://www.typescriptlang.org/docs/handbook/type-compatibility.html#function-parameter-bivariance https://www.typescriptlang.org/docs/handbook/type-compatibil... https://www.typescriptlang.org/docs/handbook/type-compatibility.html?#optional-parameters-and-rest-parameters 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.
    - codethief 3y ago
      Ah, yes, I've stumbled about plenty of such cases – TIL that "unsoundness" is an established term for them. Thanks so much!

yawaramin 3y ago

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.

djtango 3y ago
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
galaxyLogic 3y ago
So this means we have benefits of Rust but in a nicer, functional syntax?
- whitim 3y ago
  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).
bobbylarrybobby 3y ago
How does it achieve better deallocation performance?
- yawaramin 3y ago
  They have created a new precise reference-counting algorithm, called Perceus: https://www.microsoft.com/en-us/research/uploads/prod/2020/11/perceus-tr-v1.pdf 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.
  - steveklabnik 3y ago
    Interestingly, in Rust, we thought about doing this. "early drop" was the term folks talked about https://github.com/rust-lang/rfcs/pull/239 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.

nesarkvechnep 3y ago

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

asQuirreL 3y ago
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.
- ReleaseCandidat 3y ago
  > 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.
  - asQuirreL 3y ago
    But going in the opposite direction, could you not also implement arbitrary effects using conditions? (Or delimited continuations in schemes)
    - ReleaseCandidat 3y ago
      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.

galaxyLogic 3y ago

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

ReleaseCandidat 3y ago
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]
thinkharderdev 3y ago
> 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.
- codethief 3y ago

cardanome 3y ago

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.

codethief 3y ago
> 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?
- ReleaseCandidat 3y ago
  https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness https://www.typescriptlang.org/docs/handbook/type-compatibil... For example: https://www.typescriptlang.org/docs/handbook/type-compatibility.html#function-parameter-bivariance https://www.typescriptlang.org/docs/handbook/type-compatibil... https://www.typescriptlang.org/docs/handbook/type-compatibility.html?#optional-parameters-and-rest-parameters 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.
  - codethief 3y ago
    Ah, yes, I've stumbled about plenty of such cases – TIL that "unsoundness" is an established term for them. Thanks so much!