What does a pipe in a class definition mean?

Actually, it’s a “functional dependency”. In this case that means that m uniquely identifies w — the type m determines the type w. (This may be a better link.)