9 ms·

Yatima: A programming language for the decentralized web

89 points by agentofuser 5y ago

throwaway894345 5y 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 5y 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 https://github.com/yatima-inc/introit/blob/main/Map.ya#L10
- AkshatM 5y 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 5y 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).
  - jcburnham 5y 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 https://github.com/yatima-inc/introit/blob/main/Pure/Bool.ya
    - skulk 5y ago
      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.
      - jcburnham 5y ago
        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.
- jcburnham 5y 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.
  - deleted 5y ago
    [deleted]
trutannus 5y 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.
- jcburnham 5y 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
  - trutannus 5y 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.
phtrivier 5y 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 ?
- jcburnham 5y ago
  Sure, thanks for the feedback. Our standard library is here: https://github.com/yatima-inc/introit 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 5y 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.
    - jcburnham 5y ago
      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.
- _hpb 5y ago
  You must do a Straussian reading of ALL REAMDEs.
SOFAYON 5y 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-by-deleting-a-tiny-piece-of-code/from https://qz.com/646467/how-one-programmer-broke-the-internet-... fixed: https://qz.com/646467/how-one-programmer-broke-the-internet-by-deleting-a-tiny-piece-of-code/ https://qz.com/646467/how-one-programmer-broke-the-internet-...
- jcburnham 5y ago
  Fixed, thank you
deleted 5y ago
[deleted]
penisverse 5y ago
Why not just use Idris 2?
debarshri 5y 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!
- jcburnham 5y 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 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!
creata 5y 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 https://github.com/yatima-inc/yatima#motivation [1]: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta... [2]: https://github.com/yatima-inc/introit/blob/main/Empty.ya https://github.com/yatima-inc/introit/blob/main/Empty.ya
- jcburnham 5y 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 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
ryanmentor 5y 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!
- jcburnham 5y ago
  Thank you!
zomglings 5y ago
This looks fantastic. Are you guys accepting contributions or is it early for that?
- jcburnham 5y ago
  Absolutely accepting contributions, come join our matrix channel: #yatima:matrix.org https://matrix.to/#/!bBgWgXJqeKuDuiUYWN:matrix.org?via=matrix.org&via=kde.org&via=sorby.xyz 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 https://github.com/yatima-inc/yatima/issues/37
wyager 5y 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?
- jcburnham 5y 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 5y ago
Maybe a code snippet on the readme? Just to see what 'feels' like
- jcburnham 5y ago
  Our standard library is here! https://github.com/yatima-inc/introit https://github.com/yatima-inc/introit
matesz 5y 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 :)
- jcburnham 5y 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/059b0abccd0ca54b9a27a1c68f70222394dbe681/core/src/graph.rs https://github.com/yatima-inc/yatima/blob/059b0abccd0ca54b9a.... You can see the output of that here: https://i.redd.it/94zg24fboyv61.png 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 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.rs 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 5y ago
[deleted]
Bissaka 5y ago
Yatima in arabic means orphan. Was this intentional?
- jcburnham 5y 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 https://en.wikipedia.org/wiki/Lisp_machine, and to Haskell's "orphan instances" https://wiki.haskell.org/Orphan_instance https://wiki.haskell.org/Orphan_instance.

89 points by agentofuser 5y 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 5y 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 https://github.com/yatima-inc/introit/blob/main/Map.ya#L10
AkshatM 5y 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 5y 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).
- jcburnham 5y 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 https://github.com/yatima-inc/introit/blob/main/Pure/Bool.ya
  - skulk 5y ago
    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.
    - jcburnham 5y ago
      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.
jcburnham 5y 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.
- deleted 5y ago
  [deleted]

trutannus 5y 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.

jcburnham 5y 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
- trutannus 5y 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.

phtrivier 5y 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 ?

jcburnham 5y ago
Sure, thanks for the feedback. Our standard library is here: https://github.com/yatima-inc/introit 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 5y 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.
  - jcburnham 5y ago
    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.
_hpb 5y ago
You must do a Straussian reading of ALL REAMDEs.

SOFAYON 5y 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-by-deleting-a-tiny-piece-of-code/from https://qz.com/646467/how-one-programmer-broke-the-internet-... fixed: https://qz.com/646467/how-one-programmer-broke-the-internet-by-deleting-a-tiny-piece-of-code/ https://qz.com/646467/how-one-programmer-broke-the-internet-...

jcburnham 5y ago
Fixed, thank you

deleted 5y ago

[deleted]

penisverse 5y ago

Why not just use Idris 2?

debarshri 5y 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!

jcburnham 5y 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 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!

creata 5y 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 https://github.com/yatima-inc/yatima#motivation [1]: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta... [2]: https://github.com/yatima-inc/introit/blob/main/Empty.ya https://github.com/yatima-inc/introit/blob/main/Empty.ya

jcburnham 5y 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 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

ryanmentor 5y 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!

jcburnham 5y ago
Thank you!

zomglings 5y ago

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

jcburnham 5y ago
Absolutely accepting contributions, come join our matrix channel: #yatima:matrix.org https://matrix.to/#/!bBgWgXJqeKuDuiUYWN:matrix.org?via=matrix.org&via=kde.org&via=sorby.xyz 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 https://github.com/yatima-inc/yatima/issues/37

wyager 5y 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?

jcburnham 5y 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 5y ago

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

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

matesz 5y 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 :)

jcburnham 5y 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/059b0abccd0ca54b9a27a1c68f70222394dbe681/core/src/graph.rs https://github.com/yatima-inc/yatima/blob/059b0abccd0ca54b9a.... You can see the output of that here: https://i.redd.it/94zg24fboyv61.png 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 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.rs 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 5y ago

[deleted]

Bissaka 5y ago

Yatima in arabic means orphan. Was this intentional?

jcburnham 5y 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 https://en.wikipedia.org/wiki/Lisp_machine, and to Haskell's "orphan instances" https://wiki.haskell.org/Orphan_instance https://wiki.haskell.org/Orphan_instance.