Hacker News Reader

Unless length of the list (a "Vector" in typical dependent type nomenclature) I can see the issue.

I have not read the paper, but why is not a the empty list the value that returns None when called with this function? I assume the empty list is still a list in this type system?

View on HN

No, it’s not—-they’re passing in a “node”, not a list, which always contains both a head element and a (nullable) tail pointer. That’s why it can’t separate the head in the case of size one: the node must maintain a non-null head.

Reply on news.ycombinator.com