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

21–30 of 67 posts

Re: Yatima: A programming language for the decentralized web

#21

Post by jcburnham »

skulk wrote: post #17
jcburnham wrote: post #8

Earlier quoted context omitted.

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

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.

Re: Yatima: A programming language for the decentralized web

#22

Post by creata »

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

Re: Yatima: A programming language for the decentralized web

#23

Post by trutannus »

jcburnham wrote: post #10
trutannus wrote: post #5

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

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.

Re: Yatima: A programming language for the decentralized web

#24

Post by jcburnham »

debarshri wrote: post #16

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…

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!

Re: Yatima: A programming language for the decentralized web

#25

Post by brundolf »

jcburnham wrote: post #10
trutannus wrote: post #5

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

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.

Re: Yatima: A programming language for the decentralized web

#26

Post by bigiain »

jcburnham wrote: post #10
trutannus wrote: post #5

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

Re: Yatima: A programming language for the decentralized web

#28

Post by jcburnham »

trutannus wrote: post #23
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…

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

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

Re: Yatima: A programming language for the decentralized web

#29

Post by smoldesu »

jcburnham wrote: post #10
trutannus wrote: post #5

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

Re: Yatima: A programming language for the decentralized web

#30

Post by nicoty »

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

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.
Post reply on HN