@@ -6,6 +6,7 @@
6\usepackage{microtype}
6\usepackage{microtype}
7\usepackage{trfrac}
7\usepackage{trfrac}
8\usepackage{multirow}
8\usepackage{multirow}
9% \usepackage{caption}
10% \usepackage{caption}
10% \usepackage[main=english,russian]{babel}
11% \usepackage[main=english,russian]{babel}
@@ -16,6 +17,26 @@
17%include polycode.fmt
18%include polycode.fmt
20+%format forall = "\forall"
38+%format !! = "{\;}''\!\!"
39+%format <> = "\diamond"
20% \floatstyle{boxed}
41% \floatstyle{boxed}
21% \newfloat{figure}{hbp}{lst}
42% \newfloat{figure}{hbp}{lst}
@@ -58,7 +79,7 @@
59% \end{otherlanguage}
80% \end{otherlanguage}
61−\parr{Source code} \url{https://github.com/ilyakooo0/tix}
82+% \parr{Source code} \url{https://github.com/ilyakooo0/tix}
@@ -689,7 +710,7 @@ Just like in many functional type systems, our type system will support let-gene
690A simple version of rule is as follows:
711A simple version of rule is as follows:
692−\begin{equation}
713+\begin{equation} \label{eq:letGeneralization}
694 {\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}
715 {\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}
695 {\Gamma \vdash (\text{let} \; \text{x = } e_1; \; \text{in} \; e_2) : \tau_2}
716 {\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
777 {\Pi \xi_1 \update \Pi \xi_2 \sim \Pi (\xi_2 \cup \{a = \tau || (a = \tau) \leftarrow \xi_1, a \notin \xi_2\})}
798 {\Pi \xi_1 \update \Pi \xi_2 \sim \Pi (\xi_2 \cup \{a = \tau || (a = \tau) \leftarrow \xi_1, a \notin \xi_2\})}
778\end{equation}
799\end{equation}
780−\subsubsection{with expressions}
801+\subsubsection{with expressions} \label{sec:withExprType}
782\emph{with expressions} discussed in section~\ref{sec:withExp} are not difficult to define a typing rule for:
803\emph{with expressions} discussed in section~\ref{sec:withExp} are not difficult to define a typing rule for:
@@ -800,7 +821,190 @@ Instead, we opted to define a heuristic which in our testing was proven to cover
801\section{Implementation} \label{sec:implementation}
822\section{Implementation} \label{sec:implementation}
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.
826+% \subsubsection{Effects}
828+% Our implementation uses the \emph{freer-simple}\footnote{\url{https://github.com/lexi-lambda/freer-simple}} library as the effects system.
836+% Writer (SrcSpan, Errors),
837+% Writer PredicateError,
839+% State (MKM.Map Pred),
841+% Writer UnifyingError,
843+% State Substitution,
848+\subsection{Substitutions}
850+\subsubsection{Substitutions in other implementations}
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.
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:
857+sub (s1 . s2) = sub s1 . sub s2
860+\subsubsection{Substitutions in our implementation}
862+In our implementation the application of substitutions is delayed as much as possible. They are applied in exactly two cases:
865+ \item Right before unifying a constraint
866+ \item Right before closing over a type
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:
872+newtype Substitution =
873+ Substitution {unSubstitution :: Map TypeVariable NType}
875+instance Semigroup Substitution where
876+ a'@(Substitution a) <> b'@(Substitution b) =
877+ Substitution $ M.unionWith undefined
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.
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:
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
893+\subsection{Typing context}
895+The typing context in our implementation in essence consists of two distinct data structures:
898+ \item the types of variables currently in scope
899+ \item the predicates which are applicable to those types
902+\subsubsection{Variables in scope}
904+Note that in practice it only needs to contain type variables since we apply substitutions as late as possible.
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}}:
909+data VariableMapEff x where
911+ :: VarName -> VariableMapEff (Maybe Scheme)
914+ :: Member VariableMapEff eff
915+ => VarName -> Eff eff (Maybe Scheme)
916+lookupVar = send . LookupVariable
919+This allows us to dynamically redefine what it means to lookup a variable in terms of its implementation in the outer context.
921+\subsubsection{Predicates}
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.
925+For this reason we have developed a data structure we call ``multi-keyed map''.
928+class (Ord (Key t), Ord t) => Keyable t where
930+ getKeys :: t -> [Key t]
932+data MultiKeyedMap t = MultiKeyedMap
933+ (M.Map (Key t) (S.Set t)) (S.Set t)
936+The data structure contains is the product of two other data structures:
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
943+The |Keyable| typeclass is used to extract the keys from the values that need to be stored.
945+The union of two maps is defined trivially -- by taking the union of the inner structures:
948+instance (Ord (Key t), Ord t)
949+ => Semigroup (MultiKeyedMap t) where
950+ (MultiKeyedMap x x') <> (MultiKeyedMap y y') =
952+ (M.unionWith S.union x y) (x' <> y')
955+Creating a singleton map from a single values is defined like this:
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
967+With these operations defining the |insert| operation becomes trivial:
972+ => t -> MultiKeyedMap t -> MultiKeyedMap t
973+insert t m = m <> singleton t
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):
981+ => Key t -> MultiKeyedMap t -> S.Set t
982+lookup k (MultiKeyedMap m _) =
983+ fromMaybe S.empty $ M.lookup k m
986+\subsection{Closing over type variables}
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:
991+ \item are not present in the type
992+ \item are used in an outer lexical scope (environment)
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.
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.
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:
1004+ | SubTypeVariable Int Int
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.
805\section{Possible improvements}
1009\section{Possible improvements}