Dependent Types in the wild

[dumblob]

In another thread @MaiaVictor mentioned a C backend is on its way. Which is super great (assuming its goal is to support unlimited parallelism among physical/virtual CPU cores). But making it efficient and fast can become soon intimidating.

This and other things are being researched and coded in other projects already - so it might make sense to take a look, whether some parts couldn't be shared to save precious time instead of reinventing the wheel.

1. E.g. in the Project Everest they have assembly generator backend "Vale" for pure dependent types language called F*.
2. In Project Everest they even have high-quality framework for distributed and concurrent programming SteelCore (this might be a good source of inspiration for stuff discussed in Distributed computation - parallelism & concurrency #167 ).
3. Another distributed computing project which actually shares already the Formality backend with Kind 😮: https://github.com/yatima-inc/yatima (though admittedly I couldn't find anything related to distributed computing there yet 😢 - and the syntax is by far not so nice & polished as in Kind)
4. Framework for formal verification of distributed systems (uses Coq): https://github.com/uwplse/verdi
5. very cool and useful tricks in Shen mostly applicable to Kind as well: https://www.youtube.com/watch?v=BUJNyHAeAc8

... and surely others (will be added on the go).

[VictorTaelin]

We had a C backend, but it used a direct compilation to interaction nets. While optimal, it was not so efficient, specially because of the overhead of λ-encoding everything, the lack of a garbage collector, missing parallelism opportunities, and just an overall lack of man-hours (hard to compete with compilers that had orders of magnitude more manpower). But I still think it is promising, specially if we compile functions and pattern-matching to specialized inet nodes, instead of λ-encodings. I'm working on this direction but slowly. You shouldn't expect anything major unless we get way more resources to pour on this project (but if we did, I truly believe such a thing would be world-changing; I strongly believe a well-optimized inet runtime would greatly surpass GHC, ChezScheme and others).

About Yatima, I don't think it currently shares our backend in any way, does it? It just shares a lot of ideas with Kind since both languages departed from Formality, but as far as I'm aware, they've started from scratch.

[VictorTaelin]

BTW if, by chance, any rich Dogecoin investor, that happens to have a weird fetish about creating the fastest functional language physically possible, is reading this, let's talk! I'd love to put/spend some resources to build a team to develop a massively parallel inet runtime that could serve as the ultimate compile target for functional languages, but I don't think I can do that alone. Imagine Haskell, Scheme, Kind and the like running in your RTX 3080 TI cores as blazingly fast as your pro-gamer shaders and crypto miners. That is the world I want to live in!

[dumblob]

I'd love to put/spend some resources to build a team to develop a massively parallel inet runtime that could serve as the ultimate compile target for functional languages, but I don't think I can do that alone.

I'm in contact with some potentially relevant people from three universities - maybe if there was something like a "plan" (imagine you'd be signing up for Google Summer of Code and would need to meet related criteria) I could point them at it and they'll get in contact with you if there are any students willing to make this "breakthrough" happen.

[VictorTaelin]

Interesting, @MaisaMilena can you help me here? I'm not familiar with Google Summer of Code submission format and criteria but I'd be glad to provide one for such parallel functional compiler.

[MaisaMilena]

I'm in contact with some potentially relevant people from three universities - maybe if there was something like a "plan" (imagine you'd be signing up for Google Summer of Code and would need to meet related criteria) I could point them at it and they'll get in contact with you if there are any students willing to make this "breakthrough" happen.

That's cool! I imagine that the document you mentioned would be like specifying the team skills needed to complete it, the approximate time to complete it, and the goals, is that correct?

[dumblob]

@MaisaMilena exactly that!