Open jamesmckinna opened 1 month ago
Does @gallais 's comment on PR #2440 suggests that changes to intensional/reduction behaviour might be breaking
..., so: v3.0? I confess I'm not entirely clear how we arbitrate on such matters: should we suggest/require that users of stdlib
not depend on computational content of proofs? This feels like a potential minefield... given the rather careful separation of Data.*
into 'definitions' vs. 'properties...?
Hmm, so Total
and Decidable
proofs are somewhat of an exception I feel as they really are used as "real computations" (whatever that means)... Like you, I'm very reluctant to say that we can't change the reduction behaviour of proofs between minor library versions.
Hmm, so
Total
andDecidable
proofs are somewhat of an exception I feel as they really are used as "real computations" (whatever that means)... Like you, I'm very reluctant to say that we can't change the reduction behaviour of proofs between minor library versions.
Cf. #2436 / #2440
In a recent Zulip thread the question was raised as to whether a linear-time implementation of the coercion from
_≤′_
to_≤_
was possible. After some experiments (and not going viarecompute
), I wondered about the following:with (independently useful... for replacing uses of
subst
when dealing with_≤_
...?) linear-time coercions given by:More generally, should we (now start to) reconsider
Data.Nat.Properties
from the perspective of making its proofs (as well as the definitions inData.Nat.Base
) more computationally efficient?NB further optimisation may be possible in the base case
by fusing
cast-≤ʳ
and the (linear-time!) call tom≤m+n _ o
... but I think the above is opaque enough already ;-)