Consider any partial function $f \colon \subseteq X \to Y$ for arbitrary sets $X,Y$. Now assume that a total function $g$ takes any such function $f$ as a first paramter and as a second parameter a natural number from $\mathbb N$ and returns an integer from $\mathbb{Z}$. I'm now wondering how the type of $g$ looks like. First I thought about something like that:
$$g\colon \subseteq (X \to Y) \to \mathbb{N} \to \mathbb{Z}$$
I'm wondering if this is the correct notation, i.e., is the subset inclusion $\subseteq$ at the right position? Or is that type to general, i.e., would it mean that $g$ is a partial function---what I assume is the case. Then consider the following type:
$$g\colon (\subseteq X \to Y) \to \mathbb{N} \to \mathbb{Z}$$
Is this the correct notation, i.e., does it mean that $g$ is a total function, i.e., defined for all partial functions $\subseteq X \to Y$ as a first parameter and for all natural numbers as the second parameter?
