Comment on Verified dynamic programming with Σ-types in LeanComments−CSMastermind1yI've been meaning to learn Lean and fascinated with the concept but syntax like: let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.−duve021yHey, author here. This is actually not-great style on my part. Is the following better? let rec helperMemo (n : Nat) (map : HashMap Nat Nat) : Nat × HashMap Nat Nat This is how it would usually be written. I will update the post accordingly.−westurner1yDoes aliasing the types work? def MemoMap := HashMap Nat Nat def MemoResult := Nat × MemoMap let rec helperMemo : Nat → MemoMap → MemoResult−tossandthrow1yRecord types would likely help a lot also.Tupples don't really indicate what I can expect from the members.−runeblaze1yTbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard Defn. f: X → Y is flat ⇔ O_{Y,f(x)} → O_{X,x} flat ∀ x. Then immediately I dropped that class. Turns out I like real analysis much more−tikhonj1yWhat makes it hard to parse? The lack of parentheses? The way HashMap Nat Nat is a bit verbose and not clear at a glance? Something else?
Comments
I've been meaning to learn Lean and fascinated with the concept but syntax like:
is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.Hey, author here. This is actually not-great style on my part. Is the following better?
This is how it would usually be written. I will update the post accordingly.Does aliasing the types work?
Record types would likely help a lot also.
Tupples don't really indicate what I can expect from the members.
Tbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard
Then immediately I dropped that class. Turns out I like real analysis much moreWhat makes it hard to parse? The lack of parentheses? The way HashMap Nat Nat is a bit verbose and not clear at a glance? Something else?