Let's start with
Type4. I assume that the "lossless" mapping you have in mind is the library function
toList. This will just map a
Map to a corresponding
List containing all key / value pairs from the map. However, this mapping is not enough. You also need to transform all functions involving
Type3 to structure-preserving functions involving
I will try a formal definition but, as said in my comment, I would like someone with more knowledge on this topic to write a better answer.
So, formally, given two types
T2, a homomorphism
h : T1 -> T2 is a pair
(d, f), where
d : T1 -> T2 maps all values in
T1 to values in
f : (T1 -> T) -> (T2 -> T) maps any function
t : T1 -> T to a new function
f t = t' : T2 -> T, such that
t = (f t) . d.
This means that
d maps the data representation from type
T1 to a representation of type
f maps all functions on
T1 to functions on
T2 in a way that preserves the structure.
In your example,
T1 = Map<string, int>,
T2 = (string * int) list, and
d = toList. For all types
T, the function
f should map any function
t : Map<string, int> -> T to a function
f t : (string * int) list -> T in such a way that
t m = (f t) (d m) for each map
For example, the function
isEmpty : Map<string, int> -> bool should be mapped to
f isEmpty = isEmpty' in such a way that if
isEmpty m is equivalent to
isEmpty' (d m). In words: if
isEmpty tells you that a map is empty, then
isEmpty' should tell you that the corresponding list representation is empty as well.
Once you have both mappings (on data and on functions), you can say that the first type is homomorphic to the second.
Two types are isomorphic if there are homomorphisms in both directions.
For your first example, the data mapping function
d : (int * string) -> (string * int) is
d (i, s) = (s, i) and, for all type
T and functions
t : (int * string) -> T, you can define
t' = f t : (int * string) -> T by letting
t' (i, s) = t (s, i). In this way, you can see that
Type1 is homomorphic to
Type2. By defining similar functions in the other direction you can see that
Type2 is homomorphic to
Type1. Therefore the two types are isomorphic.