Towards size-dependent types for array programming

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

We present a type system for expressing size constraints on array types in an ML-style type system. The goal is to detect shape mismatches at compile-time, while being simpler than full dependent types. The main restrictions is that the only terms that can occur in types are array sizes, and syntactically they must be variables or constants. For those programs where this is not sufficient, we support a form of existential types, with the type system automatically managing the requisite book-keeping. We formalise a large subset of the type system in a small core language, which we prove sound. We also present an integration of the type system in the high-performance parallel functional language Futhark, and show on a collection of 44 representative programs that the restrictions in the type system are not too problematic in practice.

OriginalsprogEngelsk
TitelARRAY 2021 - Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming, co-located with PLDI 2021
RedaktørerTze Meng Low, Jeremy Gibbons
Antal sider14
ForlagAssociation for Computing Machinery, Inc.
Publikationsdato2021
Sider1-14
Artikelnummer3464310
ISBN (Elektronisk)978-1-4503-8466-7
DOI
StatusUdgivet - 2021
Begivenhed7th ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming, ARRAY 2021, held in association with PLDI 2021 - Virtual, Online, Canada
Varighed: 21 jun. 2021 → …

Konference

Konference7th ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming, ARRAY 2021, held in association with PLDI 2021
LandCanada
ByVirtual, Online
Periode21/06/2021 → …
SponsorACM SIGPLAN

Bibliografisk note

Funding Information:
This research has been partially supported by a grant from the Independent Research Fund Denmark, under the research project FUTHARK: Functional Technology for High-performance Architectures.

Publisher Copyright:
© 2021 ACM.

ID: 306899589