[CornCobs]

Koka is very interesting I must say. It's really cool to see how far they managed to make a functional language look imperative superficially, while being entirely functional under the hood and managing semantics via effects.

However, I believe they aren't really able to present a full imperative API to write programs in (or maybe they just haven't fully implemented the needed parts in the stdlib).

For example IIRC, the use of mut variables (internal mutability within a function and implicitly handled effect) and the related explicit heap effect don't seem to be able to share functions? And while they seem to work with entire objects the functions for mutations within arrays seemed limited the last time I tried Koka out. And everything being exposed only through the API presented some things were not possible to work around. I believe I was unable to write functions that mutated an array in place.

If anyone has had experience with Koka I would love to be proven wrong!

That said my initial point still stands - I think its an amazingly cool language and clearly a lot of interesting ideas are in it for sure.

[saityi]

So I would say this echoes my experience with it so far -- it is definitely a work in progress! However, I tend to approach Koka as if it were Standard ML with an effect system (up to a point), so the lack of a full imperative API hasn't been felt too much. I am more missing ad-hoc polymorphism than imperative tooling.

I am not sure I understand your comment about mut variables; my understanding is there are two types of mutable variables in Koka -- 'local' and 'ref'. 'local' is a locally mutable variable, and 'refs' are globally shareable. A 'ref' can be shared between functions, 'local' is just to give an imperative API using mutable variables. How 'local' works kind of confuses me so I tend to avoid it altogether in favour of local names (i.e. 'val' rather than 'var') and tail recursion (instead of loops with mutation). 'ref' seems quite usable to me and seems to reflect the SML usage of it.

I have felt the pain of a lack of an array, but I ported over an Okasaki data structure which has served well for a random-update, sequential data structure. Their data structures in the stdlib just have comments that say 'TODO': https://github.com/koka-lang/koka/blob/master/lib/std/data/m... that I am hoping are open to pull requests.

[anfelor]

You might be interested in the FBIP versions of Okasakis datastructures in https://github.com/koka-lang/koka/tree/master/test/perf/sets Most of them only have 'insert' and 'lookup', but they are ~10% faster than Okasakis versions. For red-black trees in particular the fastest implementation is https://github.com/koka-lang/koka/blob/master/test/bench/kok...

[saityi]

I'd missed those -- thank you!

[CornCobs]

I'll just hijack this thread to ask a question about effect systems:

It seems to me that effects primarily have 2 uses:

1. Provide a controlled form of dynamic scoping (decouple usage and handling - allowing functions to be generic in their effects)

2. Create custom control flow with multiple resumes etc at the effect callsite

It feels to me that these are largely orthogonal ideas, but are always conflated in effect systems. Is there a reason for this? Are there examples of one without the other?

[saityi]

I think it goes back to the neverending quest to find ways of representing computation that allows of ease of composition, changing implementation details, eliminating classes of errors by construction, etc. Monads have had some success in this arena, but they have notable issues with composition; monad transformers help, but can become unwieldy in their own ways.

An alternative are effects, hypothetically allowing for ease in building programs as separate but composeable components which can then be freely mixed in or swapped out. In practice I have found working with effect systems in Haskell via libraries stresses the type system so much you end up with scoped type variables and type applications everywhere. My understanding is that the theory behind using effects to structure computations comes from category theory's Lawvere theories (see e.g. Pretnar's 2010 dissertation on https://github.com/yallop/effects-bibliography). Lawvere theories give rise to many monads (see Bartosz Milewski's article on it -- https://bartoszmilewski.com/2017/08/26/lawvere-theories/), but with nicer compositional properties.

This is where languages like Effekt, Eff, Frank, and Koka come in -- by writing the entire language and type system to support the theories, a lot of the pain of expressing it in Haskell can be avoided.

[lakecresva]

Their section on development tasks mentions fleshing out std and improving array/mutable reference programming, so I think it just hasn't been redone yet. It seems like they spent a lot of development time recently (with great success) working on foundational stuff like perceus/fbip and doing a major version bump, so std is pretty bare.