2 ms·
Does distributivity hold? a x (b + c) = a x b + a x c
by hyperpallium 8y ago
Does distributivity hold? a x (b + c) = a x b + a x c
- danharaj 8y agoNot literally, but there is a 1-1 correspondence between terms of the former and terms of the latter. Modulo technicalities in the presence of non-termination.
- evincarofautumn 8y agoUp to isomorphism, yes. That is, you can write a pair of functions that are mutual inverses that witness the fact that those two types are isomorphic: distl :: (a, Either b c) -> Either (a, b) (a, c) distl (a, b_c) = case b_c of Left b -> Left (a, b) Right c -> Right (a, c) factl :: Either (a, b) (a, c) -> (a, Either b c) factl ab_ac = case ab_ac of Left (a, b) -> (a, Left b) Right (a, c) -> (a, Right c) With the “TypeOperators” feature enabled (and “UnicodeSyntax” for pretty arrows and such, because why not), you can write it more literally: type (×) a b = (a, b) infixl 7 × type (+) a b = Either a b infixl 6 + distl ∷ a × (b + c) → a × b + a × c factl ∷ a × b + a × c → a × (b + c)
- yawaramin 8y agoLogically, it would seem to. If you can have an apple and either a ball or a cat, that's logically the same as having either an apple and a ball, or an apple and a cat. In terms of types, they are the same.