A carregar...
Publicação
Type-checking Linearity in Core: Semantic Linearity for a Lazy Optimising Compiler
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 3.71 MB | Adobe PDF |
Orientador(es)
Resumo(s)
Linear type systems guarantee linear resources are used exactly once. Traditionally, using
a resource is synonymous with its syntactic occurrence in the program, however, under
the lens of lazy evaluation, linearity can be further understood semantically, where a syntactic occurrence of a resource does not necessarily entail using that resource when the
program is evaluated. Semantic linearity is especially necessary in optimising compilers
for languages combining linearity and laziness: optimisations leverage laziness to heavily
rewrite the source program, pushing the interaction of linearity and laziness to its limit,
regardless of the original program typing linearity conservatively. We present Linear Core,
the first type system that understands semantic linearity in the presence of laziness, suit-
able for the Core intermediate language of the Glasgow Haskell Compiler. We prove Linear
Core is both type safe and that multiple optimising transformations preserve linearity in
Linear Core while failing to do so in Core. We have implemented Linear Core as a compiler
plugin to validate the system against linearity-heavy libraries, including linear-base, in
the heart of the compiler.
Num sistema de tipos linear, recursos lineares têm de ser usados exatamente uma vez. Usar um recurso linear costuma ser equivalente a uma ocorrência sintática do mesmo no programa, no entanto, sob a perspectiva de avaliação lazy, a linearidade pode ser também compreendida de forma semântica, observando que uma ocorrência sintática de um recurso não significa necessariamente que esse recurso seja usado quando o programa é avaliado. Linearidade semântica é particularmente relevante em compiladores que optimizam linguagens com linearidade e laziness: a laziness permite ao compilador transformar consideravelmente o programa original, de tal forma que a interacção entre linearidade e laziness é levada ao extremo, independentemente de como a linearidade foi tipificada no programa original. Desenvolvemos o primeiro sistema de tipos (Linear Core) que compreende linearidade semântica na presença de laziness, um sistema adequado para a linguagem intermédia (Core) do Glasgow Haskell Compiler. Provamos que o sistema é type safe e que várias optimizações preservam linearidade no Linear Core, apesar de as mesmas não a preservarem no Core. Implementamos o Linear Core como um plugin para o compilador com o objectivo de validar o sistema em bibliotecas lineares populares.
Num sistema de tipos linear, recursos lineares têm de ser usados exatamente uma vez. Usar um recurso linear costuma ser equivalente a uma ocorrência sintática do mesmo no programa, no entanto, sob a perspectiva de avaliação lazy, a linearidade pode ser também compreendida de forma semântica, observando que uma ocorrência sintática de um recurso não significa necessariamente que esse recurso seja usado quando o programa é avaliado. Linearidade semântica é particularmente relevante em compiladores que optimizam linguagens com linearidade e laziness: a laziness permite ao compilador transformar consideravelmente o programa original, de tal forma que a interacção entre linearidade e laziness é levada ao extremo, independentemente de como a linearidade foi tipificada no programa original. Desenvolvemos o primeiro sistema de tipos (Linear Core) que compreende linearidade semântica na presença de laziness, um sistema adequado para a linguagem intermédia (Core) do Glasgow Haskell Compiler. Provamos que o sistema é type safe e que várias optimizações preservam linearidade no Linear Core, apesar de as mesmas não a preservarem no Core. Implementamos o Linear Core como um plugin para o compilador com o objectivo de validar o sistema em bibliotecas lineares populares.