I can imagine uses for this where clause in programs other than just explicitly shadowing pattern variables which would otherwise be captured. Not only might we consider definitions in there, like Haskell, we might also consider other bits and pieces. Recall the thorny issue of
[Unparseable or potentially dangerous latex formula. Error 3 : 546x32]
This is a reasonable definition, but it doesn’t make a very good view. What happens? You get a nice case when they’re equal, but when they’re not, the context acquires a proof of difference but you don’t. We could now have
Clearly, such an appeal to the context must be unambiguous, and here it is, because even if we had two proofs of the inequality, they’d be definitionally equal. This brings me back to wondering about a proof language for Epigram, where we invoke a proof (with an irrelevant value) by the proposition it proves, rather than by name. Propositional hypotheses could then be anonymous, and where clauses might be the way to make them explicit.
I think there’s an opportunity to do something very nice here, but I can’t tell what it is yet. I think we should think it out a bit more.
A bit more. Where clauses would give us an opportunity to define previously unheard of symbols showing up in right hand sides. Interactively, one might invoke an undefined function: the system could respond by opening a where clause with a template for its definition. Moreover, if the invocation constitutes a Miller pattern, the type of the local function can be plausibly inferred. As a piece of programming language syntax, this makes some sort of sense, but the question is what to call the local function globally, when it shows up in the normal form of a computation on open terms. I have some ideas about that, but their distinctly underdone.
![\[
\begin{array}[t]{rl}
\textsc{Small} := & (\left< \textsc{Field}\right>^{;\ast}) \\
| & \textsc{Var} \\
| & \texttt{\_} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]](../epilogue/latexrender/pictures/8a29f62a4fc3cb082a155cc82af254e4.png "\[
\begin{array}[t]{rl}
\textsc{Small} := & (\left< \textsc{Field}\right>^{;\ast}) \\
| & \textsc{Var} \\
| & \texttt{\_} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]")
![\[
\begin{array}[t]{rl}
\textsc{Field} := & \left< \_\right>^{?}\:\left< \textsc{Pat}\texttt{=>}\right>^{?}
\: \textsc{Term} \left< \texttt{:}\textsc{Term}\right>^{?} \\
\end{array}
\]](../epilogue/latexrender/pictures/d1f83a2bdab388b205ffc92c4d8c7434.png "\[
\begin{array}[t]{rl}
\textsc{Field} := & \left< \_\right>^{?}\:\left< \textsc{Pat}\texttt{=>}\right>^{?}
\: \textsc{Term} \left< \texttt{:}\textsc{Term}\right>^{?} \\
\end{array}
\]")
![\[
\begin{array}[t]{rl}
\textsc{Term} := & \textsc{Small}^+ \\
| & \textsc{Bop}\: \textsc{Sig}\: \textsc{Rhs} \medskip \\
\end{array}
\]](../epilogue/latexrender/pictures/467f764add2bf75b1c1e82f4b1479064.png "\[
\begin{array}[t]{rl}
\textsc{Term} := & \textsc{Small}^+ \\
| & \textsc{Bop}\: \textsc{Sig}\: \textsc{Rhs} \medskip \\
\end{array}
\]")
![\[
\begin{array}[t]{rl}
\textsc{Var} := & \textsc{Id}\left< {{}^{\wedge}\textsc{Nat}}\right>^? \medskip \\
\end{array}
\]](../epilogue/latexrender/pictures/bcb81a9f2504cacbc5266575a86c5224.png "\[
\begin{array}[t]{rl}
\textsc{Var} := & \textsc{Id}\left< {{}^{\wedge}\textsc{Nat}}\right>^? \medskip \\
\end{array}
\]")
![\[
\begin{array}[t]{rl}
\textsc{Bop} := & \texttt{lam} \\
| & \texttt{all} \\
| & \texttt{ex} \\
\end{array}
\]](../epilogue/latexrender/pictures/dc0160e9f40613fbea5974bd3f4091c1.png "\[
\begin{array}[t]{rl}
\textsc{Bop} := & \texttt{lam} \\
| & \texttt{all} \\
| & \texttt{ex} \\
\end{array}
\]")
tiles
plugin to pull off crazy stunts such as:![$\bfig \Vtrianglepair/>`<-`>`..>`>/[A`A+B`B`C ;\mathrm{inl}`\mathrm{inr}`f`{[f,g]}`g] \efig$](../epilogue/latexrender/pictures/c4edd86d0ed7e809845784ea79c7093d.png "$\bfig \Vtrianglepair/>`<-`>`..>`>/[A`A+B`B`C ;\mathrm{inl}`\mathrm{inr}`f`{[f,g]}`g] \efig$")
