Yatima: A programming language for the decentralized web(github.com)
github.com
Yatima: A programming language for the decentralized web
https://github.com/yatima-inc/yatima
66 comments
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
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
> We really do need to write an actual paper for Yatima's theory though
Looking forward to it!
Looking forward to it!
> First-class types. This lets you the programmer to tell the compiler what you intend to do in your program. Then, like a helpful robot assistant, the compiler will check to make sure that what you're actually doing matches those expressed intentions.
So static typing? Or am I missing something?
So static typing? Or am I missing something?
Their explanation is reductive, but it looks like more than that. For example, in the standard library [0] the definition of the Map type is a function of other types.
[0]: https://github.com/yatima-inc/introit/blob/main/Map.ya#L10
[0]: https://github.com/yatima-inc/introit/blob/main/Map.ya#L10
They mean dependent types, in the Idris sense. Basically, types (not just instances of types i.e. the entire collection `int` rather than 5) are first-class citizens that can be passed to functions. It enables proof checking as well as so-called "type-driven development".
Yeah to me that description sounds like "static type checking".
"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).
"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).
> 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:
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
What is 'Type'? Is it a Type as well? In a toy dependent type system I'm building I just declared the top type as an instance of itself without caring about soundness. I'm curious what the approach is here.
Type is a builtin currently, with `Type : Type`, which makes the type system unsound. There are a couple ways of addressing that that we've explored, like the standard universe polymorphism hierarchy of `Type 0 : Type 1 : Type 2 ...`, but we've also looked at more exotic solutions like whether there's actually a self-type lambda encoding of `Type` itself (which would allow for `case` matching on `Type`). Haven't quite figured it out though, so for the moment `Type : Type` is an acceptable shim while we work on getting everything else working.
Hi, Yatima co-author here, this paragraph refers broadly to static dependent types, like in Idris, but I described them as "first-class-types" here because I thought it sounded more accessible. Also, becase at the type-level Yatima types are ordinary values, so there's an analogy that can be drawn with first-class functions.
But it seems from this thread this caused confusion, so I'll update the README shortly to clarify.
But it seems from this thread this caused confusion, so I'll update the README shortly to clarify.
[deleted]
From the readme, I can't exactly tell what this is for, why I should use it, or how I should use it. Instead the readme is an expression of the creator's ideology. Nothing wrong with expressing that, but without anything concrete to look at and help me understand this project, it just sounds like another ideologically motivated project looking for a use-case.
Hi, Yatima co-author here, the intended use case is to write portable, safe and efficient programs using Yatima's advance type-system features (dependent types, substructural types, etc) and WebAssembly runtime.
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
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
Bit of feedback: I think it's fine to state your ideals, but this goes a step further and gets pretty ranty and negative, which is off-putting. It's a free internet, so do what you want, but if you want to attract people to your project I think you could word things better without having to compromise your ideals.
Your readme points out that math and computer science are fundamentally very similar, maybe the same - do you also have objections to the fact that math expertise follows a similar distribution to computer expertise? Is this math’s “fault” somehow? You seem to be assuming that the current state of affairs is based on some kind of human failure rather than a natural outcome, but I’m not sure that explanation generalizes. If you really think you can “fix” the distribution of computer experts with a new language, do you think you can “fix” the distribution of math users by expressing math in a certain way?
I think the same problems manifest in math, but to a different degree and in a different way. We do have some expectation of universal mathematics literacy, or at least math is a required subject in most schools around the world.
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.
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.
> We do have some expectation of universal mathematics literacy, or at least math is a required subject in most schools around the world.
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.
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.
One aspect of bad math education is that most folks competent in math can choose a different field than teaching and earn far more, without also figuring out how to motivate children while constrained by bureaucratized pedagogic dogma of the moment. Management is only sometimes a mob-of-children equivalent :-).
Hey, awesome that you replied. There's nothing wrong with making projects based on your beliefs (it's actually pretty cool).
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.
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.
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
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
> 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
This sounds like an invitation and a challenge, I might dig around your repo and see what's what. Good luck with the project!
This sounds like an invitation and a challenge, I might dig around your repo and see what's what. Good luck with the project!
Come join our matrix channel! #yatima:matrix.org https://matrix.to/#/!bBgWgXJqeKuDuiUYWN:matrix.org?via=matri...
How does your language solve that diversity problem?
It looks like a high barrier to entry language like Haskell, Rust or Ocaml.
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.
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 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 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.
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.
> 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 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.
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.
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.
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.
At last I truly see. Thanks.
Do you think the math emphasis of your language would make it an especially good introductory language for mathematicians?
Do you think the math emphasis of your language would make it an especially good introductory language for mathematicians?
What are the benefits of using Yatima over compiling Rust directly too web assembly?
(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?)
(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?)
So, I love Rust immensely, but it's a totally different style of programming than a functional language like Haskell. For example, Rust closures are absolutely not the same as pure functions, and if you try to use them that way you'll have a bad time. Another thing is that Rust's approach to garbage collection is "opt-in" (with Rc, etc), which is great for low-level control, but not so great when you're trying to write high-level or non-performance-critical things. And lastly, recursion is Rust is restricted by the stack, so if you try to recurse too much you'll panic. You can manually increase the stack, of course, but this is again a case of having to explicitly handle your resources.
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.
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.
> In some sense, Yatima's trying to be to Rust what Haskell is to C
Can someone explain to me how C and Haskell are related here ?
Can someone explain to me how C and Haskell are related here ?
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.
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.
Haskell's GHC compiler (eventually) transforms haskell into a "fictional assembly" called C--. It has no relation to C at all except in the generic sense that it's a low-sugar low-semantics low-level language, intended to be a machine-friendly view of high level haskell. Maybe the author meant that relationship in the generic sense. (C--could be transformed to C to be read or compiled, but it could equally be transformed into LLVM IR or native.)
Some languages do compile to C (if only for the portability and compiler quality). C++'s first compiler used such a technique.
Some languages do compile to C (if only for the portability and compiler quality). C++'s first compiler used such a technique.
I wasn't talking about C--, more about how GHC essentially exposes C libs for its primitives. Also want to clarify that Yatima doesn't compile to Rust either.
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
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
I think Yatima's type system is intended to be more powerful than Rust's. In particular, its dependent types would allow the compiler to enforce properties of data at compile time. E.g., it can be used to ensure that function only accepts/returns a list of values of a particular length (aka a vector) at compile time, which afaik isn't possible with Rust's type system.
Oh, yeah, I didn't even mention this on my other comment, haha. Rust doesn't have dependent-types (except outside of a few niche places like const-generics) and only limited/non-user-exposed sub-structural types. There's a whole range of interesting applications that that those features open up, from compiler optimizations to formal verification.
I find it hard to reconcile these goals with the language you created: Monads, applicatives etc:
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".
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".
> I find it hard to reconcile these goals with the language you created: Monads, applicatives etc
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.
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.
I applaud your efforts here, but programming languages that put humans first put computers last. I remember when Java was taking off, people rejoiced worldwide, all under some false pretense that the "human came first". What followed was 20 years of the ugliest bugfixes and slowest programs ever written.
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.
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.
Thanks for the support! I appreciate the difference of opinion here, but for me the "diversity shtick" isn't a shtick. It's a core reason of why I'm doing this project. Our field has big problem: Nearly everyone on the planet uses computers, but relatively speaking almost no one is "computing literate". The opportunity cost of this is just enormous, and I think it's not going to change unless we acknowledge the problem and set a goal to change it. I agree it would certainly be more palatable to just talk about "universal computing literacy" without mentioning the present skewed demographics of our field. But my goal is not to go through life being palatable, I want to actually make a dent in meaningful problems. And in my view, it would be pretty silly to try to solve what's effectively a massive user-experience problem without saying "Our current userbase is X, our desired userbase is Y, how do we get from X to Y?"
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)
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)
Sometimes i feel like an asshole because i want other people not to know how to code so i have less competition
Is Java still an example of an especially "human-friendly" language? That is a strange comparison to me.
I'll be the one to tell it : it's a bit weird for the README of a programming language to have an esoteric quote, pages of prose, links to five research papers / theory books, a flame war on build system, a political manifesto and grand visions about the future of programming, but not a single line of, ahem, the programming language in question ?
(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 ?
(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 ?
Sure, thanks for the feedback. Our standard library is here: https://github.com/yatima-inc/introit, I'll edit the README to make that more prominent
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.
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.
The link is helpful. But just to get a feel for the language it would be nice to have a simple “Hello world” example in the main yatima README.
That makes sense, I'll definitely add a snippet like that to the README once our IO system is finished so you can do a proper side-effecting print of "Hello World" rather than just returning the pure string.
You must do a Straussian reading of ALL REAMDEs.
If you open a link, and it doesn't work, edit the url:
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-...
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-...
Fixed, thank you
[deleted]
I think this is a really cool idea. I think you are guys are upto something. I think you need more example, probably an online editor or tutorial. May be there is some, I couldn't find it easily.
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!
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!
Thanks! We definitely do need to put up more material. This HN post caught us a little unprepared on that front; our focus for the past few months has been on our lambda-DAG reduction system (essentially a Rust implementation of https://www.ccs.neu.edu/home/shivers/papers/bubs.pdf, extended with a type-system), which is the sine qua non of the whole project.
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!
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!
Dear Language Authors
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!
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!
Thank you!
This looks fantastic. Are you guys accepting contributions or is it early for that?
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
This issue (on improving the test-suite) is a particularly good starter issue: https://github.com/yatima-inc/yatima/issues/37
The README makes a lot of bold claims for what, as far as I can tell, seems to be vaporware. Does this language have any kind of effect system yet, or can it only evaluate pure expressions?
"vaporware" is a pretty harsh accusation for a project that has:
- 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?
- 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?
Maybe a code snippet on the readme? Just to see what 'feels' like
Our standard library is here! https://github.com/yatima-inc/introit
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 :)
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 :)
Sure, so I do use petgraph for actually visualizing the lambda DAG graphs, since it's got a very nice graphviz integration: https://github.com/yatima-inc/yatima/blob/059b0abccd0ca54b9a....
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!)
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!)
[deleted]
Yatima in arabic means orphan.
Was this intentional?
Was this intentional?
It's the name of the protagonist from science fiction novel Diaspora by Greg Egan, which is where the quote at the top of the README is from.
> 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.
> 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.
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