Re:Show HN: Dependently typed language for proofs that you c...
by spinningslate on Saturday October 02, 2021 @01:18PM
(#28730255)
"smacked in the face" might be a bit extreme, but I can sympathise with GP's point. I read the first line of the first example:
A :: ~ * ~> * => {(list A) :: |new |empty }.
And got stuck at the first hurdle. I started parsing it in my mind and read "A such that tilde star arrow tilde double arrow". I stopped there, and thought "I'm lost". I started trying to interpret it: * might mean wildcard; single arrow could be curried functions (per Haskell). But I don't know what tilde means, nor the double arrow.Now, of course, I can go and look it up: it'll all be defined somewhere. But that first experience - that very first "I've never seen this before, it sounds interesting" hit a road block right there.
Maybe not smacked in the face, but enough friction for me to click the back button.
Re:Show HN: Dependently typed language for proofs that you c...
by vmladenov on Saturday October 02, 2021 @03:37PM
(#28731357)
You can take issue with the order of the presentation but the definition is in the following section. There’s nothing to look up, it’s just an arbitrary choice by the author.
Think about how long it takes to learn a new API or data model. A few minutes to learn a syntax isn't a big deal.