Tom Doris
3) In type theory, are product types consisting of distinct member types considered special in any way? i.e. does the concept have a name and what special properties do they have?
I don't know about type theory, but I've seen them called 'Type Indexed Products'. See the HList Paper [1] section 7, which refers to [31]. I've found TIP's very successful in practice. They've gotten more rugged through the gradual innovations in type inference that have been introduced into GHC. (Especially the type equality constraint (~), which improves on HList's TypeCast.) But the 'groundness issues' in HList section 9 still apply. Using TIP's relies on overlapping instances (but _not_ necessarily Functional Dependencies), so it's still a 'poor cousin' and (it seems) not to be mentioned in polite company. [1] Strongly Typed Heterogenous Collections, August 2004, Kiselyov/Laemmel/Schupke. [31] Type-indexed Rows, POPL 2001, Shields/Meijer