[bjoli]

I am always impressed by what the ocaml/Haskell people can do compared to my language of choice (scheme).

Iirc Oleg Kiselyov implemented proper delimited continuations in ocaml as a library, without touching the runtime or compiler. Something similar has been done in Haskell.

I doubt fully dependent types can be implemented in Haskell without extra help by ghc. There has been lots of work in the area, and last time I checked you could simulate DT to some degree, but it never was as powerful as the dependant types in idris. Iirc t were some edge cases where the typing became undecidable.

[fasquoika]

>Iirc Oleg Kiselyov implemented proper delimited continuations in ocaml as a library, without touching the runtime or compiler.

To clarify this, the library you're talking about implements most of the functionality in C, reusing the runtime's exception mechanism. So it doesn't require any upstream change to compiler or runtime, but it also can't be implemented in pure OCaml.

[bjoli]

Hmmm. I remembered incorrectly then. The bytecode version is possible in pure ocaml, but for native it apparently needs C.

For Haskell it is however possible. There is a neat paper by among others Kent Dybvig.