Yatima W3F Open Grant application

[johnchandlerburnham]

Grant Application Checklist

• The application template has been copied, renamed ( project_name.md) and updated.
• A BTC or Ethereum (DAI) address for the payment of the milestones is provided inside the application.
• I have read and acknowledged the Terms and Conditions.
• The software delivered for this grant will be released under an open-source license specified in the application.
• The total funding amount of the project is below USD $30k for initial grant applications and $100k for follow-up grants.
• The initial PR contains only one commit (squash if needed before submitting your PR).
• The grant will only be announced once the first milestone has been accepted.

[CLAassistant]

All committers have signed the CLA.

[semuelle]

Hi John, thank you for your application. Looks very interesting! We will properly review it as soon as possible.

[Noc2]

Thanks for the application. This sounds really interesting, especially your last milestone. Are you aware of https://rs-ipfs.github.io/offchain-ipfs-manual and https://github.com/rs-ipfs/substrate/tree/offchain_ipfs or https://github.com/ipfs-rust/libipld (also see ipld/libipld#32 (comment))?

[Noc2]

Could you also share your previous work for the IOTA and Ethereum foundation? I would also be interested in learning more about your long term plans. Do you potentially want to create a parachain based on this yourself?

[johnchandlerburnham]

Are you aware of https://rs-ipfs.github.io/offchain-ipfs-manual and https://github.com/rs-ipfs/substrate/tree/offchain_ipfs or https://github.com/ipfs-rust/libipld (also see ipld/libipld#32 (comment))?

Yes, offchain-ipfs is a really cool project, and we actually tried integrating with that and rs-ipfs first. Unfortunately we ran into some issues, and it was unclear how mature and active the development of those projects are. So rather than take on unknown technical debt we decided to fork libipld directly for the serialization/deseraliaztion and CID construction functionality we immediately needed for Yatima. This does require that if we want to actually store/distribute Yatima programs over IPFS we have to use an external IPFS node, like go-ipfs or js-ipfs, which wouldn't be advisable in a Substrate context. So the comment that you linked to seems right to me, the correct long term solution is to have an embeddable ipfs node in Substrate that shares the DB and networking. That's a very worthy engineering effort that we're 100% interested in contributing to.

For the immediate Yatima MVP though, it's not technically necessary, since we keep an internal store of:

/// A map of content-ids to defs, with content ids for the def
pub struct Defs {
  pub defs: HashMap<Cid, Def>,
  pub names: HashMap<Name, Cid>,
}

Which means you can parse, check and eval Yatima expressions packages locally just like any other language. But yeah, to make Yatima a practical smart contract language on Substrate it's going to be much more efficient to use the Substrate db.

Could you also share your previous work for the IOTA and Ethereum foundation?

Sure, so Gabriel Barreto and I previously coauthored the Formality proof language, which was supported by an Ethereum grant. Our work on Formality was an important foundation for Yatima's type theory (though not its implementation or runtime, which are novel), so we wanted to make sure to acknowledge their support. Our DevCon5 presentation on Formality is here, and our other coauthor Victor Maia is continuing the Formality project here, rebranded to Kind Language.

The IOTA Foundation gave us a grant to develop Yatima and explore integrating it with their WASP node for WASM smart contracts: https://github.com/iotaledger/wasp. Our work on the latter, where we successfully got the language building in WASP-compatible WASM, is here. We hope to continue that work at some point in the future when WASP stabilizes more.

I would also be interested in learning more about your long term plans. Do you potentially want to create a parachain based on this yourself?

Absolutely, and we think that would be a great way to both drive adoption of Yatima and give us the resources to continue development. Ideally we'd like to eventually bid for one of the Polkadot parachain slots, but since that's a scarce resources we'd also be fine with a bridge or parathread, or even supporting other chains that want to integrate Yatima.

However, we do believe that a Yatima-specific parachain is an interesting solution architecturally, since there's a possibility of using the sharing in the Yatima runtime on a global-level across an entire block. For example, if I have a transaction that computes some expensive function f(a) and you have a transaction that computes the same f(a) in the same block, then with sharing we should be able to have f(a) computed only once for that block, which will save significant resources. We currently do something similar across package import boundaries (whole program optimization), although this is still rudimentary compared to e.g. GRIN

Other plans we have include adding green-threads to the language by integrating with the Lunatic VM: https://github.com/lunatic-solutions/lunatic, or exploring frontend development with something based on the https://seed-rs.org/ model.

The end goal is to have be able to use Yatima for full-stack type-driven development, whether you're writing code on the frontend or backend, on-chain or off-chain.

