I am a little confused about the appropriate usage of Polish Notation, (Though I believe it won’t be on the test?)

I will give an example computation to show my understanding, correct me if I do anything wrong:

if f,g : int -> int, h : int -> int -> int, x : int;

h f g x

= (((h f) g) x) (f not in domain of h, interpret it as composition)

= ((h (f g)) x) ((f g) is not in domain of h, interpret it as composition)

= (h ((f g) x)) (g not in domain of f, interpret it as composition)

=(h (f (g x)))

Q1: I don’t remember we have introduce the associativity of (right-)arrow, it is right-associative, correct?

Q2: Any two function, (as long as the one being ‘applied’ is not in domain) can be composed, correct? Even they are not ‘connected’, for example, f: A -> B, g : C -> D, can compose

Q3: How to (Can we) composite two function when the applied one is in the domain of the other?

Q4: if f,g: int -> int, h : (int -> int) -> int, can I write down “h f g”? (I mean the way I want to combine them is that (h (f g))

Q5: What do you think of Type Theory? Mainly, those type systems used by those functional programming languages? For example, Haskell (extended System F) and Coq (Calculus of Inductive Construction). I see that you interpret the notation “int -> int” as a non-deterministic function, and now the “:” is so general that it can be even used to express subtype and typing. Also there is “A: [3*[4 * nat]]” which is only supported in dependent type. What do you think of these theories compared to the theory we are learning?