PomPom
Languages and libraries
dependently typed language
SHOW HN2021
138points
96comments
#369of 2,533 in 2021
Top 15%of 2021 by points
How HN took it
RoastedHalf or more of the comments are critical
5 positive, 7 neutral or asking, 0 mixed, 13 critical, out of 25 comments about the project. Thread score -0.36.
Design: 2 for, 5 againstDocs: 0 for, 4 againstIdea: 3 for, 1 againstExecution: 0 for, 2 againstPerformance: 0 for, 1 against
The thread, comment by comment
Each row is a top-level comment and its replies, in HN's order. Select a cell to open that comment on HN.
positive neutral or mixed critical about another commenter or something else the maker
What HN said
What people liked
Simple and accessible design for learning dependent types
From 2 comments
I find the often ML-inspired syntax too high of a bar for most programmers to clear when being introduced to a language. I think a syntax more similar to something like what is…
dwohnitmok on HNAs someone that has very little idea of what all of that is, I think the title is great and certainly made me consider looking into the implementation. It might be wildly…
gpderetta on HN
Objections
Syntax is too complex and hard for programmers to read
From 3 comments
The syntax is quite ... complex, I dare say. It looks like you borrowed from Haskell, which already makes it hard to gain an intuitive understanding of the syntax and added bars?
choeger on HNThe syntax is really bad. And I am familiar with Haskell, Lean, Idris, Agda etc. If the author reads this, I recommend instead copying the syntax used by Lean, Idris, or Agda.…
mbrodersen on HNI’m constantly baffled by what functional programmers call “simple”. I’m sure this language does a lot with little but calling it simple is audacious to say the least. Why do so…
jimsimmons on HN
Cannot be implemented in a day
From 1 comment
Sorry but you cannot implement this in a day. I've written my own language very similar to this and from my experience it takes way longer. Implementing type checking for just…
isaac21259 on HN
Title and claim of simplicity are overstated
From 2 comments
I’m constantly baffled by what functional programmers call “simple”. I’m sure this language does a lot with little but calling it simple is audacious to say the least. Why do so…
jimsimmons on HN> Pompom language is so simple that you can implement it yourself just by looking in the source code (you can think that our language is the BASIC language of proof assistants).…
Twirrim on HN
Requests
Use syntax from Lean, Idris or Agda
From 1 comment
The syntax is really bad. And I am familiar with Haskell, Lean, Idris, Agda etc. If the author reads this, I recommend instead copying the syntax used by Lean, Idris, or Agda.…
mbrodersen on HN
Fix the NonEmpty datatype definition
From 1 comment
The Readme defines: ``` // Data NonEmpty = | New a (NonEmpty a) NonEmpty |A :: ~ * ~> * => {(list A) :: |new}. // A list non-empty is list only with new constructor ``` The…
anfelor on HN
Questions
What foundations does it use and does it support inductive types
From 2 comments
What exactly are the foundations of this? The rules on the page suggest that it is basically the calculus of constructions but the example involving the list suggests that there…
cjfd on HNPompom 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…
caotic123 on HN
How strong normalization is possible given extensional type theory
From 2 comments
>Pompom is an attractive implementation of an extensional (!) dependently typed language >Pompom provides [...] a strong normalization system How is this possible? Extensional…
mbid on HNOh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).
caotic123 on HN
What kinds of proofs are used in real programs
From 1 comment
in practice, what kind of proof are people building when building real world programs ? Are people writing only top level assertion ( such as "this main function always…
bsaul on HN
Alternatives named
Coq
From 2 comments
So, as someone who is curious but have no idea of the theoretical background here.. what should I learn in order to help me understand the code + use this language in a basic…
baddash on HNI also recommend the software foundations in coq https://softwarefoundations.cis.upenn.edu/.
caotic123 on HN
Lean, Idris, Agda
From 1 comment
The syntax is really bad. And I am familiar with Haskell, Lean, Idris, Agda etc. If the author reads this, I recommend instead copying the syntax used by Lean, Idris, or Agda.…
mbrodersen on HN
TLA+
From 1 comment
> So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages. Or…use TLA+,…
erichocean on HN
Kind
From 1 comment
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.
caotic123 on HN