Yes. Compare also https://www.khoury.northeastern.edu/home/cmartens/Courses/74... where the abstraction itself mechanically enforces certain guarantees and contracts.
The more a language is mathematically sound, the more its linguistic constructs converge to enforce same.
Programming languages which follow this path ultimately support similar capabilities; Applicatives, Functors, Monads, Monoids, and often meta-programming via higher-kinded types and/or intrinsic AST code generation.