61–67 of 67 posts
At first glance I get the feeling that it is really nice! Any elaboration on that would be really appreciated.
Good luck with this project. For sure you are on to something. Time will tell. Don’t forget to research industry leaders like Ted Nelson :)
Could you explain why did you choose to write your own implementation of DAG instead of using something like petgraph? At first glance I get the feeling that it is really nice! Any elaboration on that would be really appreciated. Good luck with this project. For sure you are on to something. Time will tell. Don’t forget to research industry leaders like Ted Nelson :)
You can see the output of that here: https://i.redd.it/94zg24fboyv61.png
(N.B. We removed that module from the language core since we're trying to make that no_std, but we're adding it back to our utils crate soon: https://github.com/yatima-inc/yatima/issues/70)
But we can't use petgraph for the actual computational lambda-DAG because of performance. For example, one thing we get by using pointers is constant-time insertion and removal of of parent nodes (every node in the graph points to their parent). We actually wrote our own Doubly-Linked-List in Rust (it can be done!) to store pointers to the parents for this reason: https://github.com/yatima-inc/yatima/blob/main/core/src/dll.....
There's also memory concerns, given that the lambda-DAG collects its own garbage, freeing space allocated for nodes when no longer in use, whereas I believe petgraph is just `Vec` internally, which would require shrinking, and that would also be slow.
All this low-level pointer manipulation was, tbh, a huge amount of work, but the end result is a performant lazy lambda-calculus reducer with sharing in a few thousand lines of Rust, which means fast lambdas on wherever WASM runs.
(That said, I'm a little bit concerned about cache misses with all the pointer chasing we do, but I haven't yet gotten around to profiling different Yatima expressions to measure this. Would be a great project for an OSS contributor too, so I'll probably make a GH issue for it!)
Was this intentional?
Earlier quoted context omitted.
I didn't claim that we have solved or will solve the diversity problem, but I did articulate in the README a few ways that I thought Yatima might contribute. I also don't agree with your characterization of Haskell, Rust and OCaml as being "high-barrier-to-entry" compared to Python. Personally, I find languages like Python much harder to work with given how arbitrary and detail oriented they are. I think for a lot of…
> I also don't agree with your characterization of Haskell, Rust and OCaml as being "high-barrier-to-entry" compared to Python. Personally, I find languages like Python much harder to work with given how arbitrary and detail oriented they are. This is an interesting POV to be sure, but it should be made more practical and testable, by writing introductory resources for the average user that are targeted to these lang…
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.
Yatima in arabic means orphan. Was this intentional?
> In the Truth Mines, though, the tags weren't just references; they included complete statements of the particular definitions, axioms, or theorems the objects represented. The Mines were self-contained: every mathematical result that fleshers and their descendants had ever proven was on display in its entirety. The library's exegesis was helpful-but the truths themselves were all here.
Also it's a little homage to both "orphaned technologies" in the history of functional languages, such as the LISP machines: https://en.wikipedia.org/wiki/Lisp_machine, and to Haskell's "orphan instances" https://wiki.haskell.org/Orphan_instance.
Some random questions to the developers regarding the motivation that "math is more fun when you have a computer to take care of the detail-work" [0]: 1. Do you have plans to make Yatima a usable theorem prover? 2. If so, how will people typically quotient things (e.g. does it have quotient types)? 3. How far does the type theory depart from classical mathematics? 4. The paper you've linked [1] suggests that the stan…
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…
Looking forward to it!
