I find it frustrating how he's against "types" but shows the GCD algorithm where x and y must adhere to a type that can be compared with equality, admits an ord

I find it frustrating how he's against "types" but shows the GCD algorithm where x and y must adhere to a type that can be compared with equality, admits an ordering, and has a subtraction operator. Is the algorithm defined for the reals? Can we use a partial ordering? I'm skeptical of any proposal that seems to have missed even a superficial coverage of existing knowledge/literature on the topic.