Should 2 data mappers that type check count as partial "proof" of isomorphism

[strangemonad]

Why might want to sometimes invoke the target language compiler / type checker on a small amount of code.

see #23 #22

eg:

1. infer MyFoo from MyFoo.java

2. When migrating it's valid to either a) replace MyFoo.java with the new generated one or b) marshal between the original MyFoo.java and the generated ModeledMyFoo.java

3. We can generate data mappers to and from MyFoo.java and ModeledMyFoo.java. The fact that these compile is (hand wave) a partial proof of isomorphism between the 2 values. Really we just have functions in either direction but we don't have a perfect guarantee that data isn't lost. (would it be possible to exhaustively unit test the isomorphism in some cases?
   3a) The data mappers aren't needed but it would be nice to compile them once to double check the correctness of the new generated class. Note this is only a crutch (in the way parametricity is a useful property to have) for a really good type checker. We wouldn't want to re-implement a type checker for every target language.
   3b) When marshaling, keep the generated data mappers around. e.g. while still doing data migrations, deserializing old values and then marshaling them to the new modeled value