6 \frametitle{\textsc{SPLT
}}
7 \begin{block
}{Features
}
9 \item Implementation language:
10 Clean (
{\tiny\url{http://clean.cs.ru.nl
}})
12 \item State transformer monad
\pause%
14 :: Gamma :== (Map String Type,
[String
])
15 :: Env a :== StateT Gamma (Either SemError) a
17 \item Preferably we want to have an
\CI{Either
} monad transformer
18 but clean does not have that
\ldots
23 \begin{frame
}[fragile
]
24 \frametitle{Grammar changes
}
27 \item Function type:
\pause%
29 <FunType> ::= <VoidType>
['->' <FunType>
]
30 <VoidType> ::= <Void> | Type
34 append(l1, l2) ::
[t
] ->
[t
] ->
[t
] {
38 \pause\item We check in the semantic analysis that
\CI{Void
} is only in
40 \pause\item This is for future higher-order functions
44 \begin{frame
}[fragile
]
45 \frametitle{What do we analyze exactly?
}
47 :: Pos =
{line :: Int, col :: Int
}
48 :: SemOutput :== Either
[SemError
] (AST, Gamma)
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
57 sem :: AST -> SemOutput
61 \begin{frame
}[fragile
]
64 \begin{block
}{Scoping?
}
65 Local variables get a new name and are changed in the function body.
69 Does matter for variables, not for functions.
72 \item Note that this means that
\CI{ones=
1:ones
} is
75 \item Functions which have not been encountered yet are temporarily
80 \begin{block
}{Mutual recursion?
}
84 \begin{block
}{Higher order functions?
}
85 Would be an interesting idea for assignment
4
89 \begin{frame
}[fragile
]
90 \frametitle{Mutual Recursion
}
92 \item Mutual recursion is allowed and type checked, however inference is
96 flip(n, l) :: Int ->
[Int
] ->
[Int
] {
97 if( n <=
0 )
{return l;
}
98 else
{return flop(n-
1,
0:l);
}
101 flop(n, l) :: Int ->
[Int
] ->
[Int
] {
106 \item Completely typed specifications are checked correctly.
110 \begin{frame
}[fragile
]
111 \frametitle{Mutual Recursion
}
113 \item Mutual recursion is allowed and type checked, however inference is
116 flip(n, l) :: Int ->
[Int
] ->
[Int
] {
117 if( n <=
0 )
{return l;
}
118 else
{return flop(n-
1,
0:l);
}
121 flop(n, l) :: Int ->
[Int
] -> Bool
{
126 \item It is also correctly determined that
\CI{Bool
} and the return
127 type of
\CI{flip(n,l)
} don't match.
131 \begin{frame
}[fragile
]
132 \frametitle{Mutual Recursion
}
134 \item Mutual recursion is allowed and type checked, however inference is
138 if( n <=
0 )
{return l;
}
139 else
{return flop(n-
1,
0:l);
}
149 \begin{frame
}[fragile
]
150 \frametitle{Mutual Recursion
}
152 \item Mutual recursion is allowed and type checked, however inference is
155 flip(n, l) :: Int ->
[Int
] -> vTqhp
{
156 if( n <=
0 )
{return l;
}
157 else
{return flop(n-
1,
0:l);
}
160 flop(n, l) :: Int ->
[Int
] -> HSWdn
{
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.
169 \begin{frame
}[fragile
]
170 \frametitle{But wait, there is more!
}
171 \framesubtitle{Trouble that is
}
173 \item Polymorphism is not working great either.
180 \item Is typed fine, but when we introduce:
187 2:
12 SemError: Cannot unify types. Expected: Int. Given: Bool
192 \begin{frame
}[fragile
]
193 \frametitle{It is not all trouble
}
194 \begin{block
}{A lot of functionality works correctly
}
196 \item Typing of
\CI{VarDecls
}
198 \item Typing of type chains:
200 id_poly_wtf(x) :: a -> a
212 \begin{frame
}[fragile
]
213 \frametitle{It is not all trouble
}
214 \begin{block
}{A lot of functionality works correctly
}
216 \item Typing of
\CI{VarDecls
}
217 \item Typing of type chains:
219 id_poly_wtf(x) :: a -> a
228 \item Typing
\CI{var l =
1:
2:
[];
} succeeds \\
229 while.
\CI{var l =
[]; var x = True:l; var y =
1:l;
} fails
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.
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.
246 \begin{block
}{Inference for functions is a completely different story
}
248 \item Type checking for functions works very well
249 \item Type inference for functions works spotty at best
254 \begin{frame
}[fragile
]
255 \frametitle{We changed to much from the presented algorithms
}
257 \item Our type checker is written with the origin algorithm
260 \item We were confident that that would be sufficient and we would be
261 able to implement type inference this way.
263 \item As it turns out,
\emph{we couldn't
}!
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!
}
274 \begin{block
}{We can fix the type inference after code generation
}
275 And this time do it right.
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
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
292 \item[Reader
] Reader environment to read fresh type variable
293 \item[Writer
] Write constraints to
\CI{Constraint
} environment
295 \item[Transformer
] (Either SemError)
297 \emph{\small Sadly these monads are not in the Clean library.
}\\
299 Then solve with a Relatively simple Solver-Monad
301 :: Solve a = StateT Unifier (Either TypeError) a
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