Yatima: A programming language for the decentralized web
1–10 of 67 posts
Re: Yatima: A programming language for the decentralized web
#2> 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?
Re: Yatima: A programming language for the decentralized web
#3> 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?
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
Re: Yatima: A programming language for the decentralized web
#4> 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?
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".
Re: Yatima: A programming language for the decentralized web
#5From 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.
Re: Yatima: A programming language for the decentralized web
#6> 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?
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).
Re: Yatima: A programming language for the decentralized web
#7> 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?
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.
Re: Yatima: A programming language for the decentralized web
#8> 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?
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).
> 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
Re: Yatima: A programming language for the decentralized web
#9I'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 ?
Re: Yatima: A programming language for the decentralized web
#10From 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 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