3 ms·
> Figure 2. Removing the final element of a singly linked list. Note that both the returned result and list remain mutable, and the returned result is no longer
by Sniffnoy 3y ago
> Figure 2. Removing the final element of a singly linked list.
Note that both the returned result and list remain mutable,
and the returned result is no longer encapsulated by the
linked list, unlike in prior work (e.g., [26, 46]). Note also that
this function returns none on lists of size one, as it would be
impossible to separate the list from its tail in this case.
Huh, now that sounds like a substantial pitfall... any good way around this?
- deleted 3y ago[deleted]
- ObscureScience 3y agoUnless 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?
- jmgrosen 3y agoNo, 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.