Stream: ideas

Topic: integration with dependently typed languages

Qqwy / Marten (Sep 18 2022 at 17:28):

Hi all!

I recently listened/read this very interesting interview/podcast with one of the people that did a lot of work on Idris in the past and currently is writing a book about using Lean 4. https://serokell.io/blog/dependent-types-with-david-christiansen
Idris and Lean are both dependently-typed languages.

And it made me think: Wouldn't it be cool to be able to use Roc as a compilation target for Idris (or Lean, but I'm not sure whether multiple compile targets is something that is currently being considered in Lean)?
This would allow one to use dependent typing to develop the internals of certain libraries, allowing them to be 'provably correct', while being callable from other Roc code.

Qqwy / Marten (Sep 18 2022 at 17:30):

One reason why I think this might be a very cool idea is because I think that type-erased Idris/Lean code will be very close to Roc code, so there is little to no need for an extra 'runtime system'. And it would allow the triple gamut of optimization:

• On the Idris layer
• On the Roc layer
• On the LLVM/Wasm layer.

Ayaz Hafiz (Sep 18 2022 at 22:37):

It's definitely a cool idea. In my experience (which of course is limited, mostly with Coq) extraction from a proof language is pretty straightforward, if the language's core exposes a type-erased IR (that's the difficult bit in compilation, iirc)

Ayaz Hafiz (Sep 18 2022 at 22:40):

you could also imagine some interesting ideas around the discovery of theorems, and proofs of them, about Roc programs. Hipster is one example of this for Haskell; Sledgehammer is another

Ayaz Hafiz (Sep 18 2022 at 22:42):

One thing to consider is that the ergonomics of writing code that is lowered to Roc can only be as nice as that of the source language; it may not be as nice as writing Roc code directly. You will not be able to use external Roc libraries directly, nor Roc compiler/editor features

Folkert de Vries (Sep 18 2022 at 22:43):

the idris core language can be compiled to php so seems like roc should be able to be a compilation target too then

Last updated: Jun 16 2026 at 16:19 UTC