%!TEX root = ../Main.tex
\section{Conclusion}

Designing a good programming language involves subtle tradeoffs that are not at all obvious to the casual observer, and often not stated in the final write-up.


Although we could reasonably allow partially applied data constructors by assuming more work is done in the compiler, we would lose the simple canonical forms property that says all values with function type are abstractions. Allowing partially applied data constructors also makes the language asymetric, as the elim-form for data constructors (case expressions) cannot itself destruct a partial application. This second consideration is more personal preference, though. 

Supporting partially applied primops is more of a problem. As primops do not obey the function-call interface, we can't build a standard runtime PAP (partial-application) object to represent them \CITEIT{push-enter}. During compilation we could allow partially applied primops as an intermediate state, but then convert to a saturated form as a final step. However, by doing this the proof would cover the program while it is being transformed, but not while it's being executed! The fact that we have a statement of Progress for a language ensures that primops are never treated as PAPs.


\begin{itemize}

\item \CITEIT{Santos} treats program transformation only, and does not include an explicit evaluation semantics. Santos assumes that the compiler will only substitute atoms because this guarantees that work will not be duplicated at runtime.

\item The current verison of GHC allows general application, though does not explicitly require data constructors to be fully applied during transformation. However, primops must be fully applied, and if in the simplified program they are not they are eta-expanded before code generation.

\item Yes, proving a more general language is harder, but at least in the case of a-normalization and algebraic data we have factored out most of the pain into a reusable library.
\end{itemize}
