Functional programming largely treats data types w...

# functional

[raulraja]

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:

subtyping

[pakoito]

For those with parens allergy

[pakoito]

line 4 is all types are subtypes of itself

[raulraja]

yes so everything is Any? in Kotlin terms

[pakoito]

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)

[pakoito]

lines 8-10 is that if a x is a subtype of y and y is a subtype of x, then they're the same

[pakoito]

lines 11-13 is that if x is a subtype of y and z then either y is a subtype of z or z is a subtype of y

[pakoito]

hummm this one I'm curious about

[raulraja]

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

[raulraja]

that one can be omited if you don’t mention arrays

[raulraja]

since all others will still be SAT

[raulraja]

but those are the basic generalized rules of a single inheritance monotone type system for subtyping

[raulraja]

you can try it live in

[raulraja]

https://rise4fun.com/Z3/tutorial

[raulraja]

I Interpret line 11-13 as the upperbound intersection

[raulraja]

so basically widden toward the common upperbound of x, y and z