2 ms·
It depends? But it's nice to have the option. DTs doesn't mean everything is proven to the max. Haskell already has a proven `NonEmpty` list without DTs - you
by whateveracct 5y ago
It depends? But it's nice to have the option.
DTs doesn't mean everything is proven to the max.
Haskell already has a proven `NonEmpty` list without DTs - you can prove that with a product type alone :)
And that proof is useful because it allows you to have better proofs down the line. For instance, the min or max of a NonEmpty always exists. But the min/max of a list can be Nothing.