Yatima: A programming language for the decentralized web

1. yatima-lang-alpha

   1 9 450 0.0 Rust

   Discontinued A programming language for the decentralized web

   

   Totally a fair point. Honestly I'm not sure the Yatima's actually ready for on-boarding language users, as distinct from language contributors, just yet. Like, if you want to hack on a Rust implementation of a functional language and can figure out a lot stuff from the source, we're just about ready for you. If you want to use the language to build software that's useful for some other purpose, I don't think we're quite there yet. We don't even have IO yet!

   But you're definitely right that once we're ready for people who aren't contributors to use the language we'll need code examples, tutorials, a web repl (it's in progress! https://github.com/yatima-inc/yatima/tree/main/web), and all that good stuff. 100% agree on that

2. InfluxDB

   www.influxdata.com featured

   InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

   

3. introit

   2 5 20 2.6 Nix

   The Yatima Standard Library

   

   I would dearly love to make Yatima a usable theorem prover, and Lean has been a huge inspiration particularly regarding syntax. But building a usable theorem prover is a huge project, and at minimum will require substantial work on our theory, on type-inference (which is fairly minimal right now) and on advanced features like quotient types or univalence.

   On that point, we've done a little exploration on encoding the Path types from Cubical Type Theory as self-types, and I think there's some promising work to be done there. But I know my limits and while I feel very comfortable building a useful programming language that can do a little bit of basic theorem proving, I know that doing a proper job on a real theorem is going to require larger scale resources.

   As far as the link from the Self-Types paper, our theory is similar to their System S, but is not the same. Not 100% sure but I think the main relevant difference here is about Leibniz equality, which iirc allows for saying `a == b` when `a` and `b` are of different types. Yatima's Equal type https://github.com/yatima-inc/introit/blob/main/Equal.ya, implements the more standard homogenous/Martin-Löf equality, but this is just a library, not a language builtin.

   We really do need to write an actual paper for Yatima's theory though, especially considering that we've combined the self-types from System S with a variation of Quantitative Types a la Idris 2. Writing that paper is likely step 0 of any Yatima as a theorem prover project, until then we should view Yatima as just an unsound functional programming language with some nice type-level features

4. matrix.to

   3 265 1,072 4.5 JavaScript

   A simple stateless privacy-protecting URL redirecting service for Matrix

   

   Absolutely accepting contributions, come join our matrix channel: #yatima:matrix.org https://matrix.to/#/!bBgWgXJqeKuDuiUYWN:matrix.org?via=matri...

   This issue (on improving the test-suite) is a particularly good starter issue: https://github.com/yatima-inc/yatima/issues/37

5. lunatic

   4 86 4,682 5.7 Rust

   Lunatic is an Erlang-inspired runtime for WebAssembly

   

6. Seed

   5 36 3,836 2.2 Rust

   A Rust framework for creating web apps

   

7. base64-bytestring

   6 1 45 4.7 Haskell

   Fast base64 encoding and decoding for Haskell.

   

   Sure, if you consider Haskell's runtime (I know that technically GHC /= Haskell, but in practice it's the only Haskell that matters, except maybe something like Asterius) all the primitives are backed by C libraries: https://hackage.haskell.org/package/ghc-prim-0.4.0.0/docs/GH...

   Likewise with conventions around pointers, arrays, etc. to the point where if you want to do anything really low-level or performance sensitive in Haskell, you're essentially punching a hole into C. As a random example, within the fast base64bytestring library, you find lots of use of `malloc`, `ForeignPtr` etc.: https://github.com/haskell/base64-bytestring/blob/master/Dat... And of course because this is C there aren't really many safety guarantees here.

   The plan with Yatima with its primitives, and eventually when we write an FFI is to integrate with Rust in the same way that Haskell uses C. My hope is that with Yatima's affine types we might even be able to FFI to and from safe Rust (since the borrow checker uses affine types), but this is a little bit of a research project to see how much that works. Even to unsafe Rust though, we have better safety guarantees than C, since unsafe Rust's UB is still more restricted than C's is.

8. ATS-Xanadu

   7 1 218 9.9 ATS

   Bootstrapping ATS3

   

   There's definitely some similarities to ATS conceptually, but not that much in the actual implementation, and definitely not in the syntax.

   That said, Hongwei Xi is a genius, and ATS is one of the most important and innovative languages of the past decade, despite the crazy syntax (seriously, t@ype for the sort of flat memory types is just bonkers). I'm really looking forward to ATS3 though https://github.com/githwxi/ATS-Xanadu, and I think there's chance it could gain serious traction.

9. SaaSHub

   www.saashub.com featured

   SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

   

Suggest a related project