daanx

6 ms·

1.
by daanx 2y ago
> 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 actually also used in K
2.
by daanx 2y ago
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. About duplicate labels..
3.
by daanx 2y ago
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 extensions: https
4.
by daanx 2y ago
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...
5.
by daanx 5y ago
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 to play wit
6.
by daanx 5y ago
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 structure
7.
by daanx 5y ago
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 example.
8.
by daanx 5y ago
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 EST): <
9.
by daanx 6y ago
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 lik
10.
by daanx 6y ago
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 data types in Koka are i
11.
by daanx 6y ago
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 ob
12.
by daanx 6y ago
(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 mat
13.
by daanx 6y ago
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 [mimalloc]( https://github.com/microsoft&#x2F
14.
by daanx 8y ago
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 | r } -> i
15.
by daanx 8y ago
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: https://www.microsoft.com/en
16.
by daanx 9y ago
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 in PuTTY -- tha
17.
by daanx 9y ago
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` integratio