Does unification of getter and setter have to be lost? Assuming you are in a unityped context, hkts are gone, functor is not a thing. so (a -> f a) -> (s ->

Does unification of getter and setter have to be lost? Assuming you are in a unityped context, hkts are gone, functor is not a thing. so (a -> f a) -> (s -> f s) is not meaningful. If we pretend that unityped means everything is parametrically polymorphic, for the purpose of this discussion, can't we leverage parametricity to choose a representation that provides this unification? for example, if i provide laws that show for a given lens :: (s -> a, s -> a -> s) that (snd lens) s (fst lens $ s) == id s doesn't that provide the same assurance, even if less elegant and not typechecked (the latter of which is much broader than just applicability of lenses)