| 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. |