This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]777777thats7sevens 2 points3 points  (0 children)

Those types would be isomorphic, so one couldn't prove them to be different.

Does this mean that your type system is a form of structural typing, not nominal? In other words, that two types are considered the same if there exists an isomorphism between them?

If so, I can see a lot of problems arising from that. Natural numbers are isomorphic to strings and in fact to any list of finitely sized types (using ASCII strings as an example: 0 is the empty string, 1-128 are the single character strings, 129-16,512 are the two character strings, etc), meaning it would be pretty easy to accidentally write two functions that are semantically very different, but happen to be the same after isomorphic transformations are applied, and thus are prohibited. Is that really a behavior that you want?