6 \frametitle{\textsc{SPLS
}}
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{flop(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);
}
150 \begin{frame
}[fragile
]
151 \frametitle{Mutual Recursion
}
153 \item Mutual recursion is allowed and type checked, however inference is
156 flip(n, l) :: Int ->
[Int
] -> vTqhp
{
157 if( n <=
0 )
{return l;
}
158 else
{return flop(n-
1,
0:l);
}
161 flop(n, l) :: Int ->
[Int
] -> HSWdn
{
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.
170 \begin{frame
}[fragile
]
171 \frametitle{But wait, there is more!
}
172 \framesubtitle{Trouble that is
}
174 \item Polymorphism is not working great either.
181 \item Is typed fine, but when we introduce:
188 2:
12 SemError: Cannot unify types. Expected: Int. Given: Bool
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.
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.
206 \begin{block
}{Inference for functions is a completely different story
}
208 \item Type checking for functions works very well
209 \item Type inference for functions works spotty at best
214 \begin{frame
}[fragile
]
215 \frametitle{We changed to much from the presented algorithms
}
217 \item Our type checker is written with the origin algorithm
220 \item We were confident that that would be sufficient and we would be
221 able to implement type inference this way.
223 \item As it turns out,
\emph{we couldn't
}!
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!
}
234 \begin{block
}{We can fix the type inference after code generation
}
235 And this time do it right.
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
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
250 \item[Reader
] Reader environment to read fresh type variable
251 \item[Writer
] Write constraints to
\CI{Constraint
} environment
253 \item[Transformer
] (Either SemError)
255 \emph{Sadly these monads are not in the Clean library.
}\\
256 Then solve with a Relatively simple Solver-Monad
258 :: Solve a = StateT Unifier (Either TypeError) a
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