2
Czy istnieje nietrywialny typ, który jest równy jego własnej pochodnej?
Artykuł zatytułowany The Derivative of a Regular Type to Type One-Hole Contexts pokazuje, że „zamek błyskawiczny” typu - jego konteksty z jedną dziurą - są zgodne z regułami różnicowania w algebrze typów. Mamy: ∂xx∂x0∂x1∂x( S+ T)∂x( S× T)↦ 1↦ 0↦ 0↦ ∂xS.+ ∂xT.↦ ∂xS.× T+ S× ∂xT.∂xx↦1∂x0↦0∂x1↦0∂x(S+T)↦∂xS+∂xT∂x(S×T)↦∂xS×T+S×∂xT\begin{align} \partial_x x &\mapsto …