caotic123

PyMagic is a library used to write specs/models inspired by model checkers. It can be used to write formal specs and has the benefit to improve LLM-code by reasoning over specs instead of real-world running code.

PyMagic is a library used to write specs/models inspired by model checkers. It can be used to write formal specs and has the benefit to improve LLM-code by reasoning over specs instead of real-world running code.

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

My intention is more to show the lambda code itself.

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

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.

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

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

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

Exactly, it does not necessarily means co-data, thank you for reporting it, i will fix it.

The syntax you presented is really very accessible. Of course, it makes things a little more verbose, but I think you are right, the path for bringing more attention to dependent types is probably making more accessible also. Btw, great article I will have a more detailed look after.

Well, half of it does not have to be necessarily implemented in the core (we are not talking of complex languages like Agda), but yeah, I think if you do not know anything about the PomPom will take some time to finalize it. But I am pretty sure if you have some knowledge about the core you can have a lot of progress in one day.

Also, my current work/job is using Kind as a foundation, the purpose of this language is exactly what you have asked for, give a check on https://github.com/uwu-tech/Kind.

You can always use let (in that our case def) to minimize the problem with inlining. I think functional programmers get used to big expressions because they do not inspect every symbol when they are reading, the context gives enough information! But you are correct, I couldn't make it better than its syntax/semantics because the implementation should be also very simple. And yes, PomPom is very simple compared to other proof assistants (we are not dealing only with functional programming but also dependent types).

I think you misunderstood, I have just made an analogy with BASiC. BASIC is normally a language that students used to implement when they are dealing with compiler topics. The fact is because BASIC is simple to learn and implement in the universe of structural languages. So, what I am saying is that you can do the same thing with Pompom, but of course, aiming at people that have at least a little experience with functional programming and type systems.

Pompom does not offer inductive data types, instead, it provides static symbols (as in the LF framework or λΠ-Calculus Modulo). Of course, we do not use the rewriting foundation of these frameworks, however, we apply a usual unification algorithm to get the same power. There are a lot of things that need proper formalization in the core, but the intention of this work is not it yet. To be fair, not inductive data types as Coq/Agda.