Towards size-dependent types for array programming
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
Towards size-dependent types for array programming. / Henriksen, Troels; Elsman, Martin.
ARRAY 2021 - Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming, co-located with PLDI 2021. red. / Tze Meng Low; Jeremy Gibbons. Association for Computing Machinery, Inc., 2021. s. 1-14 3464310.Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Towards size-dependent types for array programming
AU - Henriksen, Troels
AU - Elsman, Martin
N1 - Publisher Copyright: © 2021 ACM.
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
KW - functional programming
KW - parallel programming
KW - type systems
U2 - 10.1145/3460944.3464310
DO - 10.1145/3460944.3464310
M3 - Article in proceedings
AN - SCOPUS:85109012020
SP - 1
EP - 14
BT - ARRAY 2021 - Proceedings of the 7th ACM SIGPLAN International Workshop on Libraries, Languages and Compilers for Array Programming, co-located with PLDI 2021
A2 - Low, Tze Meng
A2 - Gibbons, Jeremy
PB - Association for Computing Machinery, Inc.
T2 - 7th ACM SIGPLAN International Workshop on Libraries, Languages, and Compilers for Array Programming, ARRAY 2021, held in association with PLDI 2021
Y2 - 21 June 2021
ER -
ID: 306899589