Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Idris: A Language for Type-Driven Development. Parent comment
> since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.
> another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.
Certainly a good suggestion, but, unlike `foo`, not the only one—e.g., `bar xs = length xs + 1` or `bar xs = 2*(length xs)` also work.
> since we know absolutely NOTHING about A, all we can really do is give it back to you, so foo turns out to be identity, or id.
> another might be bar: [A] -> Nat we still don't know anything about A, but we know a little about lists, so a good suggestion might be length.
Certainly a good suggestion, but, unlike `foo`, not the only one—e.g., `bar xs = length xs + 1` or `bar xs = 2*(length xs)` also work.