Continuations

[Mathnerd314]

During the talk, you mentioned a "type system which will solve the world's programming problems forever, unifying every possible type of language feature into one grand abstraction", and presented a slide showing "Higher-kinded dependently-typed GOTO".

But Malfunction doesn't have continuations, just lambdas. You can't even write GOTO, much less COMEFROM. Furthermore it seems like continuations are an elegant way to unify eager and lazy programming.

My point here is that while OCaml doesn't support continuations, SML/NJ does. I guess it's a little slower than OCaml, but not by much (7.8 vs 9.3 seconds in a toy benchmark).

[stedolan]

I'm not quite sure what you're suggesting / asking for. Do you want Malfunction to be retargeted to SML/NJ? I'm unfamiliar with SML/NJ's internals, does it have an untyped intermediate representation before closure conversion? Regardless, I think that would be a separate project.

Speaking of continuations, Malfunction / OCaml is unlikely to ever have call/cc. There are good reasons to avoid it!. We're working on adding delimited continuations / algebraic effects to OCaml, which will hopefully show up in Malfunction eventually.

[Mathnerd314]

Do you want Malfunction to be retargeted to SML/NJ? I'm unfamiliar with SML/NJ's internals, does it have an untyped intermediate representation before closure conversion? Regardless, I think that would be a separate project.

I'm not that familiar with SML/NJ either, but I think it has a structured compilation pipeline. I guess I will poke around to find someone else more knowledgeable on that subject.

Speaking of continuations, Malfunction / OCaml is unlikely to ever have call/cc. There are good reasons to avoid it!. We're working on adding delimited continuations / algebraic effects to OCaml, which will hopefully show up in Malfunction eventually.

I was using continuations in the sense of the "Haskell is not not ML" paper, which I guess is a rather non-standard definition. Its continuations are a sort of zero-argument lambda, that is guarantee to never produce a value, and where the type of the continuation specifies the expected layout of the stack/heap.

The question I had boils down to whether there's anything like those continuations in the OCaml compilation pipeline, that maybe Malfunction could expose, or if it's necessary to write yet another closure conversion library to experiment with the paper's continuations.

[stedolan]

OCaml has nothing directly comparable to the continuations / negation types in the paper you linked, but I suspect you could simulate them by implementing ~T as functions from T to some abstract result type.