We spent a long time on the choice. But it was really important in this setting to avoid the word "type", and sort is a technically correct term too — e.g., as used in many-sorted logics [https://en.wikipedia.org/wiki/Many-sorted_logic]. Given the precedent from mathematics, it seemed like a pretty good choice (and to me, still does).