caotic123

6 ms·

1.
by caotic123 3y ago
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
2.
by caotic123 4y ago
My intention is more to show the lambda code itself.
3.
I am selling a lambda expression as an NFT(opensea.io)
3 points by caotic123 4y ago|3 comments
4.
by caotic123 4y ago
There is not much to say about it. If people like monkeys maybe, why not buy a beautiful lambda?
5.
by caotic123 5y ago
That's so cool Victor. I will probably waste some time implementing something using your runtime. So happy to be part of this.
6.
by caotic123 5y ago
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.
7.
by caotic123 5y ago
Thank you, it is exactly what I was expecting people to understand!
8.
by caotic123 5y ago
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 expres
9.
by caotic123 5y ago
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&#x27
10.
by caotic123 5y ago
Yep, these codifications are just examples of what you can do, as Vmladenov said, try reading the examples above.
11.
by caotic123 5y ago
As far i know, pompom has a decidable type check though.
12.
by caotic123 5y ago
Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).
13.
by caotic123 5y ago
I also recommend the software foundations in coq https://softwarefoundations.cis.upenn.edu/ .
14.
by caotic123 5y ago
Exactly, it does not necessarily means co-data, thank you for reporting it, i will fix it.
15.
by caotic123 5y ago
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 a
16.
by caotic123 5y ago
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
17.
by caotic123 5y ago
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 .
18.
by caotic123 5y ago
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 informa
19.
by caotic123 5y ago
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 un
20.
by caotic123 5y ago
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 alg
21.
A dependently typed language for proofs that you can implement in one day(github.com)
134 points by caotic123 5y ago|84 comments