[HN Gopher] Yatima: A programming language for the decentralized...
___________________________________________________________________
Yatima: A programming language for the decentralized web
Author : agentofuser
Score : 40 points
Date : 2021-06-07 18:09 UTC (4 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| phtrivier wrote:
| 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 wrote:
| 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 wrote:
| 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.
| debarshri wrote:
| 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!
| trutannus wrote:
| 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 wrote:
| 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
| SOFAYON wrote:
| 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-...
| [deleted]
| penisverse wrote:
| Why not just use Idris 2?
| throwaway894345 wrote:
| > 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 wrote:
| 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 wrote:
| 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".
| jcburnham wrote:
| 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]
| chubot wrote:
| 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 wrote:
| > 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 l P t f => t))
| (& false : P (data l P t f => f)) -> P self
| def true : Bool = data l P t f => t def false : Bool =
| data l P t f => f
|
| from https://github.com/yatima-
| inc/introit/blob/main/Pure/Bool.ya
| skulk wrote:
| What is 'Type'? Is it a Type as well? (Feel free to not
| answer and just link to reading material.)
___________________________________________________________________
(page generated 2021-06-07 23:01 UTC)