3 ms·
> who still cannot formally prove a linked list properly after decades. Huh? Prove what about a linked list? https://www.idris-lang.org/docs/idris2/current/bas
by consilient 3y ago
> who still cannot formally prove a linked list properly after decades.
Huh? Prove what about a linked list? https://www.idris-lang.org/docs/idris2/current/base_docs/docs/Data.List.html https://www.idris-lang.org/docs/idris2/current/base_docs/doc... seems like a perfectly good dependently-typed linked list to me.
- astrange 3y agoWhich makes it useless, since despite their teaching-programming popularity, linked lists aren't actually good for anything. The useful kind is called intrusive linked lists, but nobody teaches those.
- consilient 3y agoIntrusive linked lists trade away simplicity and ease of refactoring for better memory characteristics. There's a huge amount of code where that trade is a terrible deal. Obviously you shouldn't use ordinary linked lists deep in the guts of an OS kernel or automated trading system but claiming that they're useless is absurd.
- astrange 3y agoThe main issue is that a list of pointers is inefficient but also overkill; a small list is probably fine as an array even if you're mutating it. But intrusive lists also have clearer ownership, since the object knows all the lists it can be in, and that's handy sometimes.