Why the inverse function does not mean isomorphism

Let's say I have two functions with a name f :: a -> band it is the reverse g :: b -> asuch that f . g ≡ id.

Now not g . f ≡ id? (Which means isomorphism)

I tried to write a similar example and came up with the following:

myRead :: String -> Int
myRead = read

myShow :: Int -> String
myShow = show

In ghci:

λ> myRead . myShow $ 3
3
λ> myShow . myRead $ "33"
"33"

But it seems that the inverse function does not imply isomorphism . So can someone point me to what I am doing wrong here?

+4
source share
3 answers

Here is a really trivial example. If it Ais a set {1,2}and a Bset {1}, then the functions:

f :: A -> B
f = const 1

g :: B -> A
g 1 = 1

are relevant f . g = id, but not relevant g . f = id. Counterexample -

g (f 2) = 1

, , f . g = id g . f = id, . , , , .

, . , - , .

, ... , .


. - i () , i . i = i. , f . g = id, g . f , :

i . i = (g . f) . (g . f) = g . f . g . f = g . (f . g) . f = g . f = i

- f :: A -> B " " inv f :: B -> (A -> Bool).

inv :: Eq b => (a -> b) -> b -> a -> Bool
inv f b a = f a == b

codomain B A, A B, partition A ( ).

g :: B -> A , g b inv f b (.. inv f b (g b) == True B),

f . g == id

, A B, . , g B A, f .

, "" .

+15

g :: X -> Y , f :: Y -> X. , g f.

g maps X to Y, which reverses some function f from Y to X, shown in orange

, y y x x, f. g, x x y y, g . f == id. x y, y x (.. ). ( , g - ).

+3

, myRead . myShow ≡ id,

(myShow . myRead) "0xFF" = "255"

so myShow . myRead ≢ id, :

A type Inthas a finite number of values, and it Stringis infinitely many, therefore, if you can go from Intto Stringand back, going from an infinite type Stringto a finite type, you Intmust discard the information, so you cannot always return to the original line, and therefore it is impossible to construct an isomorphism between Intand String.

+2
source

Source: https://habr.com/ru/post/1540761/


All Articles