


@ 205,8 +205,8 @@ There are two difficulties with the code we had to write:





values are \emph{named} far from where they are \emph{expressed} in





the program; notice for example how \lstinline{u'} binds the witness





of \lstinline{hastype u v}, but is placed farther away in the





program. This problem gets worse when inferring the types of more





complex constructs.





program. This problem gets worse when writing inference code for





more complex constructs.










When we explain this code, we say that the \lstinline{Infer.ty}





result of \lstinline{exist} or the \lstinline{(F.term * F.ty) list}




@ 297,20 +297,20 @@ any functor \lstinline{'a t}, the type\\ %





\lstinline{type 'a m = 'r. ('a > 'r t) > 'r t} has a monadic





structure. This lets us write \lstinline{exist} and our





\lstinline{traverse} above in monadic style, and then rely on our





usual monadic programming hbits. Unfortunately, we found this too hard





usual monadic programming habits. Unfortunately, we found this too hard





to use in practice for the following reasons:





\begin{itemize}










\item \lstinline{exist} is a naturally \emph{scoped} construction:





besides generating a free variables, it builds a raw constraint term





of the form \lstinline{CExist(x,rc)}, where the inference variable





is only bound in the constraint subterm \lstinline{rc}.





scopes over the constraint subterm \lstinline{rc}.










A \lstinline{co_cps} computation builds a single evergrowing scope





(by composing continuations in scope of all quantifiers effect





performed so var). The scope is only ``closed'' when the computation





is ``run'' by invoking it with the identity continuation  we can





define a closing combinator to encapsulate this transformation.





define a \lstinline{close} combinator doing this.










Note that lifting all existential constraints to a toplevel, global





scope would be incorrect, due to the interplay with polymorphism /




@ 388,7 +388,10 @@ which introduce arguments of type \lstinline{'a} to build a constraint





in a delimited scope returning a \lstinline{'r co}. Only terms of this





type are written in continuationpassing style. They are used through





\lstinline{let@}, that opens a quantifier which naturally scopes until





the end of the lexical block.





the end of the lexical block. The binder syntax is a reference to





OCaml's infix application operator \lstinline{(@@)}: %





\lstinline{(let@ p = a in b)} is equivalent to %





\lstinline{(b @@ fun p > a)}.










Our ``tuple'' case becomes as follows:





\begin{lstlisting}




@ 417,15 +420,15 @@ expression at the logical place in the code (\lstinline{ty} and





\lstinline{us'} for example). Being in the applicative, a modal input





variable \lstinline{x} cannot be used asis to build the witness, it





has to be ``unpacked'' in the final%





\lstinline{let+ .. and+ .. in <witness>} block by the construction





(at first surprising) \lstinline{and+ x = x}.










Unpacking is slightly surprising, and the redudancy is frustrating





(one could think of a proper modaltyping rule in the compiler that





would implicitly unpack modal inputs); but note that the unpacking place





corresponds to the place, in the previous style, where the variable





would have been first named. Unpacking is a fair price to pay to





recover readable code.





\lstinline{let+ .. and+ .. in <witness>} block by the odd construction





\lstinline{and+ x = x}.





%





This unpacking construction is surprising, and the redudancy is





frustrating (one could think of a proper modaltyping rule in the





compiler that would implicitly unpack modal inputs); but note that the





unpacking place corresponds to the place, in the previous style, where





the variable would have been first named. Unpacking is a fair price to





pay to recover readable code.










\bibliography{biblio}





\end{document}




