exercise with Distance, foldMap and Maybe for Section 4.3

[Liable5607]

When I was trying to get a handle on Monoids, I spent a lot of time playing with the Distance example. Personally I found that really helpful. One of those practice problems (calculating the Euclidean distance) also involved foldMap and Maybe so I thought it might make a nice exercise.

[stefan-hoeck]

While I like the example for its practical relevance, I don't think that the square of a Distance is still a Distance. At least in physics - where we are strict about this kind of thing - it is not. So, semantically, square and sqrt are not sound. In addition, sqrt is a partial function.

I therefore wonder, if we'd need not explain more about this in order to include it here.

[Liable5607]

Thanks, you're right. I'll try to think of a more sound exercise with these Idris concepts.