WEKO3
アイテム
Lightweight Linearly-typed Programming with Lenses and Monads
https://ipsj.ixsq.nii.ac.jp/records/195819
https://ipsj.ixsq.nii.ac.jp/records/1958190680f315-1498-44b1-ad20-df882ee4ca9a
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO1202005.pdf (488.7 kB)
|
Copyright (c) 2019 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2019-05-21 | |||||||||
| タイトル | ||||||||||
| タイトル | Lightweight Linearly-typed Programming with Lenses and Monads | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | Lightweight Linearly-typed Programming with Lenses and Monads | |||||||||
| 言語 | ||||||||||
| 言語 | eng | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | [通常論文] OCaml, linear types, functional programming, monad, lens | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||||
| 資源タイプ | journal article | |||||||||
| 著者所属 | ||||||||||
| Faculty of Engineering, Gifu University | ||||||||||
| 著者所属 | ||||||||||
| Graduate School of Mathematics, Nagoya University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Faculty of Engineering, Gifu University | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Graduate School of Mathematics, Nagoya University | ||||||||||
| 著者名 |
Keigo, Imai
× Keigo, Imai
× Jacques, Garrigue
|
|||||||||
| 著者名(英) |
Keigo, Imai
× Keigo, Imai
× Jacques, Garrigue
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | This paper shows an encoding of linear types in OCaml and its applications. The encoding enables to write correct OCaml programs based on safe resource access guided by linear types. Linear types ensure that every variable is used exactly once, and, thus, they can be used to check the behavioural aspects of programs such as resource access and communication protocols in a static way. However, linear types require significant effort to be integrated into existing programming languages. Our encoding allows the vanilla OCaml typechecker to enforce linearity by using lenses and a parameterised monad. Parameterised monads are monads with a pre- and a post-condition, and we use them to track the creation and consumption of resources at the type level. Lenses, which point at parts of a data type, are used to refer to a resource in pre- and post-conditions. To handle comfortably structured data such as linearly typed lists, we further propose an extension to pattern matching based on the syntax-extension mechanism of OCaml. We show an application to static checking of communication protocols in OCaml. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.27(2019) (online) ------------------------------ |
|||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | This paper shows an encoding of linear types in OCaml and its applications. The encoding enables to write correct OCaml programs based on safe resource access guided by linear types. Linear types ensure that every variable is used exactly once, and, thus, they can be used to check the behavioural aspects of programs such as resource access and communication protocols in a static way. However, linear types require significant effort to be integrated into existing programming languages. Our encoding allows the vanilla OCaml typechecker to enforce linearity by using lenses and a parameterised monad. Parameterised monads are monads with a pre- and a post-condition, and we use them to track the creation and consumption of resources at the type level. Lenses, which point at parts of a data type, are used to refer to a resource in pre- and post-conditions. To handle comfortably structured data such as linearly typed lists, we further propose an extension to pattern matching based on the syntax-extension mechanism of OCaml. We show an application to static checking of communication protocols in OCaml. ------------------------------ This is a preprint of an article intended for publication Journal of Information Processing(JIP). This preprint should not be cited. This article should be cited as: Journal of Information Processing Vol.27(2019) (online) ------------------------------ |
|||||||||
| 書誌レコードID | ||||||||||
| 収録物識別子タイプ | NCID | |||||||||
| 収録物識別子 | AA11464814 | |||||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 12, 号 2, 発行日 2019-05-21 |
|||||||||
| ISSN | ||||||||||
| 収録物識別子タイプ | ISSN | |||||||||
| 収録物識別子 | 1882-7802 | |||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
