Vilem (Sep 23 2022 at 16:27): Vilem (Sep 23 2022 at 16:27):Hi y'all. Is there a language reference for Roc? I am doing a PhD in programming language theory and I might have a go at formalising Roc's type system.
Richard Feldman (Sep 23 2022 at 19:53):there is not currently, but I'd be happy to work with you on that!
Ayaz Hafiz (Sep 23 2022 at 21:09):Wow, that sounds great! Echoing what Richard said.
Ayaz Hafiz (Sep 23 2022 at 21:09):We have some open questions around the type system (esp. with regard to type classes interacting with other type-level features in Roc) that we're working on trying to strongly define, if you have any interest in that as well.
Vilem (Sep 24 2022 at 19:39):First of all, massive disclaimer: I will _try_–I'm still learning to wrangle Coq. Also, I won't be proving any properties about the _implementation_ of the type system, but rather I will be writing a _specification_ and proving metatheoretic properties of the specification.
Based on my current understanding, from watching the presentations linked on the website, Roc features an HM type system with:
I probably got some of this wrong and perhaps there are missing bits; please let me know if that is the case.
I confess that I haven't built the Roc compiler yet, so that might be a good starting point for getting more of an intuition for the language, as the online playground didn't work for me.
My current action plan is to get a proof of progress and preservation ("well typed programs don't go wrong") with features 1 thru 4 from the list above. If I get that far, then we can talk ;)
Ayaz Hafiz (Sep 24 2022 at 20:02):Yeah, that's correct!
anonymous, disjoint sums
tags/labels
These are the same thing in Roc, Roc's disjoint sums are very similar to polymorphic variants a-la OCaml.
There are other type-level features that are not in this list (i.e. some tricks to express defunctionalization at the type-level), but that can mostly be thought of as orthogonal to the type system in general.
Ayaz Hafiz (Sep 24 2022 at 20:03):What are effect modalities?
Ayaz Hafiz (Sep 24 2022 at 20:03):as the online playground didn't work for me.
Could you please let us know what problems you ran into, by filing an issue?
Richard Feldman (Sep 24 2022 at 20:14):there are also nightly releases of the compiler for various operating systems, so you should be able to download one and try it out without having to build from source!
Vilem (Sep 25 2022 at 10:56):Ayaz Hafiz said:
What are effect modalities?
The type-level constructors used in effect tracking. I'm guessing this is something like an indexed m***d?
Ayaz Hafiz (Sep 25 2022 at 15:59):I see. yeah, it's like an indexed monad, but it falls out entirely from the behavior of Roc's tag unions. There are some examples in https://github.com/roc-lang/roc/blob/main/examples/interactive/cli-platform/File.roc; in short if you have two effects read : {} -> Task Str [Read] and write : Str -> Task {} [Write] (here you can pretend Task is any monad) and you compose them, you send up with {} -> Task {} [Read, Write].
Folkert de Vries (Sep 25 2022 at 16:01):you're missing some type variables there. it should be read : {} -> Task Str [Read]*, so that the "effect row" can grow to include more things
Vilem (Sep 25 2022 at 16:24):Is [Read, Write] a set?
Folkert de Vries (Sep 25 2022 at 16:25):effectively
Last updated: Jul 05 2025 at 12:14 UTC