Re:Show HN: Dependently typed language for proofs that you c...
by dllthomas on Tuesday October 12, 2021 @05:41PM
(#28845426)
> Checker.HS uses {-# LANGUAGE LambdaCase #-}
Allowing people to write
\case SomePattern -> ... | OtherPattern -> ...
\x -> case x of SomePattern -> ... | OtherPattern -> ...
Re:Show HN: Dependently typed language for proofs that you c...
by caotic123 on Sunday October 03, 2021 @04:23PM
(#28740228)
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.
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