Stefan pushed to branch report/hmdup at Stefan / Typer

Commits: 93e6993d by Stefan Monnier at 2020-09-26T20:41:16-04:00 Add an example

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -68,10 +68,13 @@ \DeclareUnicodeCharacter{2080}{\ensuremath{_0}} \DeclareUnicodeCharacter{2081}{\ensuremath{_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{_2}} +\DeclareUnicodeCharacter{2113}{\ensuremath{\ell}} \DeclareUnicodeCharacter{21D2}{\ensuremath{\Rightarrow}} \DeclareUnicodeCharacter{21DB}{\ensuremath{\Rrightarrow}} \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} \DeclareUnicodeCharacter{2203}{\ensuremath{\exists}} +\DeclareUnicodeCharacter{2237}{:\ensuremath{!}:} +\DeclareUnicodeCharacter{2254}{:\ensuremath{!}=} \DeclareUnicodeCharacter{2261}{\ensuremath{\equiv}} \DeclareUnicodeCharacter{2980}{\ensuremath{|||}} \DeclareUnicodeCharacter{1D4B0}{\ensuremath{\mathcal{U}}} @@ -295,8 +298,8 @@ any program that can be typed by HM-inference should be accepted by our system without any need for type annotations either; (2) to preserve the let-polymorphism and automatic specialization of HM-inference; (3) to be simple and adaptable to most features of modern typed lambda calculi. -While the first two goals reduce the need for type annotations, -minimizing the amount of type annotations was secondary to the design. +%% While the first two goals reduce the need for type annotations, +%% minimizing the amount of type annotations was secondary to the design..

