Shape-Constrained Array Programming with Size-Dependent Types

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt

Standard

Shape-Constrained Array Programming with Size-Dependent Types. / Bailly, Lubin; Henriksen, Troels; Elsman, Martin.

FHPNC 2023 - Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, Co-located with ICFP 2023. red. / Gabriele Keller; Sam Westrick. Association for Computing Machinery, Inc., 2023. s. 29-41.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt

Harvard

Bailly, L, Henriksen, T & Elsman, M 2023, Shape-Constrained Array Programming with Size-Dependent Types. i G Keller & S Westrick (red), FHPNC 2023 - Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, Co-located with ICFP 2023. Association for Computing Machinery, Inc., s. 29-41, 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, FHPNC 2023, co-located with ICFP, Seattle, USA, 04/09/2023. https://doi.org/10.1145/3609024.3609412

APA

Bailly, L., Henriksen, T., & Elsman, M. (2023). Shape-Constrained Array Programming with Size-Dependent Types. I G. Keller, & S. Westrick (red.), FHPNC 2023 - Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, Co-located with ICFP 2023 (s. 29-41). Association for Computing Machinery, Inc.. https://doi.org/10.1145/3609024.3609412

Vancouver

Bailly L, Henriksen T, Elsman M. Shape-Constrained Array Programming with Size-Dependent Types. I Keller G, Westrick S, red., FHPNC 2023 - Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, Co-located with ICFP 2023. Association for Computing Machinery, Inc. 2023. s. 29-41 https://doi.org/10.1145/3609024.3609412

Author

Bailly, Lubin ; Henriksen, Troels ; Elsman, Martin. / Shape-Constrained Array Programming with Size-Dependent Types. FHPNC 2023 - Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, Co-located with ICFP 2023. red. / Gabriele Keller ; Sam Westrick. Association for Computing Machinery, Inc., 2023. s. 29-41

Bibtex

@inproceedings{8e8eeb39c42c46ec8bf50dc00282b884,
title = "Shape-Constrained Array Programming with Size-Dependent Types",
abstract = "We present a dependent type system for enforcing array-size consistency in an ML-style functional array language. Our goal is to enforce shape-consistency at compile time and allow nontrivial transformations on array shapes, without the complexity such features tend to introduce in dependently typed languages. Sizes can be arbitrary expressions and size equality is purely syntactical, which fits naturally within a scheme that interprets size-polymorphic functions as having implicit arguments. When non-syntactical equalities are needed, we provide dynamic checking. In contrast to other dependently typed languages, we automate the book-keeping involved in tracking existential sizes, such as when filtering arrays. We formalise a large subset of the presented type system and prove it sound. We also discuss how to adapt the type system for a real implementation, including type inference, within the Futhark programming language.",
keywords = "functional programming, parallel programming, type systems",
author = "Lubin Bailly and Troels Henriksen and Martin Elsman",
note = "Publisher Copyright: {\textcopyright} 2023 ACM.; 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, FHPNC 2023, co-located with ICFP ; Conference date: 04-09-2023",
year = "2023",
doi = "10.1145/3609024.3609412",
language = "English",
pages = "29--41",
editor = "Gabriele Keller and Sam Westrick",
booktitle = "FHPNC 2023 - Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, Co-located with ICFP 2023",
publisher = "Association for Computing Machinery, Inc.",

}

RIS

TY - GEN

T1 - Shape-Constrained Array Programming with Size-Dependent Types

AU - Bailly, Lubin

AU - Henriksen, Troels

AU - Elsman, Martin

N1 - Publisher Copyright: © 2023 ACM.

PY - 2023

Y1 - 2023

N2 - We present a dependent type system for enforcing array-size consistency in an ML-style functional array language. Our goal is to enforce shape-consistency at compile time and allow nontrivial transformations on array shapes, without the complexity such features tend to introduce in dependently typed languages. Sizes can be arbitrary expressions and size equality is purely syntactical, which fits naturally within a scheme that interprets size-polymorphic functions as having implicit arguments. When non-syntactical equalities are needed, we provide dynamic checking. In contrast to other dependently typed languages, we automate the book-keeping involved in tracking existential sizes, such as when filtering arrays. We formalise a large subset of the presented type system and prove it sound. We also discuss how to adapt the type system for a real implementation, including type inference, within the Futhark programming language.

AB - We present a dependent type system for enforcing array-size consistency in an ML-style functional array language. Our goal is to enforce shape-consistency at compile time and allow nontrivial transformations on array shapes, without the complexity such features tend to introduce in dependently typed languages. Sizes can be arbitrary expressions and size equality is purely syntactical, which fits naturally within a scheme that interprets size-polymorphic functions as having implicit arguments. When non-syntactical equalities are needed, we provide dynamic checking. In contrast to other dependently typed languages, we automate the book-keeping involved in tracking existential sizes, such as when filtering arrays. We formalise a large subset of the presented type system and prove it sound. We also discuss how to adapt the type system for a real implementation, including type inference, within the Futhark programming language.

KW - functional programming

KW - parallel programming

KW - type systems

U2 - 10.1145/3609024.3609412

DO - 10.1145/3609024.3609412

M3 - Article in proceedings

AN - SCOPUS:85174071185

SP - 29

EP - 41

BT - FHPNC 2023 - Proceedings of the 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, Co-located with ICFP 2023

A2 - Keller, Gabriele

A2 - Westrick, Sam

PB - Association for Computing Machinery, Inc.

T2 - 11th ACM SIGPLAN International Workshop on Functional High-Performance and Numerical Computing, FHPNC 2023, co-located with ICFP

Y2 - 4 September 2023

ER -

ID: 375210823