Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Yatima: A programming language for the decentralized web

github.com

Post reply on HN
Print view View original

31–40 of 67 posts

Re: Yatima: A programming language for the decentralized web

#31

Post by jcburnham »

bigiain wrote: post #26
jcburnham wrote: post #10

Earlier quoted context omitted.

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 o…

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?)

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.

Re: Yatima: A programming language for the decentralized web

#32

Post by jcburnham »

nicoty wrote: post #30
bigiain wrote: post #26

Earlier quoted context omitted.

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 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.

Re: Yatima: A programming language for the decentralized web

#33

Post by jcburnham »

creata wrote: post #22

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 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

Re: Yatima: A programming language for the decentralized web

#35

Post by ktm8 »

jcburnham wrote: post #31
bigiain wrote: post #26

Earlier quoted context omitted.

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?)

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 wri…

> 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 ?

Re: Yatima: A programming language for the decentralized web

#36

Post by parafactual »

smoldesu wrote: post #29
jcburnham wrote: post #10

Earlier quoted context omitted.

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 o…

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 everyth…

Is Java still an example of an especially "human-friendly" language? That is a strange comparison to me.

Re: Yatima: A programming language for the decentralized web

#38

Post by jcburnham »

smoldesu wrote: post #29
jcburnham wrote: post #10

Earlier quoted context omitted.

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 o…

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 everyth…

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)

Re: Yatima: A programming language for the decentralized web

#39

Post by jcburnham »

ktm8 wrote: post #35
jcburnham wrote: post #31

Earlier quoted context omitted.

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 wri…

> 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 ?

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.

Re: Yatima: A programming language for the decentralized web

#40

Post by Banana699 »

ktm8 wrote: post #35
jcburnham wrote: post #31

Earlier quoted context omitted.

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 wri…

> 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 ?

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.

Post reply on HN