Yeah, you could always use a language model to handle the parsing. I think that is the state-of-art of crawling today, but you have to worry about proxies, and rendering pages. But the only API that I know that truly is able to scrape using zero code is datalambda, you contact them at contact@datalambda.tech

There is not much to say about it. If people like monkeys maybe, why not buy a beautiful lambda?

Nobody is buying it. What strategy is left for you?

My intention is more to show the lambda code itself.

That's so cool Victor. I will probably waste some time implementing something using your runtime. So happy to be part of this.

The syntax is also a point of "easy for parse", for sure it can be improved but IDK if just copying the syntax of these languages is the better solution.

Thank you, it is exactly what I was expecting people to understand!

The simplicity comes from picking simple abstractions to build a dependent type checker. If I have decided to put linear types in PomPom, for example, you will probably waste more time implementing it than actually capturing a lot of expressivity. So the point is to pick what you think is better in the trade-off.

Well, it's pretty normal to assume some basic knowledge when you dealing with some specific topic (as type theory), normally people who know dependent types also knows functional programming, GHC, coq, Agda..., the point is if you're this person so you might be able to rewrite PomPom very fast, even if you do not have implemented a dependent type checker before. . And yes, the time you spent working with some project shouldn't matter so much, but a lot of people do not have enough time/motivation to work on a toy project for 4 months straight, bringing a choice of working on some project of only a week can improve the experience of language implementers.

Yep, these codifications are just examples of what you can do, as Vmladenov said, try reading the examples above.

Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).

As far i know, pompom has a decidable type check though.

I also recommend the software foundations in coq https://softwarefoundations.cis.upenn.edu/.