daanx
- Karma
- 50
- Created
- July 31, 2017 (8y ago)
- Submissions
- 0
<https://www.microsoft.com/en-us/research/people/daan>
<https://github.com/koka-lang/koka>
<https://github.com/microsoft/mimalloc>
<https://github.com/koka-lang/koka>
<https://github.com/microsoft/mimalloc>
> This idea is so simple, so crazy, so stupid, and works so well, but I never thought of it. Bravo to the authors. Thanks for the nice summary -- looking forward to read the paper! The same idea of self-tagging is…
Haha, thank you for your kind reply :) really enjoyed the blog post as it shows nicely that implementing HM can be straightforward -- many papers on inference are usually quite math heavy which can be a tough read.…
That's a nice overview of Hindley-Milner in practice! For those interested, I recently have been thinking of a better way to specify type inference with principal derivations that lends itself better for type system…
And Andrew Kennedy gave a very nice lecture on this recently as part of Xavier Leroy's seminar on control structures: https://www.college-de-france.fr/fr/agenda/seminaire/structu...
Yes -- I think historically the power of condition handling was not well understood and algebraic effect handlers were a "rediscovery" coming from well-studied category theory (Plotkin, Power, and Pretnar). If you want…
I like the characterization that Andrej Bauer uses: "while relates to goto, as effect handlers to shift/reset" :-) That is, you indeed need delimited continuations to implement effect handlers, but they have more…
Yes! a nice aspect of effect handlers is that they have an untyped dynamic semantics. Having said that, tracking effect types can be very beneficial, especially if you do interesting control flow like async/await for…
The modern way of call/cc and shift/reset is using Effect Handlers instead [1]. If you are interested in this, Ningning Xie and I give a tutorial about effect handlers (and more) at ICFP'21 tomorrow (Thursday 12:30…
In practice, I have not (yet) found many great use cases for the distinction in Koka. It is nice to have "total" functions, but "pure" (exceptions+divergence) is still a good thing (and what Haskell gives you). And like…
Just to add to this: Koka can (obviously :-)) not always determine if a function will terminate or not so it generally adds a `div` effect whenever there is the possibility of infinite recursion. However, since most…
Ah, I think Stephen meant to write the following: fun add-refs( a : ref<h,int>, b : ref<h,int> ) : st<h> int { a := 10 b := 20 (!a + !b) } where indeed the effect is `st<h>` as the updates are observable. How the…
(Daan here, creator of [Koka](https://github.com/koka-lang/koka) This is an interesting point and comes down to the question -- what is an effect really? I argue that effect types tell you the type signature of the…
Interesting article -- thanks! I see they used the `key ^ P` encoding where the `key` is `L >> PAGESHIFT` to use the ASLR randomized bits from the free list position `L`. In…
Thanks :-) TREX (by Mark Jones and Benedict Gaster) is great. The beauty is that a lacks constraints can get translated to fields offsets at runtime making it super efficient! E.g. a type like: foo :: r/x => { x :: int…
Looks like a fun project, very nice :-) For those interested in more of the beautiful theory on extensible row types, this project seems to be based on an earlier paper I wrote on scoped labels:…
I tried to cite much related work on co-routines and threading libraries in C -- including Simon Tatham's page on co-routines in C [1] -- But I was not yet aware of the work on Icon nor did I know co-routines were used…
Hi, I am the author of this report -- thank you for the interest :-) Just wanted to add that you can find the library at: https://github.com/koka-lang/libhandler The `dev` branch contains a sample of `libuv`…