Notation for dependent function type Very often (really, very often), when declaring the type of a function, I find the common mathematical notation lacking. And I wish for a way to express the type more precisely.
Assume we have some set $X$, and there is some function $f$ that takes a (non-empty) subset of $X$ and maps it to an element of that subset.
Using common notation, we could introduce $f$ as $f \colon 2^X \to X$.
But we know more! We know that the application of $f$ must return an element of the argument.
Using some made-up notation, we could write $f \colon (A \colon 2^X) \to A$, giving the name $A$ to the argument of the function, and reusing it as the type of the codomain.
So the questions are:


*

*Is there some accepted convention for expressing these dependent types?

*Assuming not, is the proposed notation readable and intuitive? Personally, I find it confusing, as it looks a bit like $f\colon A \to A$.

 A: I think you're basically looking for the notations $$\sum_{x \in X} Y_x \qquad \prod_{x \in X} Y_x.$$ The former means the set of all ordered pairs $(x,y)$ such that $x \in X$ and $y \in Y_x$. The latter means the set of all ways of assigning to each element $x \in X$ a corresponding element of $Y_x$.
For example, a function $f$ that maps each non-empty subset of $X$ to an element of that subset could be denoted $$f \in \prod_{A\in \mathcal{P}_{\neq 0}(X)}A.$$
Some people would call this "type theory", but really it's just set theory.
A: If this type of functions occurs many times in your context you can say the following:
Given a family ${\cal F}$ of nonempty subsets of $X$ a function $f:\>{\cal F}\to X$ satisfying $f(A)\in A$ for all $A\in{\cal F}$ is called a choice function.
A: In mathematical writing, it's not common to think properties like the one you describe as part of the type of the function. The notation $f:Y\to Z$ is essentially only used to denote the domain and codomain of a function (or perhaps a "partial function"), not any extra information.
If the input must be a nonempty subset, and you haven't made it abundantly clear that you're allowing partial functions, then you can't write $f:2^X\to X$ since that would allow an empty subset as an input. 
Depending on what you want to do with functions of this sort, one way to express your idea in mathematical language might be something like:
"Let $f:2^X-\{\emptyset\}\to X$ satisfy $f(A)\in A$ for all $A\in2^X-\{\emptyset\}$."
There are many notational/wording variants, but that should give you some ideas/help you narrow down what you'd like to say.
A: This answer is based on goblin's answer, its comments, and my recent experience.
Product Notation
A function $f \colon A \to B$ is a way of assigning to each element of $A$ (the domain) an element of $B$ (the codomain).
We can also think of this function as a subset of tuples $f \subseteq A \times B$ that has the property that each element of $A$ occurs exactly once as a first (left) entry. Using $\prod$ as quantifier for (cartesian) product, we can write this as
$$f \in \prod_{a \in A} \{a\} \times B,$$
or using index notation
$$f \in \prod_{a \in A} B_a.$$
With this notation, we can formulate more precise codomains for each $a$, e.g., for the general case where $C \colon A \to 2^B$ maps each $a$ to a subset of $B$
$$f \in \prod_{a \in A} C(a)_a,$$
which is more precise than stating $f \colon A \to B$.
Indexed Families
Indexed Families are basically the same as the above product notation — simply using a different notation.
Using an indexed family, we can write
$$f = (B_a)_{a \in A},$$
which means the same as
$$f \in \prod_{a \in A} B_a.$$
Note how both notations contain the same information: $a \in A$ and $B_a$.
When using an indexed family, function application is usually written as $f_a$ instead of $f(a)$, but as both mean the same thing, they are formally interchangeable. Although this might be unexpected for some readers.
Exponential Function Notation As Special Case
Starting from the product notation
$$f \in \prod_{a \in A} B_a,$$
we can remove the index $a$, if the codomain does not depend on the concrete value of $a$:
$$f \in \prod_{a \in A} B.$$
If we rewrite above product in exponential form, we arrive at the (more or less) common exponential function notation
$$f \in B^A.$$
