Top all-time · #9719
Twan van Laarhoven
Personal blog · twanvl.nl/blogprogrammingmath
Twan van Laarhoven's personal blog at twanvl.nl covers programming and math. Since 2011, 8 different Hacker News readers have linked it 11 times, most often “The complete correctness of sorting (2013)”. The last post was in 2018, but the archive is still widely read.
Too few sampled comments (7) to say how often HN recommends it.?
Why HN links it
HN commenters link this blog as a source for dependently typed examples, such as a verified sorting algorithm in Agda, and for a post on van Laarhoven lenses in Haskell.
Summarised by Claude from a sample of 7 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
Most-linked posts?
- The complete correctness of sorting (2013)3 people · 3 mentions · first linked 2013-05-24
- /blog/agda/sorting2 people · 3 mentions · first linked 2018-05-14
What Hacker News says?
Van Laarhoven lenses were also introduced in a blog post :): http://www.twanvl.nl/blog/haskell/cps-functional-references
Comment linking /blog/haskell/cps-functional-references
on “I think I've solved the Haskell records problem”Submitted Finding rectangles in images using Haskell as a story · 48 points
HN discussionHow are you finding Idris? or are you more in the Agda camp? If you want to definitely rule out as many errors as possible, dependently typed languages are the state of the art, allowing you to write a sort function that will fail to compile if it returns a list that isn't sorted (eg, https://dafoster.net/articles/2015/02/27/proof-terms-in-idri... , or https://www.twanvl.nl/blog/agda/sorting ). After all, if you can…
Comment linking /blog/agda/sorting
on “Trying Out Generics in Go”Submitted The complete correctness of sorting (2013) as a story · 28 points
HN discussion> Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas? Have a look at areas like "cost semantics", e.g. http://lambda-the-ultimate.org/node/5021 This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc. A simplistic way to track…
Comment linking /blog/agda/sorting
on “Total Functional Programming [pdf]”Submitted Knuth-Morris-Pratt in Haskell (2007) as a story · 3 points
HN discussionWe can absolutely use types to ensure that our algorithms are constant time, e.g. https://www.usenix.org/conference/usenixsecurity16/technical... We can use types to enforce the big-O runtime of our functions too, e.g. ensuring that a mergesort implementation runs in O(nlogn) steps: https://www.twanvl.nl/blog/agda/sorting I have no idea about doing these things in Java/C/C++/C# though; anything we try to enforce can…
Comment linking /blog/agda/sorting
on “Leveraging the type system to avoid mistakes”Submitted The complete correctness of sorting in Agda as a story · 1 points
HN discussion> How to do you verify an algorithm? Can you give me an example. Lets say you are trying to come up with some sorting algorithm, and you unknown wrote Bubble sort - how would you go about verifying the algorithm? Verification requires a formal specification, then we follow a fixed set of logical rules to turn the statement 'implementation XYZ matches specification ABC' into the statement 'true'. This won't always be…
Comment linking /blog/agda/sorting
on “The ATS Programming Language”I have implemented KMP in Haskell. This version doesn't use any index! It is built purely functionally by realizing KMP's failure table is just a finite state automaton(well, almost...) However it is much longer than the C++ version... Code: https://github.com/Mgccl/haskell-algorithm/blob/master/KMP.h... Description: http://www.chaoxuprime.com/posts/2014-04-11-the-kmp-algorith... Actually, KMP is a little harder to…
Comment linking /blog/haskell/Knuth-Morris-Pratt-in-Haskell
on “Knuth–Morris–Pratt algorithm”> > It's possible to implement anything correctly with dynamic types but the point is static typing makes it easier to do so > This is where the argument became circular and we can basically stop. I think any appeal to "easier" is inherently subjective. I've certainly tried to avoid making any such claims. Instead, I've mostly tried to argue that static types can forbid certain programs from ever running, and we can…
Comment linking /blog/agda/sorting
on “Are dynamic languages going to replace static languages? (2003)”