Functional programming largely treats data types without a notion of inheritance and is largely based in invariance and ad-hoc extension but the subtyping rules can be encoded as bounds if the system is strong typed like Kotlin. Mixing FP and OOP concepts and patterns can be even be formally verified . If anyone is interested what a simplified version of the formal rules of subtyping are here is a script in smtlib that helped me understand them. Warning LISP ahead:

For those with parens allergy

yes so everything is Any? in Kotlin terms

lines 5-7 is if x is a subtype of y and y is a subtype of z, x is a subtype of z (transitivity)

yes, the rest is to demonstrate array-of which would be a simple constructor like any other in the lang