Yatima: A programming language for the decentralized web

by agentofuser • 5 years ago

89 62 5 years ago

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?

nxrabl• 5 years ago

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

AkshatM• 5 years ago

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

chubot• 5 years ago

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

jcburnham26• 5 years ago

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

from https://github.com/yatima-inc/introit/blob/main/Pure/Bool.ya

jcburnham26• 5 years ago

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.

trutannus3• 5 years ago

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.

jcburnham26• 5 years ago

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

trutannus3• 5 years ago

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.

brundolf• 5 years ago

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.

bigiain• 5 years ago

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

smoldesu• 5 years ago

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.

wyager3• 5 years ago

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?

qualudeheart3• 5 years ago

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.

beders• 5 years ago

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

phtrivier• 5 years ago

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 ?

jcburnham26• 5 years ago

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.

asimjalis• 5 years ago

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.

_hpb• 5 years ago

You must do a Straussian reading of ALL REAMDEs.

SOFAYON• 5 years ago

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

jcburnham26• 5 years ago

Fixed, thank you

debarshri• 5 years ago

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!

jcburnham26• 5 years ago

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!

creata2• 5 years ago

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

jcburnham26• 5 years ago

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

creata2• 5 years ago

We really do need to write an actual paper for Yatima's theory though

Looking forward to it!

ryanmentor• 5 years ago

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!

jcburnham26• 5 years ago

Thank you!

zomglings• 5 years ago

This looks fantastic. Are you guys accepting contributions or is it early for that?

jcburnham26• 5 years ago

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

wyager3• 5 years ago

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?

jcburnham26• 5 years ago

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

gdsdfe• 5 years ago

Maybe a code snippet on the readme? Just to see what 'feels' like

jcburnham26• 5 years ago

Our standard library is here! https://github.com/yatima-inc/introit

matesz• 5 years ago

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

jcburnham26• 5 years ago

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

Bissaka• 5 years ago

Yatima in arabic means orphan.

Was this intentional?

jcburnham26• 5 years ago

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.

Yatima: A programming language for the decentralized web

Related Stories