Is there any OCaml(not ML or StandardML) - inspired languages with dependent types and algebraic affects?

Is there any OCaml - inspired languages with dependent types and algebraic affects or libraries / preprocessors / compiler extensions that provides such features for OCaml?

Perhaps this could be of interest :

https://www.fstar-lang.org/

5 Likes

I think the canonical answer to this is http://www.eff-lang.org/ --Eff was the proof-of-concept for OCaml’s upcoming effect handler system.

3 Likes

Eff was the proof-of-concept for OCaml’s upcoming effect handler system.

I think that is a bit of a stretch. I think Eff deserves a little more credit. Eff predates the idea of effect handlers in OCaml. After all, Eff is the very first language to incorporate effect handlers, and as such, a proof-of-concept for any subsequent language adaptation of effect handlers. It might be fair to say that the work on effect handlers in Multicore OCaml has been influenced by Eff to some extent, but their respective designs are very different. They are both very much their own thing.

That said, to provide some kind of answer to OP

Is there any OCaml - inspired languages with dependent types and algebraic affects or libraries / preprocessors / compiler extensions that provides such features for OCaml?

While the surface syntax in Eff is inspired from OCaml, it does not have dependent types.

A few years ago Edwin Brady experimented with effect handlers and dependent types in Idris (I do not know whether this qualifies as “OCaml inspired”). Edwin implemented effect handlers as a library called “Effects”, c.f. his ICFP’13 paper “Programming and Reasoning with Algebraic Effects and Dependent Types”.

How to integrate dependent types and computational effects is an area of active research, where Danel Ahman has made some recent advances on the theoretical side (the linked paper is to appear at POPL and is based on his PhD thesis). However, I am not aware whether any of this has been brought into to practice via an implementation.

I would like to point the OP, and others who may be interested, to Jeremy Yallop’s collaborative effects bibliography, which is a curated collection of literature and software regarding computational effects.

8 Likes

Fair enough, I’m not an expert. Maybe I should have said rather, Eff was the inspiration for OCaml’s effect handlers work.

Yes, the collaborative effects bibliography is really the right place to look at. In particular, it starts with a list of languages/libraries.

1 Like