A Haskell implementation of Myhill's isomorphism theorem

Myhill.hs

module Myhill where

import Data.List (find)

type N = Integer

-- given injective maps `f, g : N → N` that witness 1-1 reductions `A ≤₁ B` and `B ≤₁ A`, respectively,
-- `myhill f g` computes the graph of a bijection `h : N → N` that witnesses `A ≡ B`, see
-- https://en.wikipedia.org/wiki/Myhill_isomorphism_theorem
myhill :: (N -> N) -> (N -> N) -> [(N,N)]
myhill f g = iterate1 0 [] where
  iterate1 :: N -> [(N,N)] -> [(N,N)]
  iterate1 z lst = if any (\(x,y) -> x == z) lst then iterate2 z lst else (z,y) : iterate2 z ((z,y) : lst)
    where y = search1 z
          search1 x = let y = f x in maybe y (search1 . fst) . find ((==) y . snd) $ lst

  iterate2 :: N -> [(N,N)] -> [(N,N)]
  iterate2 z lst = if any (\(x,y) -> y == z) lst then iterate1 (succ z) lst else (x, z) : iterate1 (succ z) ((x,z) : lst)
    where x = search2 z
          search2 y = let x = g y in maybe x (search2 . snd) . find ((==) x . fst) $ lst

example1 = take 20 $ myhill (\k -> k) (\k -> k)
-- output: [(0,0),(1,1),(2,2),(3,3),(4,4),(5,5),(6,6),(7,7),(8,8),(9,9),(10,10),(11,11),(12,12),(13,13),(14,14),(15,15),(16,16),(17,17),(18,18),(19,19)]

example2 = take 20 $ myhill (\k -> 2 * k + 3) (\k -> k + 1)
-- output: [(0,3),(1,0),(2,1),(3,2),(4,11),(5,4),(6,5),(7,6),(8,7),(9,8),(10,9),(11,10),(12,27),(13,12),(14,13),(15,14),(16,15),(17,16),(18,17),(19,18)]