deliverables/p2/p2.tex

   1 %&p2
   2 \begin{document}
   3 \frame{\titlepage}
   4
   5 \begin{frame}[fragile]
   6         \frametitle{\textsc{SPLT}}
   7         \begin{block}{Features}
   8                 \begin{itemize}
   9                         \item Implementation language:
  10                                 Clean ({\tiny\url{http://clean.cs.ru.nl}})
  11                         \pause%
  12                         \item State transformer monad\pause%
  13                                 \begin{CleanCode}
  14 :: Gamma :== (Map String Type, [String])
  15 :: Env a :== StateT Gamma (Either SemError) a
  16                                 \end{CleanCode}
  17                         \item Preferably we want to have an \CI{Either} monad transformer
  18                                 but clean does not have that\ldots
  19                 \end{itemize}
  20         \end{block}
  21 \end{frame}
  22
  23 \begin{frame}[fragile]
  24         \frametitle{Grammar changes}
  25
  26         \begin{itemize}
  27                 \item Function type:\pause%
  28                         \begin{CleanCode}
  29 <FunType>  ::= <VoidType> ['->' <FunType>]
  30 <VoidType> ::= <Void> | Type
  31                         \end{CleanCode}
  32                 \pause Example%
  33                         \begin{CleanCode}
  34 append(l1, l2) :: [t] -> [t] -> [t] {
  35     ...
  36 }
  37                         \end{CleanCode}
  38                 \pause\item We check in the semantic analysis that \CI{Void} is only in
  39                         the last type.
  40                 \pause\item This is for future higher-order functions
  41         \end{itemize}
  42 \end{frame}
  43
  44 \begin{frame}[fragile]
  45         \frametitle{What do we analyze exactly?}
  46         \begin{CleanCode}
  47 :: Pos = {line :: Int, col :: Int}
  48 :: SemOutput :== Either [SemError] (AST, Gamma)
  49 :: SemError
  50     = ParseError Pos String                     // Post-parse errors
  51     | UnifyError Pos Type Type                  // Unification
  52     | FieldSelectorError Pos Type FieldSelector // hd, tail, fst, snd
  53     | OperatorError Pos Op2 Type                // 'a' == 5
  54     | UndeclaredVariableError Pos String        // Variable ordering
  55     | Error String
  56
  57 sem :: AST -> SemOutput
  58         \end{CleanCode}
  59 \end{frame}
  60
  61 \begin{frame}[fragile]
  62         \frametitle{Analyses}
  63         \pause%
  64         \begin{block}{Scoping?}
  65                 Local variables get a new name and are changed in the function body.
  66         \end{block}
  67         \pause%
  68         \begin{block}{Order?}
  69                 Does matter for variables, not for functions.
  70                 \pause
  71                 \begin{itemize}
  72                         \item Note that this means that \CI{ones=1:ones} is
  73                                         not allowed.
  74                         \pause
  75                         \item Functions which have not been encountered yet are temporarily
  76                                 typed $\alpha$.
  77                 \end{itemize}
  78         \end{block}
  79         \pause%
  80         \begin{block}{Mutual recursion?}
  81                 Yep!
  82         \end{block}
  83         \pause%
  84         \begin{block}{Higher order functions?}
  85                 Would be an interesting idea for assignment 4
  86         \end{block}
  87 \end{frame}
  88
  89 \begin{frame}[fragile]
  90         \frametitle{Mutual Recursion}
  91         \begin{itemize}
  92                 \item Mutual recursion is allowed and type checked, however inference is
  93                 not complete.
  94                 \pause
  95                 \begin{CleanCode}
  96 flip(n, l) :: Int -> [Int] -> [Int] {
  97   if( n <= 0 ) {return l;}
  98   else {return flop(n-1, 0:l);}
  99 }
 100
 101 flop(n, l) :: Int -> [Int] -> [Int] {
 102   return flip(n, 1:l);
 103 }
 104                 \end{CleanCode}
 105                 \pause
 106                 \item Completely typed specifications are checked correctly.
 107         \end{itemize}
 108 \end{frame}
 109
 110 \begin{frame}[fragile]
 111         \frametitle{Mutual Recursion}
 112         \begin{itemize}
 113                 \item Mutual recursion is allowed and type checked, however inference is
 114                 not complete.
 115                 \begin{CleanCode}
 116 flip(n, l) :: Int -> [Int] -> [Int] {
 117   if( n <= 0 ) {return l;}
 118   else {return flop(n-1, 0:l);}
 119 }
 120
 121 flop(n, l) :: Int -> [Int] -> Bool {
 122   return flip(n, 1:l);
 123 }
 124                 \end{CleanCode}
 125                 \pause
 126                 \item It is also correctly determined that \CI{Bool} and the return
 127                 type of \CI{flip(n,l)} don't match.
 128         \end{itemize}
 129 \end{frame}
 130
 131 \begin{frame}[fragile]
 132         \frametitle{Mutual Recursion}
 133         \begin{itemize}
 134                 \item Mutual recursion is allowed and type checked, however inference is
 135                 not complete.
 136                 \begin{CleanCode}
 137 flip(n, l) {
 138   if( n <= 0 ) {return l;}
 139   else {return flop(n-1, 0:l);}
 140 }
 141
 142 flop(n, l) {
 143   return flip(n, 1:l);
 144 }
 145                 \end{CleanCode}
 146         \end{itemize}
 147 \end{frame}
 148
 149 \begin{frame}[fragile]
 150         \frametitle{Mutual Recursion}
 151         \begin{itemize}
 152                 \item Mutual recursion is allowed and type checked, however inference is
 153                 not complete.
 154                 \begin{CleanCode}
 155 flip(n, l) :: Int -> [Int] -> vTqhp {
 156   if( n <= 0 ) {return l;}
 157   else {return flop(n-1, 0:l);}
 158 }
 159
 160 flop(n, l) :: Int -> [Int] -> HSWdn {
 161   return flip(n, 1:l);
 162 }
 163                 \end{CleanCode}
 164                 \item However when no type information is given at all our algorithm
 165                 fails to correctly infer the result type of the two function.
 166         \end{itemize}
 167 \end{frame}
 168
 169 \begin{frame}[fragile]
 170         \frametitle{But wait, there is more!}
 171         \framesubtitle{Trouble that is}
 172         \begin{itemize}
 173                 \item Polymorphism is not working great either.
 174                 \begin{CleanCode}
 175 id(x) :: a -> a {
 176     return x;
 177 }
 178                 \end{CleanCode}
 179                 \pause
 180                 \item Is typed fine, but when we introduce:
 181                 \begin{CleanCode}
 182 var x = id(5);
 183 var y = id(True);
 184                 \end{CleanCode}
 185                 \pause
 186                 \begin{CleanCode}
 187 2:12 SemError: Cannot unify types. Expected: Int. Given: Bool
 188                 \end{CleanCode}
 189         \end{itemize}
 190 \end{frame}
 191
 192 \begin{frame}[fragile]
 193         \frametitle{It is not all trouble}
 194         \begin{block}{A lot of functionality works correctly}
 195                 \begin{itemize}
 196                         \item Typing of \CI{VarDecls}
 197                         \pause
 198                         \item Typing of type chains:
 199                         \begin{CleanCode}
 200 id_poly_wtf(x) :: a -> a
 201 {
 202   var a = x;
 203   var b = a;
 204   var c = b;
 205   return c;
 206 }
 207                         \end{CleanCode}
 208                 \end{itemize}
 209         \end{block}
 210 \end{frame}
 211
 212 \begin{frame}[fragile]
 213         \frametitle{It is not all trouble}
 214         \begin{block}{A lot of functionality works correctly}
 215         \begin{itemize}
 216                 \item Typing of \CI{VarDecls}
 217                 \item Typing of type chains:
 218                 \begin{CleanCode}
 219 id_poly_wtf(x) :: a -> a
 220 {
 221   a a = x;
 222   a b = a;
 223   a c = b;
 224   return c;
 225 }
 226                 \end{CleanCode}
 227                 \pause
 228                 \item Typing \CI{var l = 1:2:[];} succeeds \\
 229                           while. \CI{var l = []; var x = True:l; var y = 1:l;} fails
 230         \end{itemize}
 231         \end{block}
 232 \end{frame}
 233
 234 \begin{frame}[fragile]
 235         \frametitle{Why is there so much trouble?}
 236                 \begin{block}{Our type inference algorithm is too greedy}
 237                         It globally types a function once it is applied to a value, even
 238                         if this types it more specified then needed.
 239                 \end{block}
 240                 \pause
 241                 \begin{block}{Basically type inference for \CI{VarDecl} works great}
 242                         All instances of VarDecl work well. Including those where a var is
 243                         assigned by function application.
 244                 \end{block}
 245                 \pause
 246                 \begin{block}{Inference for functions is a completely different story}
 247                         \begin{itemize}
 248                                 \item Type checking for functions works very well
 249                                 \item Type inference for functions works spotty at best
 250                         \end{itemize}
 251                 \end{block}
 252 \end{frame}
 253
 254 \begin{frame}[fragile]
 255         \frametitle{We changed to much from the presented algorithms}
 256         \begin{itemize}
 257                 \item Our type checker is written with the origin algorithm
 258                         \emph{in mind}
 259                 \pause
 260                 \item We were confident that that would be sufficient and we would be
 261                         able to implement type inference this way.
 262                 \pause
 263                 \item As it turns out, \emph{we couldn't}!
 264         \end{itemize}
 265 \end{frame}
 266
 267 \begin{frame}[fragile]
 268         \frametitle{This not a problem for code generation}
 269         \begin{block}{Sufficiently typed programs can be generated}
 270                 When all functions in the SPL program are completely typed then the
 271                 type inference algorithm yields a fully typed AST.\\
 272                 \CI{VarDecls} \emph{types are correctly infered!}
 273         \end{block}
 274         \begin{block}{We can fix the type inference after code generation}
 275                 And this time do it right.
 276         \end{block}
 277 \end{frame}
 278
 279 \begin{frame}[fragile]
 280         \frametitle{Doing it right}
 281         \framesubtitle{How we will redo the type inference}
 282         \begin{block}{Properly implement the \emph{exact} algorithm}
 283                 We will implement the Hindley-Miller algorithm exactly instead of
 284                 \emph{``kinda''}
 285         \end{block}
 286         \pause
 287         \begin{block}{Split constraint generation and solving}
 288                 Hide all the nasty details of constraint generation using a
 289                 Reader-Writer-State-Transformer-Monad
 290                 \pause
 291                 \begin{description}
 292                         \item[Reader] Reader environment to read fresh type variable
 293                         \item[Writer] Write constraints to \CI{Constraint} environment
 294                         \item[State] Gamma
 295                         \item[Transformer] (Either SemError)
 296                 \end{description}
 297                 \emph{\small Sadly these monads are not in the Clean library.}\\
 298                 \pause
 299                 Then solve with a Relatively simple Solver-Monad
 300                 \begin{CleanCode}
 301 :: Solve a = StateT Unifier (Either TypeError) a
 302                 \end{CleanCode}
 303         \end{block}
 304 \end{frame}
 305
 306 % - Can functions that are defined later in a file call earlier defined functions?
 307 % - Can local variables be defined in terms of other local variables?
 308 % - How do you deal with assignments?
 309 % - Tell us if and how you include the value restriction.
 310 %- How do you deal with recursion?
 311 %- How do you deal with multiple recursion?
 312 %- If you forbid multiple recursion, how do you do so?
 313 % - Does your language support higher-order functions?
 314 % - How do you deal with polymorphism?
 315 % - How do you deal with overloading?
 316 % - How does the absence/presence of type signatures influence your type
 317 %  checker?
 318 \end{document}