@@ -314,7 +317,8 @@ minimizing the amount of type annotations was secondary to the design. \newcommand \Meta [1] {#1} \newcommand \DArw [3] {\forall #1 : #2 . #3} \newcommand \Let [3] {\kw{let}~#1=#2~\kw{in}~#3} -\newcommand \MDArw [2] {\forall \overrightarrow{#1} . #2} +\newcommand \CDArw [2] {\forall {#1} . #2} +\newcommand \MDArw [2] {\CDArw{\overrightarrow{#1}}{#2}} \newcommand \HasType [2] {#1 : #2}

\newcommand \Jcheck [3][\Gamma] {#1 \vdash #2 \Leftarrow #3} @@ -388,7 +392,7 @@ the fact that our types are not stratified into monomorphic types and type schemes. The use of explicit metavariables is not very important here, but it will play a bigger role once we adapt our system to more powerful type systems. Similarly, the lack of stratification does not make -a significant difference at this stage: the algorithm will still only infer +a significant difference at this stage: the algorithm will still infer only those types which can be represented in the traditional stratified system, but our later systems do not make use of such a stratification. @@ -456,7 +460,7 @@ $u_2$ was instantiated to. %% \label{fig:bidi-check} %% \end{figure}

-Figure~\cite{fig:bidi-check} shows the traditional bidirectional rules to +Figure~\ref{fig:bidi-check} shows the traditional bidirectional rules to type check the $\lambda$-calculus.

\begin{figure} @@ -508,7 +512,7 @@ type check the $\lambda$-calculus. \label{fig:bidi-infer} \end{figure}

-Figure~\cite{fig:bidi-infer} shows how we can generalize them to the case +Figure~\ref{fig:bidi-infer} shows how we can generalize them to the case where we do type inference. The last rule is the one that lets us infer the type of a $\Lam{x}{e}$. It also makes the rules non-syntax directed, so it should only be used when $e$ is a ``checking expression'', in our case @@ -679,7 +683,7 @@ While we do not intend to require as few annotations as systems like existing type information to try and reduce the amount of annotations needed. To this end, we need to pay attention to the places where redundant type information can be better used. In the original Hindley-Milner -algorithm, we can see that the only place where we might ``burn off'' excess +algorithm, we can see that the main place where we might ``burn off'' excess information is in the \textsc{HM-App} rule, where the type $\tau_1$ of the argument might be inferred both from $e_2$ and from $e_1$.

@@ -700,6 +704,16 @@ which we can just \emph{check} the type of $e_2$ against $\tau_1$. This is because in the vast majority of cases we already know the type of the function we're calling.

+In HM, $\forall$-quantification can only appear in the context: it is introduced +when adding a variable to the context via \textsc{HM-Let} and it is then +systematically eliminated when referring to those variables via +\textsc{HM-Var}. + +To cover System-F, these constraints need to be relaxed such that +$\forall$-quantification can be introduced and eliminated virtually anywhere, +which intuitively explains why the problem is undecidable unless we require +the addition of explicit annotations. + The only change to the syntax of the language is the addition of the form $\HasType{e}{\tau}$. While the specific form of the type annotations is not a primary concern for us, we did want to avoid ``non-standard'' annotations @@ -827,6 +841,91 @@ incompatible with things like value polymorphism.

\FIXME{Change the rules to avoid those extra eta-redexes}

+\section{Examples} + +Fully annotated example: +%% type NList (ℓ ∷ Level) (t : Type ℓ) (n : Nat) +%% | nnil (n ≡ zero) +%% | ncons (n' ∷ Nat) (n = succ n') t (NList (ℓ ≔ ℓ) t n'); +\begin{verbatim} + type NList [ℓ : Level] (t : Type ℓ) (n : Nat) + | nnil : NList [ℓ] t zero + | ncons [n' : Nat] t (NList [ℓ] t n') + : NList [ℓ] t (succ n'); + + empty : [ℓ : Level] → [t : Type ℓ] → [n : Nat] + → NList [ℓ] t n → Bool; + empty = λ [ℓ : Level] [t : Type ℓ] [n : Nat] + (xs : NList [ℓ] t n) + → case xs + | nnil ⇒ true + | ncons [_] _ _ ⇒ false; + + append : [ℓ : Level] → [t : Type ℓ] → [n₁ : Nat] → [n₂ : Nat] + → NList [ℓ] t n₁ → NList [ℓ] t n₂ + → NList [ℓ] t (n₁ + n₂); + append = λ [ℓ : Level] [t : Type ℓ] [n₁ : Nat] [n₂ : Nat] + (xs₁ : NList [ℓ] t n₁) + (xs₂ : NList [ℓ] t n₂) + → case xs₁ + | nnil ⇒ xs₂ + | ncons [n'] x xs + ⇒ ncons [ℓ] [t] [n'] + x (append [ℓ] [t] [n'] [n₂] + xs xs₂); +\end{verbatim} + +Annotations where inference tries to fill implicit actual arguments, +type annotations, and use bidirectional type checking to infer implicit +formals: +\begin{verbatim} + type NList [ℓ] (t : Type ℓ) n + | nnil : NList t zero + | ncons [n'] t (NList t n') : NList t (succ n'); + + empty = λ [ℓ] [t : Type ℓ] [n] + (xs : NList t n) + → case xs + | nnil ⇒ true + | ncons _ _ ⇒ false; + + append : [ℓ] → [t : Type ℓ] → [n₁] → [n₂] + → NList t n₁ → NList t n₂ → NList t (n₁ + n₂); + append = λ xs₁ xs₂ + → case xs₁ + | nnil ⇒ xs₂ + | ncons x xs ⇒ ncons x (append xs xs₂); +\end{verbatim} +Notice how we still need the annotation ``\texttt{:~Type~ℓ}'' on the +\texttt{t} argument, even though the uses of \texttt{t} make it clear it +should be a type. Similarly, we still need the annotation +``\texttt{:~NList~t~n}'' on the \texttt{xs} argument of \texttt{empty} +because inference will clearly figure out that it should have the form +``\texttt{NList~?~?}'' but will not know to use the \texttt{t} and +\texttt{n} arguments that the programmer added specifically for +that purpose. + +Further reduction based on HM-style automatic generalisation: +\newpage +\begin{verbatim} + type NList t n + | nnil : NList t zero + | ncons t (NList t ?n') : NList t (succ ?n'); + + empty = λ xs → case xs + | nnil ⇒ true + | ncons _ _ ⇒ false; + + append : NList ?t ?n₁ → NList ?t ?n₂ → NList ?t (?n₁ + ?n₂); + append = λ xs₁ xs₂ → case xs₁ + | nnil ⇒ xs₂ + | ncons x xs ⇒ ncons x (append xs xs₂); +\end{verbatim} +Notice how the generalization not only allows the programmer to omit +writing the implicit formal arguments but it also allows the removal of the +type annotations ``\texttt{:~Type~ℓ}'' and ``\texttt{:~NList~t~n}''. + + \section{Elaboration}

\FIXME{We should probably directly present the elaborating version of the @@ -1080,6 +1179,18 @@ our language is extended as follows:

\cite{Mycroft84,Henglein93}

+%% Crap! That's what this article was trying to do! +%% Differences I can see so far: +%% - Doesn't do HM-style let-generalization +%% - Focuses on automatic insertion of implicit +%% lambdas rather than implicit applications +%% - We want to deal with universe levels +\cite{Kovacs20} + +\cite{Laufer92} %Twelf-style elision of existential quantification in datatypes + +\cite{Odersky96} %System-F inference via type annotations + \section{Conclusion}

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93e6993d295382988becca604d0f22b90e...