[Noc2]

Thanks for the detailed information. I’m happy to support your project and will share it with the rest of the team.

[mmagician]

It's indeed an interesting proposal. I've got a few conceptual questions:

1. I'm having a hard time imagining how using Yatima would work in practice. If it compiles to WASM, would a developer be able to use pallet-contracts to upload the WASM blobs there directly, so that the pallet executes these? (so in this scenario, it would be equivalent to a smart contract programming language like ink!)

2. You mention an idea of potential integration with ink! - so could you call/delegate some logic from within an ink! contract to Yatima?

3. Smart contracts are, among other things, a tool for writing & reading on-chain storage. How will you handle that? I guess this is not covered by the scope of the grant?

4. We will create a Substrate module that will allow for parsing, typechecking and evaluating Yatima language expressions

But it won't evaluate these expressions directly on Yatima, but rather execute the WASM that Yatima compiled to, right? Which would clash with the idea from point 1 -> so I guess I'm missing something here.

[johnchandlerburnham]

@mmagician

1. ... If it compiles to WASM, would a developer be able to use pallet-contracts to upload the WASM blobs there directly, so that the pallet executes these?

There's a distinction between running Yatima on WASM via the compiled Yatima runtime vs directly compiling a Yatima program to a WASM binary. Currently we do the former, which is loosely analogous to how when you compile Haskell with GHC, your binary has the GHC runtime system which does garbage collection, FFI, concurrency, etc. (although the Yatima runtime is much slimmer than the GHC RTS, since our lambda-DAG machine is basically a pointer graph). So you wouldn't want to package the Yatima runtime inside a (runtime + program) WASM blob that gets executed by pallet-contracts, rather you'd want to extend pallet-contracts with a library sp_yatima that lets it directly interpret a Yatima program.

The other approach is to compile a Yatima program directly to WASM without any runtime. This can be done with techniques like lambda lifting, but requires statically determining allocation and freeing. There are some interesting projects like the neut language that show how this can be done with dependent types. And of course the Rust borrow checker is the best example of using substructural types for this. Yatima has both dependent and substructural types, so we think producing no-runtime WASM or x86 binaries from Yatima is certainly an exciting future possibility, but we're not quite there yet.

Even if we had direct compilation though, we would still want to package the Yatima language core inside Substrate so that we could have the ability to parse and typecheck the language on-chain, which opens up the possibility of having a trustless formal verifier contract.

2. You mention an idea of potential integration with ink! - so could you call/delegate some logic from within an ink! contract to Yatima?

This is another benefit of having the language core as a library. We currently have a yatima! Rust quasiquoter macro that would you do something like:

let x: u64 = 1;
let f: Term = yatima!("(lambda x => U64.add 1u64 x)");
let res: Term = yatima!("($f $x)", f, x).eval();
assert!(res.unwrap(),  2u64)

(The current syntax is a little uglier for this, but it wouldn't take too much work to implement something close to the above)

So we can imagine using Yatima as like a kind of "Rc for closures" within ink! potentially, where ink! would handle the interaction between the contract and the rest of the network, but you could write pure functional expressions via yatima!.

3. Smart contracts are, among other things, a tool for writing & reading on-chain storage. How will you handle that? I guess this is not covered by the scope of the grant?

This is a complicated topic, and I wanted to exclude it from the scope of the current grant because it seemed hard to come up with a great deliverable with the time and resources of the initial Open Grant. But once we have sp_yatima, I want to propose a follow-up for this. My initial idea is to use dependent records to model the common "state + methods" style of smart contracts. (I put a short sketch of how that might look syntactically in a gist, since this comment is getting kinda long)

4. But it won't evaluate these expressions directly on Yatima, ...

I think my answer to question 1 touched on this, but let me know if there's anything I can expand on!

[semuelle]

Excited for this

[Lederstrumpf]

Thanks for the detailed clarifications @johnchandlerburnham!

Your application is excellent and I really look forward to the fruits of your work :)

[github-actions]

Congratulations! As part of the Open Grants Program, we want to help winning teams acknowledge their grants publicly. To that end, we’ve created a badge for projects that successfully delivered their first milestone. Please observe the foundation’s guidelines when making any announcements; in particular, don’t announce the grant publicly before you've completed at least the first milestone of the project.

At that point, we will be happy to collaborate on an announcement about the work you’re doing. Please get in touch with us at grantspr@web3.foundation in case you're interested (at least two weeks notice is preferred).

[johnchandlerburnham]

Thanks everyone!

[RouvenP]

hi @johnchandlerburnham we transferred the payment for M3 today.