deliverables/p2/p2.tex

   1 %&p2
   2 \begin{document}
   3 \frame{\titlepage}
   4
   5 \begin{frame}[fragile]
   6         \frametitle{\textsc{SPLS}}
   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{flop(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
 150 \begin{frame}[fragile]
 151         \frametitle{Mutual Recursion}
 152         \begin{itemize}
 153                 \item Mutual recursion is allowed and type checked, however inference is
 154                 not complete.
 155                 \begin{CleanCode}
 156 flip(n, l) :: Int -> [Int] -> vTqhp {
 157   if( n <= 0 ) {return l;}
 158   else {return flop(n-1, 0:l);}
 159 }
 160
 161 flop(n, l) :: Int -> [Int] -> HSWdn {
 162   return flip(n, 1:l);
 163 }
 164                 \end{CleanCode}
 165                 \item However when no type information is given at all our algorithm
 166                 fails to correctly infer the result type of the two function.
 167         \end{itemize}
 168 \end{frame}
 169
 170 \begin{frame}[fragile]
 171         \frametitle{But wait, there is more!}
 172         \framesubtitle{Trouble that is}
 173         \begin{itemize}
 174                 \item Polymorphism is not working great either.
 175                 \begin{CleanCode}
 176 id(x) :: a -> a {
 177     return x;
 178 }
 179                 \end{CleanCode}
 180                 \pause
 181                 \item Is typed fine, but when we introduce:
 182                 \begin{CleanCode}
 183 var x = id(5);
 184 var y = id(True);
 185                 \end{CleanCode}
 186                 \pause
 187                 \begin{CleanCode}
 188 2:12 SemError: Cannot unify types. Expected: Int. Given: Bool
 189                 \end{CleanCode}
 190         \end{itemize}
 191 \end{frame}
 192
 193 \begin{frame}[fragile]
 194         \frametitle{But wait, there is more!}
 195         \framesubtitle{Trouble that is}
 196                 \begin{block}{Our type inference algorithm is too greedy}
 197                         It globally types a function once it is applied to a value, even
 198                         if this types it more specified then needed.
 199                 \end{block}
 200                 \pause
 201                 \begin{block}{Basically type inference for \CI{VarDecl} works great}
 202                         All instances of VarDecl work well. Including those where a var is
 203                         assigned by function application.
 204                 \end{block}
 205                 \pause
 206                 \begin{block}{Inference for functions is a completely different story}
 207                         \begin{itemize}
 208                                 \item Type checking for functions works very well
 209                                 \item Type inference for functions works spotty at best
 210                         \end{itemize}
 211                 \end{block}
 212 \end{frame}
 213
 214 \begin{frame}[fragile]
 215         \frametitle{We changed to much from the presented algorithms}
 216         \begin{itemize}
 217                 \item Our type checker is written with the origin algorithm
 218                         \emph{in mind}
 219                 \pause
 220                 \item We were confident that that would be sufficient and we would be
 221                         able to implement type inference this way.
 222                 \pause
 223                 \item As it turns out, \emph{we couldn't}!
 224         \end{itemize}
 225 \end{frame}
 226
 227 \begin{frame}[fragile]
 228         \frametitle{This not a problem for code generation}
 229         \begin{block}{Sufficiently typed programs can be generated}
 230                 When all functions in the SPL program are completely typed then the
 231                 type inference algorithm yields a fully typed AST.\\
 232                 \CI{VarDecls} \emph{types are correctly infered!}
 233         \end{block}
 234         \begin{block}{We can fix the type inference after code generation}
 235                 And this time do it right.
 236         \end{block}
 237 \end{frame}
 238
 239 \begin{frame}[fragile]
 240         \frametitle{Doing it right}
 241         \framesubtitle{How we will redo the type inference}
 242         \begin{block}{Properly implement the \emph{exact} algorithm}
 243                 We will implement the Hindley-Miller algorithm exactly instead of
 244                 \emph{``kinda''}
 245         \end{block}
 246         \begin{block}{Split constraint generation and solving}
 247                 Hide all the nasty details of constraint generation using a
 248                 Reader-Writer-State-Transformer-Monad
 249                 \begin{description}
 250                         \item[Reader] Reader environment to read fresh type variable
 251                         \item[Writer] Write constraints to \CI{Constraint} environment
 252                         \item[State] Gamma
 253                         \item[Transformer] (Either SemError)
 254                 \end{description}
 255                 \emph{Sadly these monads are not in the Clean library.}\\
 256                 Then solve with a Relatively simple Solver-Monad
 257                 \begin{CleanCode}
 258 :: Solve a = StateT Unifier (Either TypeError) a
 259                 \end{CleanCode}
 260         \end{block}
 261 \end{frame}
 262
 263 % - Can functions that are defined later in a file call earlier defined functions?
 264 % - Can local variables be defined in terms of other local variables?
 265 % - How do you deal with assignments?
 266 % - Tell us if and how you include the value restriction.
 267 %- How do you deal with recursion?
 268 %- How do you deal with multiple recursion?
 269 %- If you forbid multiple recursion, how do you do so?
 270 % - Does your language support higher-order functions?
 271 % - How do you deal with polymorphism?
 272 % - How do you deal with overloading?
 273 % - How does the absence/presence of type signatures influence your type
 274 %  checker?
 275 \end{document}