[isaac21259]

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 lambdas, pi types, universes, unit, and absurd would take a day or two on it's own. Not to mention Sigma types, co-product types, w-types, identity types, natural numbers, and lists. You also have type inference and evaluation. Also the time spent coming to grips with what all of this means. It's a really cool project but I expect it would take a week minimum to implement this and have a solid understanding of everything you've done.

[caotic123]

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.

[igravious]

A week minimum?

This is such a frustrating space.

The bar for understanding this code and toy project code like this (in this space) is in-depth knowledge of either ML or Haskell (or some functional language with proper built-in functions but generally either ML or Haskell†) … this is key; all these type-theoretic "look at what I built" jaunts leverage these languages.

In this case PomPom says: "The only requisite is cabal and GHC" – which is nothing at all like saying that all you need is C and its standard library.

How long would it take you to write your dependently typed language PomPom in C with just its standard library? If the answer to this is far more than a day then I guess that Cabal (I would capitalise Cabal) and GHC are doing some pretty heavy lifting. I don't think this is me being petty. Why is Cabal needed. Because from looking at the code, at least the parser Parsec. Oh. Ok. Why not say Parsec is needed? It would be weird for me to say that a language I wrote only needed Ruby and Bundler/Rubygems … I mean what would that even mean?

Most everybody else writes "The only requisite is cabal and GHC" as I wrote PomPom in the GHC version of Haskell, you need at least version X.Y.Z of GHC and it relies on the following language features (a,b,c,…)‡ and the following external libraries (A,B,C,…).

So you've written a whole language and, get this, there are no comments in the code about the language syntax and the README jumps straight to "For example proving that inserting a element in any position in a list always returns a non-empty list can be encoded like :" I mean … No, here is the syntax of PomPom. Why? I can only conclude that the syntax does not matter. And isn't it an odd and strange language where the syntax is unimportant?

> Sorry but you cannot implement this in a day.

You're absolutely correct you can't. First of all you need a deep understanding off GHC and its ecosystem. Second of all you need a good grasp of type theory. Then you'd have to figure out the syntax off PomPom, then you'd have to reimplement all the important parsing and type checking bits.

Now say that you wanted to use the esoteric C or one of its super esoteric descendents (C#, Java, C++, Kotlin, Swift, etc.) or you wanted to use something exotic like Rust or Go or even one of those dynamic languages that nobody uses (Javascript, Python, Ruby, etc.) because you didn't feel like learning GHC and its ecosystem. What then?

What I'm trying to get at is that I would respond to the claims in this space that you can build language CoolTypes in X days with a roll of the eyes, or more charitably a raised eyebrow (would respond witth something going on round the ocular area is what I'm getting at).

† Not to mention Coq, or Idris, or LEAN, Agda, or god knows what else

‡ We all know that it's never just GHC, it's always at least version X.Y.Z of GHC with experimental(?) language features a and b and so on enabled.

[caotic123]

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.

[strbean]

"You have to know the language" is a pretty poor criticism IMHO. How are we to gauge time for any such project if we don't assume competency with the language first? How long would it take to make a simple blog? Depends on how long it will take you to learn HTML/CSS/Javascript...

[igravious]

”Pompom language is so simple that you can implement it yourself just by looking in the source code (We have only 1000 lines in the core, you can think that our language is the BASIC language of proof assistants).”

The reason PomPom is so simple and the reason why the basic syntax of PomPom has lambda and abstraction is because GHC gives you that machinery for free, and that's just for starters. Look at how the README is ordered: bunch of verbose language examples, then terse language syntax, then oh by the way you need Cabal and GHC.

Instead of your blog example which I can't quite analogise from … imagine I said that I had an implementation of a cool custom OOP library (let's stick with programming language features) and then said: here are some examples of the code, and here is the syntax, and by the way I used C++ (or some other language that has built-in OOP) and Bison (or some other parser generator), among other things.

What I'm saying is. Where is the simplicity coming from?

Six Haskell files. Checker.HS uses {-# LANGUAGE LambdaCase #-} and has

[dllthomas]

> Checker.HS uses {-# LANGUAGE LambdaCase #-}

Allowing people to write

    \case SomePattern -> ... | OtherPattern -> ...

instead of

    \x -> case x of SomePattern -> ... | OtherPattern -> ...

is not a meaningful change in complexity.

[caotic123]

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.