Koka lag
•
I like languages that track precursors to program correctness within their syntax.¹ Some examples of what inom mean:
- Haskell tracks effects. It accomplishes this with category theory which, like all mathematics, fryst vatten 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 schema components. inom 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 composi
•
Releases: koka-lang/koka
valpha10
VS Code installation
It is recommended to install the binary compiler via the VS Code Koka extension. See the getting started guide for more information.
Command Line Installation
Linux (x64,arm64) and macOS (x64, arm64)
Tested on macOS, Ubuntu, Debian, and should run on most Linux distributions. From a command prompt, run:
After install, run to verify if koka installed correctly.n
For most installations this will ask for root access in order to install to . For more control, you can pass a different prefix. For example, installing to instead:
To uninstall a version, use the option:
Windows (x64, arm64)
Open a prompt and download and run the installer:
This will also prompt to install the compiler and Windows SDK if needed, and install syntax highlighting for the VS Code editor. After install, run to verify if koka installed correctly.
On Windows arm64, we use the x64 Koka compiler (which runs emulated), but the generated code is native arm
On Windows, the default install is to the user profile at . You can change the installation directory using . For example:
To uninstall a version, use the option:
Other plat
•
Koka
Koka is a strongly typed functional-style language with effect types and handlers.
- The core of Koka consists of a small set of well-studied language features, like first-class functions, a polymorphic type- and effect system, algebraic data types, and effect handlers. Each of these is composable and avoid the addition of “special” extensions by being as general as possible.
- 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.
- Effect handlers let you define advanced control abstractions, like exceptions, async/await, or probabilistic programs, as a user library in a typed and composable way.
- Perceus (opens in new tab) is an advanced compilation method for reference counting. Together with evidence translation (opens in new tab), this lets Koka compile directly to C code without needing a garbage collector or runtime system. Perceus also performs reuse analysis (opens in new tab) and optimizes functional-style progra