@@ -6,6 +6,7 @@
66\usepackage{microtype}
77\usepackage{trfrac}
88\usepackage{multirow}
9+\usepackage{textcomp}
910% \usepackage{caption}
1011% \usepackage[main=english,russian]{babel}
1112
@@ -16,6 +17,26 @@
1617
1718%include polycode.fmt
1819
20+%format forall = "\forall"
21+%format a = "\alpha"
22+%format a'
23+%format b = "\beta"
24+%format b'
25+%format c = "\gamma"
26+%format c'
27+%format d = "\delta"
28+%format d'
29+%format s = "\sigma"
30+%format m = "\mu"
31+%format r = "\psi"
32+%format x = "\eta"
33+%format x'
34+%format y = "\zeta"
35+%format y'
36+%format ^ = " "
37+%format ^^ = "\;"
38+%format !! = "{\;}''\!\!"
39+%format <> = "\diamond"
1940
2041% \floatstyle{boxed}
2142% \newfloat{figure}{hbp}{lst}
@@ -58,7 +79,7 @@
5879
5980% \end{otherlanguage}
6081
61−\parr{Source code} \url{https://github.com/ilyakooo0/tix}
82+% \parr{Source code} \url{https://github.com/ilyakooo0/tix}
6283
6384% \newpage
6485
@@ -689,7 +710,7 @@ Just like in many functional type systems, our type system will support let-gene
689710
690711A simple version of rule is as follows:
691712
692−\begin{equation}
713+\begin{equation} \label{eq:letGeneralization}
693714 \trfrac
694715 {\Gamma \vdash e_1 : \tau_1 \qquad \Gamma, (\text{x}: \forall \{\text{ftv}(\tau_1) - \text{ftv}(\Gamma)\}. \; \tau_1) \vdash e_2 : \tau_2}
695716 {\Gamma \vdash (\text{let} \; \text{x = } e_1; \; \text{in} \; e_2) : \tau_2}
@@ -777,7 +798,7 @@ The definition of the ``update'' predicate uses standard set comprehension notat
777798 {\Pi \xi_1 \update \Pi \xi_2 \sim \Pi (\xi_2 \cup \{a = \tau || (a = \tau) \leftarrow \xi_1, a \notin \xi_2\})}
778799\end{equation}
779800
780−\subsubsection{with expressions}
801+\subsubsection{with expressions} \label{sec:withExprType}
781802
782803\emph{with expressions} discussed in section~\ref{sec:withExp} are not difficult to define a typing rule for:
783804
@@ -800,7 +821,190 @@ Instead, we opted to define a heuristic which in our testing was proven to cover
800821
801822\section{Implementation} \label{sec:implementation}
802823
803−\cite{github-source}
824+In this section we will explore the techniques employed in our implementation~\cite{github-source} of our type system. It is implemented in the \emph{Haskell}\footnote{\url{https://www.haskell.org}} programming language.
825+
826+% \subsubsection{Effects}
827+
828+% Our implementation uses the \emph{freer-simple}\footnote{\url{https://github.com/lexi-lambda/freer-simple}} library as the effects system.
829+
830+% The
831+
832+% \begin{code}
833+% type InferEffs =
834+% !! [ Fresh,
835+% Reader SrcSpan,
836+% Writer (SrcSpan, Errors),
837+% Writer PredicateError,
838+% Writer Pred,
839+% State (MKM.Map Pred),
840+% VariableMapEff,
841+% Writer UnifyingError,
842+% Writer InferError,
843+% State Substitution,
844+% TreeTracer
845+% ]
846+% \end{code}
847+
848+\subsection{Substitutions}
849+
850+\subsubsection{Substitutions in other implementations}
851+
852+In most typechecker implementations a substitution is a mapping from \emph{type variables} to \emph{types}. These substitutions are usually generated during the unification of type constraints and are, in general, applied to types as soon as they are available.
853+
854+The notion of substitution composition is usually taken to mean a binary operation which produces a new substitution that when applied (|sub|) to a type would produce the same result as sequentially applying the two source substitutions:
855+
856+\begin{code}
857+sub (s1 . s2) = sub s1 . sub s2
858+\end{code}
859+
860+\subsubsection{Substitutions in our implementation}
861+
862+In our implementation the application of substitutions is delayed as much as possible. They are applied in exactly two cases:
863+
864+\begin{enumerate}
865+ \item Right before unifying a constraint
866+ \item Right before closing over a type
867+\end{enumerate}
868+
869+This choice has several implications. Firstly, we can never have conflicting ``keys'' in substitutions (which is not the case in other implementations). Using this information we can define stronger substitution composition:
870+
871+\begin{code}
872+newtype Substitution =
873+ Substitution {unSubstitution :: Map TypeVariable NType}
874+
875+instance Semigroup Substitution where
876+ a'@(Substitution a) <> b'@(Substitution b) =
877+ Substitution $ M.unionWith undefined
878+ (fmap (sub b') a)
879+ (fmap (sub a') b)
880+\end{code}
881+
882+
883+This means that the order of composition does no longer matter, and applying the composition of substitutions yields more information than applying them sequentially.
884+
885+Another consequence of the decision to delay substitutions is that now the role of the |infer| step of typechecking only does the following tree things:
886+
887+\begin{enumerate}
888+ \item returns a type variable that represents the type of the expression being inferred
889+ \item emits constraints generated during inferring
890+ \item emits predicates generated during inferring
891+\end{enumerate}
892+
893+\subsection{Typing context}
894+
895+The typing context in our implementation in essence consists of two distinct data structures:
896+
897+\begin{enumerate}
898+ \item the types of variables currently in scope
899+ \item the predicates which are applicable to those types
900+\end{enumerate}
901+
902+\subsubsection{Variables in scope}
903+
904+Note that in practice it only needs to contain type variables since we apply substitutions as late as possible.
905+
906+In actual fact, due to the heuristics described in section~\ref{sec:withExprType} the types of variables in scope can not be represented as static data structure, but rather is implemented as a scoped effect\footnote{Effects in our case are implemented using the \emph{freer-simple} library: \url{https://github.com/lexi-lambda/freer-simple}}:
907+
908+\begin{code}
909+data VariableMapEff x where
910+ LookupVariable
911+ :: VarName -> VariableMapEff (Maybe Scheme)
912+
913+lookupVar
914+ :: Member VariableMapEff eff
915+ => VarName -> Eff eff (Maybe Scheme)
916+lookupVar = send . LookupVariable
917+\end{code}
918+
919+This allows us to dynamically redefine what it means to lookup a variable in terms of its implementation in the outer context.
920+
921+\subsubsection{Predicates}
922+
923+Predicates can, on the other hand, be stored as a static data structure. The only non-standard behavior is that the set of predicates needs to be queried and manipulated based on the types that they contain, rather than on the predicates themselves.
924+
925+For this reason we have developed a data structure we call ``multi-keyed map''.
926+
927+\begin{code}
928+class (Ord (Key t), Ord t) => Keyable t where
929+ type Key t :: Type
930+ getKeys :: t -> [Key t]
931+
932+data MultiKeyedMap t = MultiKeyedMap
933+ (M.Map (Key t) (S.Set t)) (S.Set t)
934+\end{code}
935+
936+The data structure contains is the product of two other data structures:
937+
938+\begin{enumerate}
939+ \item A map, mapping possible keys of the stored |t| to a set of values the contains the given key
940+ \item A set which contains the values that don't contain any keys
941+\end{enumerate}
942+
943+The |Keyable| typeclass is used to extract the keys from the values that need to be stored.
944+
945+The union of two maps is defined trivially -- by taking the union of the inner structures:
946+
947+\begin{code}
948+instance (Ord (Key t), Ord t)
949+ => Semigroup (MultiKeyedMap t) where
950+ (MultiKeyedMap x x') <> (MultiKeyedMap y y') =
951+ MultiKeyedMap
952+ (M.unionWith S.union x y) (x' <> y')
953+\end{code}
954+
955+Creating a singleton map from a single values is defined like this:
956+
957+\begin{code}
958+singleton :: Keyable t => t -> MultiKeyedMap t
959+singleton t = case getKeys t of
960+ [] -> MultiKeyedMap M.empty (S.singleton t)
961+ ks@(_ : _) -> MultiKeyedMap
962+ (M.fromList $ fmap (,s) ks) S.empty
963+ where
964+ s = S.singleton t
965+\end{code}
966+
967+With these operations defining the |insert| operation becomes trivial:
968+
969+\begin{code}
970+insert
971+ :: Keyable t
972+ => t -> MultiKeyedMap t -> MultiKeyedMap t
973+insert t m = m <> singleton t
974+\end{code}
975+
976+Now we come to the lookup operation. Not that the algorithmic complexity of querying the predicates by a type they contain is now the cost of an ordinary map lookup -- $O(log(n))$ where $n$ is the number of values contained in the map (in our case thw number of all types referenced from within the predicates):
977+
978+\begin{code}
979+lookup
980+ :: Keyable t
981+ => Key t -> MultiKeyedMap t -> S.Set t
982+lookup k (MultiKeyedMap m _) =
983+ fromMaybe S.empty $ M.lookup k m
984+\end{code}
985+
986+\subsection{Closing over type variables}
987+
988+An observation we can make is the following: it only makes sense to close over the type variables that were generated during the inference of the type we are closing over. Any other type variables either:
989+
990+\begin{enumerate}
991+ \item are not present in the type
992+ \item are used in an outer lexical scope (environment)
993+\end{enumerate}
994+
995+This greatly simplifies implementing the typing rule~\ref{eq:letGeneralization} since instead of having to calculate a set of free type variables of the whole context, we only need to obtain a predicate which identifies if a type variable was introduced during the inference of an expression. This is made even easier if type variables are internally represented as integers, as they often are.
996+
997+In our case this is complicated by the fact that we need to introduce type variables which are fields of an \emph{attribute set} from an outer lexical scope. This is problematic because while the type variable is can be defined during inference, it is actually logically defined at the same position as the initial \emph{attribute set} it has the same lexical scope as the \emph{attribute set}. So the lexical scope of a type variable can not be derived from the inference context of an expression.
998+
999+A solution we came up with is two have two ways a type variable can be constructed -- as an ordinary type variable backed by a single integer, or as a sub-type variable which has the same lexical scope as another type variable:
1000+
1001+\begin{code}
1002+data TypeVariable
1003+ = TypeVariable Int
1004+ | SubTypeVariable Int Int
1005+\end{code}
1006+
1007+This way, when applying a predicate to check the lexical scope of a type variable we can always restrict ourselves to the first integer.
8041008
8051009\section{Possible improvements}
8061010