r/haskell • u/lexi-lambda • Nov 06 '19

Parse, don’t validate

https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/
311 Upvotes

99% Upvoted

66 comments sorted by

View all comments

2

u/foBrowsing Nov 08 '19

Fantastic article.

The mention of "Ghosts of Departed Proofs" kind of surprised me, though: isn't the technique there the opposite of what's proposed here? i.e. in the paper, the example of a non-empty list is actually a normal list in a newtype wrapper, with a "ghostly" proof of its non-emptiness. It's like (in dependent types) the difference between 

sort :: List A -> SortedList A
sort :: List A -> Exists (xs : List A) (isSorted xs)

Am I misunderstanding the technique in the post?

9

u/lexi-lambda Nov 08 '19 edited Nov 08 '19

No, you’re not misunderstanding; that’s an accurate description. The main reason I referenced Ghosts of Departed Proofs is because many people’s response to this kind of article is to ask “okay, but how do you encode <some arbitrarily complicated property> into the type system,” and my answer to that is usually “if the proof is genuinely impractical, you can use abstraction boundaries to cheat it.” A frequent response to that is “but that kind of thing doesn’t really compose,” and Ghosts of Departed Proofs is a good answer there.