assistant-calculus.tex

\section{Assistant Calculus}\label{sec:assistant-calculus}

blah blah blah types
{\fontspec{Symbola}\symbol{"1F4CE}}
{\fontspec{Symbola}\symbol{"1F4CE}}
\paperclip
$\paperclip$

TODOs:
\begin{itemize}
    \item \sout{get cursor icons from hazelnut paper }
    \item \sout{get right arrow for bidi}
    \item \sout{basic zipper cases}
    \item remaining zipper cases? do i need to actually include mirror cases?
    \item \sout{var + varapp}
    \item \sout{NOTE: we basically need a construct expression action for varapp}
    \item \sout{proj}
    \item \sout{base case for hole}
    \item \sout{base cases for non-empty holes, incld:}
    \item \sout{delete + act for general hexps}
    \item \sout{simple wrap for exprs incld. non-empty-holes}
    \item complex (n-ary) wraps
    \item iterated wraps? with cutoffs? (:jean-shorts-emoji)
    \item \sout{are there non-empty-hole suggests distinct from arbitrary expr suggests?} don't think so
    \item \sout{for all: change type to type consistency}
    \item \sout{for all: add numerical subscripts to types where missing}
    \item \sout{fig 4: make it consistency not equal}
    \item \sout{fig 5: change proj judgement to analysis}
    \item \sout{fig 4: change varapp proj to have x in gamma, not gamma comma x}
    \item \sout{consider matched product, matched arrow to suggest for unknown types}
    \item above: not sure i want matched arrow type in fig 5? feels weirder to suggest an unknown typed var for fn than value...
    \item rankings:
    \item priviledge more specific types
    \item read contextual modal types
    \item \sout{replace constructs with construct-expressions}
    \item AppProj needs a better treatment for selection (should be first non-empty hole)... chain a separate action?
    \item implementation: implement ENTER vs TAB
    \item add keyboard shortcuts for swap etc
    \item proj1 and proj2: make tau in product another underscore
    \item intro rule for type=hole
    \item fig 4 var and approj case: type consistency not premise: put in 
    \item read: polarity: noam zalburger. bob harper blog post
    \item what does it mean to synthesize 'action a': sensibility theorem:
    \item well-typed in synthetic case, checked against tau in analytic case
    \item $\suggest{A}{B}$
    \item $\suggestp{A}{B}$
    \item $\paperclip$
    \item NEW
    \item synthetic  pos: everything
    \item sensibility: all actions result in well-typed states
    \item constructiblity of complete terms: with move to next hole
    \item scorers: symbol + subscript for judgement (num holes judgement)
    
    
\end{itemize}

\newcommand{\singleton}[1]{\{ #1 \}}
\newcommand{\singleaction}[1]{\singleton{\mathtt{#1}}}
\newcommand{\varapparrow}[0]{\rightsquigarrow}
\newcommand{\varappjudge}[4]{#1 \vdash #2 \varapparrow #3 \Leftarrow #4}
\newcommand{\projjudge}[4]{#1 \vdash #2 \twoheadrightarrow #3 \Leftarrow #4}



\newpage



\begin{figure}[t]
    $\arraycolsep=4pt
    \begin{array}{lllllll}
    
    \mathsf{HTyp} & \tau & ::= &
        \tunit ~\vert~
        \tsum{\tau}{\tau} ~\vert~
        \tprod{\tau}{\tau} ~\vert~
        \tarr{\tau}{\tau} ~\vert~
        \tehole\\

    \mathsf{HExp} & \hexp & ::= &
        () ~\vert~
        L~e ~\vert~
        R~e ~\vert~
        ({\hexp},{\hexp}) ~\vert~
        x ~\vert~
        {\hlam{x}{\hexp}} ~\vert~
        {\hexp}(\hexp) ~\vert~
        \hehole ~\vert~
        \hhole{\hexp}
  
    \end{array}$
    \caption{Syntax of H-types and H-expressions. Metavariable $x$ ranges over variables.}
    \label{fig:hexp-syntax}
\end{figure}

\begin{figure}
    \centering
    \fbox{$\suggest
        {\hsyn{\hGamma}{\zexp}{\tau}}
        {\bigalpha}$}~~\text{$\hexp$ synthesizes $\tau$, suggesting actions $\bigalpha$}
    \\
    \fbox{$\suggest
        {\hana{\hGamma}{\zexp}{\tau}}
        {\bigalpha}$}~~\text{$\hexp$ analyzes against $\tau$, suggesting actions $\bigalpha$}  \\
    \caption{Suggestion Judgement Forms}
    \label{fig:suggest_judge}
\end{figure}

\begin{figure}
    \begin{mathpar}
    \centering
    \inferrule[]{
            \suggest
                {\hana{\hGamma}{\zexp}{\tau_1}}
                {\bigalpha}
        }{
            \suggest
                {\hana{\hGamma}{L~\zexp}{\tsum{\tau_1}{\tau_2}}}
                {\bigalpha}
        }
    \\
    \inferrule[]{
            \suggest
                {\hana{\hGamma}{\zexp}{\tau_2}}
                {\bigalpha}
        }{
            \suggest
                {\hana{\hGamma}{R~\zexp}{\tsum{\tau_1}{\tau_2}}}
                {\bigalpha}
        }
    \\
    \inferrule[]{
            \hana{\hGamma}{\hexp_1}{\tau_2} \\
            \suggest
                {\hana{\hGamma}{\zexp_2}{\tau_1}}
                {\bigalpha}
        }{
            \suggest
                {\hana{\hGamma}{(\hexp_1, \zexp_2)}{\tprod{\tau_1}{\tau_2}}}
                {\bigalpha}
        }
    \\
    \inferrule[]{
            \suggest
                {\hana{\hGamma}{\zexp_1}{\tau_1}}
                {\bigalpha}\\
            \hana{\hGamma}{\hexp_2}{\tau_2}
        }{
            \suggest
                {\hana{\hGamma}{(\zexp_1, \hexp_2)}{\tprod{\tau_1}{\tau_2}}}
                {\bigalpha}
        }
    \\
        \inferrule[]{
            \suggest
                {\hsyn{\hGamma}{\zexp_1}{\tau_1}}
                {\bigalpha} \\
            \arrmatch{\tau_1}{\tarr{\tau_2}{\tau}} \\
            \hana{\hGamma}{\hexp_2}{\tau_2}
        }{
            \suggest
                {\hana{\hGamma}{\dap{\zexp_1}{\hexp_2}}{\tau}}
                {\bigalpha}
        }
    \\
    \inferrule[]{
            \hsyn{\hGamma}{\hexp_1}{\tau_1}
            \\
            \arrmatch{\tau_1}{\tarr{\tau_2}{\tau}} \\
            \suggest
                {\hana{\hGamma}{\zexp_2}{\tau_2}}
                {\bigalpha}
        }{
            \suggest
                {\hana{\hGamma}{\dap{\hexp_1}{\zexp_2}}{\tau}}
                {\bigalpha}
        }
    \\
        \inferrule[]{
            \arrmatch{\tau}{\tarr{\tau_1}{\tau_2}} \\
            \suggest
                {\hana{\hGamma, x: \tau_1}{\zexp}{\tau_2}}
                {\bigalpha}
        }{
            \suggest
                {\hana{\hGamma}{\hlam{x}{\zexp}}{\tau}}
                {\bigalpha}
        }
    \\
    \inferrule[DoesThisWork]{
            \suggest
                {\hana{\hGamma}{\zexp}{\tau}}
                {\bigalpha}
        }{
            \suggest
                {\hana{\hGamma}{\hhole{\zexp}}{\tau}}
                {\bigalpha}
        }
    \\
    \end{mathpar}
    \caption{Analytic Suggestion Zipper Cases}
    \label{fig:suggests_zipper}
\end{figure}

\begin{figure}
    \begin{mathpar}
        \inferrule[Suggest Expr Syn]{
            \suggest
                {\hana{\hGamma}{\zexp}{\tehole{}}}
                {\bigalpha_{}}
        }{
            \suggest
                {\hsyn{\hGamma}{\zexp}{\_}}
                {\bigalpha_{}}
        }
    \end{mathpar}
    \caption{Synthetic Case}
\end{figure}

\begin{figure}
    \begin{mathpar}
        \inferrule[Suggest Hole Analytic]{
            \suggestStar{\mathsf{Intros}(\tau)}{\bigalpha_{intros}} \\
            \suggestStar{\mathsf{Elims}(\Gamma, \tau)}{\bigalpha_{elims}}
        }{
            \suggest
                {\hana{\hGamma}{\zwsel{\hehole{}}}{\tau}}
                {\bigalpha_{intros} \cup \bigalpha_{elims}}
        }
        \\
        \inferrule[Suggest Expr Analytic]{
            \suggestStar{\mathsf{Wraps}(\hexp, \tau)}{\bigalpha_{wraps}} \\
            \suggestStar{\mathsf{Replaces}(\Gamma, \tau)}{\bigalpha_{replaces}}
        }{
            \suggest
                {\hana{\hGamma}{\zwsel{\hexp}}{\tau}}
                {\bigalpha_{wraps} \cup \bigalpha_{replaces}}
        }
        \\
        \inferrule[Replacement]{
            \suggest
                {\hana{\hGamma}{\zwsel{\hehole{}}}{\tau}}
                {\bigalpha}
        }
        {
            \suggestStar
                {\mathsf{Replaces}(\Gamma, \tau)}
                {\{ \mathtt{del} \;;\; \alpha  \;|\; \alpha \in \bigalpha\}}
        }
        \\
        \inferrule[Wrapping (simple)]{
            \hsyn{\hGamma}{\hexp}{\tau_e} \\
            \tconsistent{\tau_e}{\tau'}
        }
        {
            \suggestStar
                {\mathsf{Wraps}(\hexp, \tau)}
                {\{ \construct{\dap{f}{\zwsel{\hexp}}} \;|\; f : \tarr{\tau'}{\tau} \in \Gamma\}}
        }        
    \end{mathpar}
    \caption{Analytic base cases}
    \label{fig:suggests}
\end{figure}

\begin{figure}
    \begin{mathpar}
    
        \inferrule[IntrosTriv]
            { }
            {\suggestStar
                {\mathsf{Intros}(\tunit)}
                {\singleaction{\construct{\zwsel{()}}}}}

        \inferrule[IntrosProd]
            { }
            {\suggestStar
                {\mathsf{Intros}(\tprod{\tau_1}{\tau_2})}
                {\singleaction{\construct{\hpair{\zwsel{\hehole{}}}{\hehole{}}}}}}
        
        \inferrule[IntrosArrow]
            { }
            {\suggestStar
                {\mathsf{Intros}(\tarr{\tau_1}{\tau_2})}
                {\singleaction{\construct{\hlam{x}{\zwsel{\hehole{}}}}}}}

        \inferrule[IntrosSum]
            { }
            {\suggestStar
                {\mathsf{Intros}(\tsum{\tau_1}{\tau_2})}
                {\{{\construct{\hinL{\zwsel{\hehole{}}}}},
                 {\construct{\hinR{\zwsel{\hehole{}}}}}} \}}

        \inferrule[IntrosHole]
            {
            \suggestStar{\mathsf{Intros}(1)}{\bigalpha_{1}} \\
            \suggestStar{\mathsf{Intros}(\tprod{\tehole}{\tehole})}{\bigalpha_{\tprod{}{}}} \\
            \suggestStar{\mathsf{Intros}(\tsum{\tehole}{\tehole})}{\bigalpha_{\tsum{}{}}} \\
             \suggestStar{\mathsf{Intros}(\tarr{\tehole}{\tehole})}{\bigalpha_{\tarr{}{}}} \\
            }
            {\suggestStar
                {\mathsf{Intros}(\tehole{})}
                {\bigalpha_{1} \cup {\bigalpha_{\tprod{}{}} \cup \bigalpha_{\tsum{}{}} \cup \bigalpha_{\tarr{}{}}}}}

    \end{mathpar}
    \caption{Introduction suggestions}
    \label{fig:suggest_intros}
\end{figure}

\begin{figure}
    \begin{mathpar}

        \inferrule[Suggest Elims]{
            \suggestStar{\mathsf{ElimCase}}{\bigalpha_{case}} \\
            \suggestStar{\mathsf{Var}(\Gamma, \tau)}{\bigalpha_{var}} \\
            \suggestStar{\mathsf{AppProj}(\Gamma, \tau)}{\bigalpha_{approj}} \\
        }{
         \suggestStar
            {\mathsf{Elims}(\Gamma, \tau)}
            {\bigalpha_{case} \cup \bigalpha_{var} \cup \bigalpha_{approj}}
        }

        \inferrule[ElimCase]
            { }
            {\suggestStar
                {\mathsf{ElimCase}}
                {\singleaction{\construct{\hcase{\zwsel{\hehole{}}}{x}{\hehole{}}{y}{\hehole{}}}}}}

        \inferrule[Var]
            {\tconsistent{\tau}{\tau'}}
            {\suggestStar
                {\mathsf{Var}(\Gamma, \tau)}
                {\{\mathtt{\construct{\zwsel{x}}} \;|\; x : \tau' \in \Gamma\}}}

        \inferrule[AppProj]
            {\tconsistent{\tau}{\tau'}}
            {\suggestStar
                {\mathsf{AppProj}(\Gamma, \tau)}
                {\{\mathtt{\construct{\zwsel{e}}}
                 \;|\;
                 x : \tau' \in \Gamma \; \wedge \; \varappjudge{\Gamma}{x}{e}{\tau}\}}}

    \end{mathpar}
    \caption{Elimination suggestions}
    \label{fig:suggest_elims}
\end{figure}

\begin{figure}
    \judgbox
        {\varappjudge{\Gamma}{\hexp}{\hexp'}{\tau}}
        { \\ $\hexp$, applied to 0 or more holes, \\ and projected 0 or more times, \\
         yields an expr analyzing to $\tau$}
    \begin{mathpar}
        \inferrule[AppProjBase]
            {\hana{\Gamma}{\hexp}{\tau}}
            {\varappjudge{\Gamma}{e}{e}{\tau}}

            % output type is tau'' != hole
            %

        \inferrule[App]
            {
                \hsyn{\Gamma}{\hexp}{\tau'} \\
                \arrmatch{\tau'}{\tarr{\_}{\_}} \\
                \varappjudge{\Gamma}{\dap{\hexp}{\hehole{}}}{\hexp'}{\tau}
            }
            {\varappjudge{\Gamma}{\hexp}{\hexp'}{\tau}}

        \inferrule[Proj1]
                {
                    \hsyn{\Gamma}{\hexp}{\tau'} \\
                    \prodmatch{\tau'}{\tprod{\tau}{\_}} \\
                    \varappjudge{\Gamma}{\pi_1 \hexp}{\hexp'}{\tau}
                }
                {\varappjudge{\Gamma}{e}{e'}{\tau}}
        
        \inferrule[Proj2]
                {
                    \hsyn{\Gamma}{\hexp}{\tau'} \\
                    \prodmatch{\tau'}{\tprod{\_}{\tau}} \\
                    \varappjudge{\Gamma}{\pi_2 \hexp}{\hexp'}{\tau}
                }
                {\varappjudge{\Gamma}{e}{e'}{\tau}}   

    \end{mathpar}
    \caption{Supporting elimination judgments}

    \label{fig:support_elims}
    
\end{figure}

\begin{figure}
    \begin{mathpar}
    \centering
    
        \inferrule[Errors Triv]{ }
        { \errorCount{()}{0} }

        \inferrule[Errors Var]{ }
        { \errorCount{x}{0} }

        \inferrule[Errors EmptyHole]{ }
        { \errorCount{\hehole{}}{0} }

        \inferrule[Errors NonEmptyHole]
        { \errorCount{\hexp}{n} }
        { \errorCount{\hhole{\hexp}{}}{n+1} }

        \inferrule[Errors Lambda]
        { \errorCount{\hexp}{n} }
        { \errorCount{\hlam{x}{\hexp}}{n+1} }

        \inferrule[Errors Pair]{
           \errorCount{\hexp_1}{n_1} \\
           \errorCount{\hexp_2}{n_2} \\
           n_1 + n_2 = n
        }{ \errorCount{(\hexp_1,\hexp_2)}{n} }
        
        \inferrule[Errors Ap]{
           \errorCount{\hexp_1}{n_1} \\
           \errorCount{\hexp_2}{n_2} \\
           n_1 + n_2 = n
        }{ \errorCount{\dap{\hexp_1}{\hexp_2}}{n} }
    \end{mathpar}
    \caption{Count hole rules}
\end{figure}

\begin{figure}
    \begin{itemize}
        \item T3 (Suggestion sensibility theorem):\\
        For all $\Gamma, \zexp, \tau, a \in \bigalpha$
        where $\suggest
        {\hana{\hGamma}{\zexp}{\tau}}
        {\bigalpha}$ \\
        there exists $\zexp', \tau'$ \\
        such that $\numErrors{\removeSel{\hexp}} \leq \numErrors{\removeSel{\hexp'}}$
        and $\performAna{\hGamma}{\zexp}{\tau}{\alpha}{\zexp'}$ \\
        \\
        \item T0 (Suggestion generalizes typing Ana):\\
        For all $\Gamma, \zexp, \tau, \bigalpha$ \\
        where $\suggest
            {\hana{\hGamma}{\zexp}{\tau}}
            {\bigalpha}$ \\
        we have $\hana{\hGamma}{\removeSel{\zexp}}{\tau}$\\
        \\
        \item T1 (Existence and uniqueness of suggestions Ana):\\
        For all $\Gamma, \zexp, \tau$
        such that $\hana{\hGamma}{\removeSel{\zexp}}{\tau}$, \\
        there exists a unique $\bigalpha$ such that 
        $\suggest
            {\hana{\hGamma}{\zexp}{\tau}}
            {\bigalpha}$\\
        \\
        \item T2 (lemma for T1):\\
        For all $\tau$ there exists a unique $\bigalpha$ such that \\
        $\suggestStar {\mathsf{Intros}(\tau)} {\bigalpha}$\\
        \\
    \end{itemize}
    \caption{Theorems & Lemmas}
\end{figure}