xameerJun 18, 2021
When you sum the elements of a list ( may be by using #recursion , with mconcat #monoid ) , you assume associativity
As in a+(b+c) = (a+b)+c
Which amounts to saying that two trees on the lhs and rhs are identical!
What is the topology of a tree?
Show threadxameerJun 18, 2021
List is recursive To right
To see how associativity matters here think of foldr and foldl
Also
given two lists L, L'
List.append :
If recurse L = empty, result= L'
Else result =tail L
Show threadxameer
In practical terms, without assuming associativity
granting append L ' to the beginning, left, of L O(n^2) does not imply the correctness of append L ' at the end, right , of L , O(n).
Jun 19, 2021 at 7:30amWeb
Show threadxameerJun 19, 2021
Even if you pick the right monoid #homomorphism and have proven that it works* , as you optimize to #refactor , you are assuming associativity
* If I were you, I am not , I d write my own proof checker than, using some library