1. 34

  2. 21

    The github link seems much more useful as an introduction: https://github.com/koka-lang/koka.

    Koka is a strongly typed, strict functional language which tracks the (side) effects of every function in its type. Koka syntax is Javascript/C like, the evaluation is strict like OCaml/C, and the type- and effect system is Haskell like, 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. (Given the importance of effect typing, the name Koka was derived from the Japanese word for effective (Kōka, 効果)).

    1. 1

      nice, the section on “perceus” reference counting was particularly interesting and provides a good motivation for “why would i use this language”

      1. 1

        Yes, I am thinking you might be right. Thanks for posting!

      2. 8

        Algebraic effect handlers struck me as a really neat idea when I first read about them, but such a new concept in PL theory that basically no language was using them. I’m interested in learning more about how this Koka language reifies the idea.

        1. 2

          There is something similar, also called “effects”, in the Nim language. In my brief time with Nim I haven’t encountered them in actual use, whereas they seem very in-your-face in Koka. (I recognize other common concepts between the two languages, like unifying function-call and method-call syntax.)

          1. 2

            Yes, aren’t the OCaml folks looking into them as well? I need to learn more, myself.

          2. 2

            I like languages that track precursors to program correctness within their syntax.¹ Some examples of what I mean:

            • Haskell tracks effects. It accomplishes this with category theory which, like all mathematics, is elegant for some things and not for others.²
            • Now that Haskell’s been around for decades, we’ve developed a better understanding of what’s useful for tracking effects. Koka builds on this knowledge, taking a more refined, pragmatic approach to effect tracking.
            • Meanwhile, Rust uses this metadata to track ownership and lifetimes.

            I would love to see something like Koka that also integrated Rust’s memory (and perhaps thread) safety features, all while remaining a formally specified language… unlike Rust. This might lose the user a lot of flexibility in how tight a hold to have on the low-level implementation of program components. I think retaining that flexibility would require being able to “choose a language” like you can in Racket, while also being able to selectively enable/disable GC like you can in Go. I’m missing some knowledge on this, so if anyone knows more, please fill me in!

            ¹ These should have a term… “integrated metadata languages”?

            ² Monad composition is rough, and the main solution is to use monad transformers. A quick Google search brought up a good treatment (Quora) of the problem.