Dependent Function

A function where the type of its return value is dependent on the value of its argument. That is, the co-domain is not fixed.

Dependent Function Type ($\Pi$-Type)

The type of a dependent function can be described with this notation:

$${\Pi }_{x\in A}B(x)$$

If B is a constant function, then this type is reduced to ordinary function type $A\to B$

Related

• Dependent Type Theory