Yatima: A programming language for the decentralized web
github.com
github.com
(I hope I'm not missing sarcasm.)
Or is it to weed out the people who don't know about beta-reductions ? Am I suddenly in blub world for simply wanting a code example ? Or is there already a tutorial and the link just happens to be missing ?
As far as docs and tutorials, we weren't planning on doing a public release for another month or two, so there isn't anything yet. The language is still pre-alpha, so our focus has been on getting the core working correctly before smoothing the on-ramp.
Also, tbh, I'm not 100% settled on what the user-facing syntax should be. Right now we have a simple lisp-like core syntax, but I'm thinking about implementing something like Racket's #lang declaration to allow the user to define and import frontends to that core syntax.
That said, we're still pre-alpha, so there's a lot of work to do before I'd recommend anyone other than PL nerds actually use the project for anything.
As far as ideology goes, yes, definitely I have strong opinions about computing and how it fits into the human experience. I wrote the Motivation section of the README to make that clear and explicit up-front, so that people can make informed decisions about what they spend their time and attention on.
For example, I recognize that not everyone will agree with the view I express here:
> Yatima, as a project, has an opinionated view of that future. We think computing should belong to individual users rather than corporations or states. A programming language is an empowering medium of individual expression, where the user encounters, and extends their mind through, a computing machine. We believe "Programmer" shouldn't be a job description, anymore than "scribe" is a job description in a world with near-universal literacy. Computing belongs to everyone, and computer programming should therefore be maximally accessible to everyone.
> Currently, it's not: There are about 5 billion internet users worldwide, but only an estimated 25 million software developers. That's a "Programming Literacy rate" of less than 1%. Furthermore, that population is not demographically representative. It skews heavily toward men, the Global North, and those from privileged socioeconomic or ethnic backgrounds. This is a disgrace. It is if we live in some absurd dystopia where only people with green eyes play music
But I don't think that math education is generally very successful at teaching people math, as described in Lockhart's Lament: https://www.maa.org/sites/default/files/pdf/devlin/Lockharts...
My suspicion is that a big part of the issue is the way math is presented early on is really tedious and boring to a lot of people, in a way that could be addressed by theorem provers. I think something like the Xena Project https://xenaproject.wordpress.com/what-is-the-xena-project/ is potentially an interesting development in that regard (though more for undergraduate math than grade school math).
I also don't think this is anyone's "fault" really. I'm more interested in figuring out what might make things better than assigning blame. Nor do I think I personally can fix it single-handedly with a new programming language. If Yatima can move the ball forward a little bit by eventually contributing to a few people learning and falling in love with programming and math, that's more than enough for me.
Certainly not to the degree required to use this programming language :)
> But I don't think that math education is generally very successful at teaching people math
I agree, but the most likely hypothesis that I am forced to adopt given the available evidence is that this has very little to do with how math is taught and a great deal to do with the fact that aptitude in many subjects is largely heritable.
I think there are serious benefits to be harvested from improved pedagogy, but almost entirely at the top end. A worthwhile goal, certainly, but only going to exacerbate the state of affairs you’re objecting to.
> I'm more interested in figuring out what might make things better than assigning blame
A worthwhile goal, but I don’t think a new dependently typed functional language is likely to cause any marginal changes in the direction you’ve stated a preference for. Probably the exact opposite direction, if anything.
What I was trying to get at more was that, from the readme, there's nothing there to get me to understand what exactly I'm looking at (ie: code samples, a few examples of what you might make with it, ect). Hard to get onboard with a project if there's no way to really tell how you'd go about using it.
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
This sounds like an invitation and a challenge, I might dig around your repo and see what's what. Good luck with the project!
If you wanted to bring in new people wouldn’t it be more effective to make a python for beginners and children youtube course?
Why not build a GPT-3 to python code generator?
Please never do that last one, actually, you’ll make everyone here unemployed.
Sorry if I sound hostile. Really not meant to seam that way. English just isn’t my first language.
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 people that kind of language is fine. Those people are already well served by existing resources.
The people I want to reach are people who have not yet been exposed to a presentation of mathematics or computer science as an elegant unified field, where proofs are programs and theorems are types. This is what I would have responded well to as a kid who detested Math and CS well into my late teens. Much of what is marketed as "accessible" or "educational" in programming languages comes across as patronizing, a lot of visual programming languages are guilty of this. That approach would also not have worked for me.
So what I'm doing instead is building a language that I would thought was awesome when I was 12. Will that work for everyone, who knows? Probably not. But it would have worked for me, and if there are other people out there in the same situation, then that's good enough motivation for me to keep building.
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 languages. Right now, the closest comparison to your prospective design for Yatima might actually be ATS, and I have trouble seeing ATS as figuring in a "Programming 101" tutorial.
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.
Do you think the math emphasis of your language would make it an especially good introductory language for mathematicians?
(I'm in the "thinking about it in every free moment" stage of jumping into a project using Rust on both the backend and the frontend via wasm-pack. Is Yatima intended purely/mostly for web assembly/frontend use, or would writing both front and backend in Yatima be a project goal?)
In some sense, Yatima's trying to be to Rust what Haskell is to C. We reuse a lot of the primitives (like ints, uints, chars, etc), but in a separate runtime layer that lets you just use a lambda like a lambda, and not have to worry if you're recursing too much. Now, that comes with overhead, but in a lot of places (like on the web) that's acceptable.
Another thing to think about is determinism. One goal of Yatima is to have each content-id always run the same way given the same inputs. That means we have to forgo using things like hardware floats (or at least not without some complex wrapping) which can cause UB if you try to read their bits (even in WASM).
I think definitely we're going to want to explore both frontend (along the lines of something like https://seed-rs.org/) and backend use cases for Yatima. I'm looking with great interest at https://github.com/lunatic-solutions/lunatic to see if there's a way for us to integrate their lightweight processes. As far as I understand this is along the lines of what https://www.unisonweb.org/ is doing.
The other thing I'm thinking about is smart contracts. Since Yatima is almost `no_std`, we should be able to build it as a pallet for substrate.dev.
Can someone explain to me how C and Haskell are related here ?
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.
Some languages do compile to C (if only for the portability and compiler quality). C++'s first compiler used such a technique.
The comparison to Haskell/C was an imperfect analogy, I was just trying to express that "functional programming language that integrates with Rust" seems like a mostly unfilled niche that Yatima could exist in
That is a steep hill to climb for beginners. Any ideas how to guide them along?
And it is also not clear how programming languages or computing are tied to corporations and not to individuals. There's no contradiction here.
And you need corporations to build the device you are currently using to reply. We do our jobs on the shoulder of giants. Thousands of corporations in a world-wide link that provide the necessary resources and know-how to build computers. Not sure how that rhymes with "computing should belong to individual users".
You know, I've never understood the the "Monad is hard" meme. Monad isn't hard. Functor is hard. Like, really hard, especially when you consider contravariance and covariance. Monad is like a tiny little teaspoon of hard on top of the swimming pool of Functor hard.
But does any of that complexity prevent you from calling `Option::map` in Rust or `Array.prototype.map` in JS? Or from seeing the pattern between them?
"I have an A and a function A -> B, so I can make a B."
"I have a List A and a function A -> B, so I can make an List B."
"I have an Option A and a function A -> B, so I can make an Option B."
"I have an F A and a function A -> B, so I can make an F B."
Is that too steep of a hill for people? I don't think so. It may not be intuitive, but neither is learning to read and write, and it turns out that virtually everyone can do that with enough practice.
Yatima is not an intuitive language, but it is very simple, whereas a language like Python is much more intuitive, but vastly more complicated. My take is that the former set of properties makes for a more learnable system than the latter. Maybe I'm wrong on that, who knows, but to me it seems like a thesis worth exploring.
> And you need corporations to build the device you are currently using to reply. We do our jobs on the shoulder of giants. Thousands of corporations in a world-wide link that provide the necessary resources and know-how to build computers. Not sure how that rhymes with "computing should belong to individual users".
I appreciate the intricate dance of capital behind making the devices we're communicating on. That is not what I'm talking about when I say "computing should belong to individuals rather than corporations." I simply mean that users should have control and agency of what they do on the computing instruments they buy, in the same way they have control and agency of what they do with the writing instruments, or musical instruments they buy.
Or in concrete terms, I have nothing against Apple selling me an iPhone, great piece of hardware. But I do think that once I buy the phone, it's mine and I should be able to run what I want on it, without the phone telling Apple what I'm doing. It's a question of mental autonomy and integrity; I'm extending my mind through the device, so if Apple controls the phone it's like they control a piece of my mind.
For a programming language this philosophy informs a lot of decisions, particularly regarding build system servers. Consider for example that in JS npm is owned by Microsoft, whereas in Rust crates.io is owned by the Rust Foundation. I think the latter is better than the former. But I think the way Yatima's package management works over the decentralized IPFS network is better than either.
Furthermore, the diversity shtick just completely turns me off from this project. I agree with pretty much everything you're saying, too: but putting it in your readme is like putting a sample of your fanfiction in your cover letter; It's unprofessional and gives a lot of people the wrong idea about your efforts.
If you or anyone else is off-put by that or disagrees with it, that's completely your right, and I respect it.
(Also, by the way, a sample of fanfiction in a cover letter sounds awesome, and a great fit for the kind of creative engineering culture I like to be a part of)
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 standard definition of contradiction is "too strong" in its theory, but that appears to be the definition of Empty [2]. What am I missing?
[0]: https://github.com/yatima-inc/yatima#motivation
[1]: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...
[2]: https://github.com/yatima-inc/introit/blob/main/Empty.ya
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
Looking forward to it!
It still feels very experimental is nature and has feel of a side project. Not sure if you guys are pursuing it seriously. If yes, I would recommend you to create more education material. I think it is very radical idea that has a huge learning curve. Also, I would recommending moving the motivation and manifesto to your landing page if any and focus on getting started, setting up your dev environment and how you could run your first application.
Cheers!
This was really tricky, and involved a lot of unsafe Rust, pointer manipulation, etc, but the upshot is that we now have a performant functional programming runtime that can run anywhere WASM can.
The project absolutely is still a little experimental though, and while we do have a full-time team on it, most of the work is happening beneath the surface. But we're definitely planning on having docs, tutorials, a web repl etc. in the near future!
I have only read the first few paras of the readme and I am in love with this language and you already
Thank you for this!
text: leftpad incident
link: https://qz.com/646467/how-one-programmer-broke-the-internet-...
fixed: https://qz.com/646467/how-one-programmer-broke-the-internet-...
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!)
So static typing? Or am I missing something?
But it seems from this thread this caused confusion, so I'll update the README shortly to clarify.
[0]: https://github.com/yatima-inc/introit/blob/main/Map.ya#L10
"First-class types" on the other hand means that types are expressions that can be manipulated at runtime, or by compile-time metaprogramming stage. I think Julia is very much like this: types are very complex expressions and they're expressed with the same machinery as arithmetic expressions (femtolisp).
This is how it works in Yatima. Since we use self-types and lambda-encodings for our datatypes, all type expressions are built up via some combination of self types, pi types and a few type-level constants (like primitives).
For example, the type of booleans can be expressed as:
def Bool : Type =
@self ∀
(0 P : ∀ (Bool) -> Type)
(& true : P (data λ P t f => t))
(& false : P (data λ P t f => f))
-> P self
def true : Bool = data λ P t f => t
def false : Bool = data λ P t f => f
This issue (on improving the test-suite) is a particularly good starter issue: https://github.com/yatima-inc/yatima/issues/37
- A performant lazy functional runtime with sharing implemented from scratch in Rust
- A dependent type system with substructural types
- Parsing, tooling, a standard library, ability to run on the web via wasm
- Content-addressing and serialization to IPLD so that packages can be shared over IPFS
That's what we claim to do in our README, and that's what we do.
It's true that Yatima doesn't have an effect system yet, nor is it production-ready, but it's a pre-alpha programming language project, what's the standard being applied here?
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.