New answers tagged functional-programming
0
You could do it by making the second parameter of your function function like the index of the summation, and recursively increment this parameter as long as $0 \leq i < n$.
$$f(n, i) = \begin{cases}
1 & \text{if } n =0\\
f(i, 0)\cdot f(n-i-1,0) + f(n, i+1) & \text{if } 0 \leq i < n\\
0 & \text{otherwise}\\
\end{cases}$$
Then $...
6
Without cummulative universes, if you have $A : \mathsf{Type}_3$ then you do not have $A : \mathsf{Type}_7$. Instead, we also have to introduce lifting functions $\iota_{i,j} : \mathsf{Type}_i \to \mathsf{Type}_j$ for all $i \leq j$ and write $\iota_{3,7}(A)$ to port $A$ from the third universe to the seventh one. But this is not all, we also want to know ...
3
Suppose you have X : Type0. What universe can X -> Type0 go in?
It can't go in Type0, because Type0 : Type0 doesn't hold. Universes are presumably closed under function types, so we'd hope it can go in Type1 because Type0 : Type1. But without the subtyping rule, we don't know that X : Type1, we only know that it is in Type0.
Now, you could instead say ...
0
AFAIK, the meaning of the term “declarative vs. imperative” changed over time. The original meaning is what you cited, “how vs. what”. This distinction is philosophical, so its meaning varies from person to person. To be honest, after all these years, I failed to understand it, so I will not discuss it here.
A more specific meaning of “imperative” emerged: ...
Top 50 recent answers are included
