Your question is related to the concept of full abstraction in programming language semantics. This page [1] is a more trustworthy explanation of it than mine.

Your question is related to the concept of full abstraction in programming language semantics. This page [1] is a more trustworthy explanation of it than mine. TL;DR: if you picture a set whose elements are program fragments and you construct another set whose elements are "meanings" of program fragments (according to you), and you cleverly arrange for a bijective (one-to-one) mapping between those sets (in other words, one that associates a unique meaning with every fragment and vice-versa), then you can say your semantic model is fully abstract. I don't know if anyone uses the term in reference to types, but maybe you could start a trend. [1] https://plato.stanford.edu/entries/games-abstraction/#ProgEquiFullAbst https://plato.stanford.edu/entries/games-abstraction/#ProgEq...