The Semantics of Miranda's Algebraic Types
Miranda has two interesting features in its typing system: implicit polymorphism (also known as ML-style polymorphism) and algebraic types. Algebraic types create new types from old and can operate on arbitrary types. This paper argues that functions of types, or type constructors, best represent th...
| Main Authors: | , |
|---|---|
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149135 |
| _version_ | 1826203919933505536 |
|---|---|
| author | Bruce, Kim B. Riecker, Jon G. |
| author_facet | Bruce, Kim B. Riecker, Jon G. |
| author_sort | Bruce, Kim B. |
| collection | MIT |
| description | Miranda has two interesting features in its typing system: implicit polymorphism (also known as ML-style polymorphism) and algebraic types. Algebraic types create new types from old and can operate on arbitrary types. This paper argues that functions of types, or type constructors, best represent the meaning of algebraic types. Building upon this idea, we develop a denotational semantics for algebraic types. We first define a typed lambda calculus that specifies type constructors. A semantic model of type constructors is them built, using the ideal model as a basis. (The ideal model gives the most natural semantics for Miranda's implicit polymorphism.) The model is shown to be sound with respect to this lambda calculus. FInally, we demonstrate how to use the model to interpret algebraic types, and prove that the translation produces elements in the model. |
| first_indexed | 2024-09-23T12:45:32Z |
| id | mit-1721.1/149135 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T12:45:32Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1491352023-03-30T03:43:28Z The Semantics of Miranda's Algebraic Types Bruce, Kim B. Riecker, Jon G. Miranda has two interesting features in its typing system: implicit polymorphism (also known as ML-style polymorphism) and algebraic types. Algebraic types create new types from old and can operate on arbitrary types. This paper argues that functions of types, or type constructors, best represent the meaning of algebraic types. Building upon this idea, we develop a denotational semantics for algebraic types. We first define a typed lambda calculus that specifies type constructors. A semantic model of type constructors is them built, using the ideal model as a basis. (The ideal model gives the most natural semantics for Miranda's implicit polymorphism.) The model is shown to be sound with respect to this lambda calculus. FInally, we demonstrate how to use the model to interpret algebraic types, and prove that the translation produces elements in the model. 2023-03-29T14:31:02Z 2023-03-29T14:31:02Z 1987-08 https://hdl.handle.net/1721.1/149135 MIT-LCS-TM-335 application/pdf |
| spellingShingle | Bruce, Kim B. Riecker, Jon G. The Semantics of Miranda's Algebraic Types |
| title | The Semantics of Miranda's Algebraic Types |
| title_full | The Semantics of Miranda's Algebraic Types |
| title_fullStr | The Semantics of Miranda's Algebraic Types |
| title_full_unstemmed | The Semantics of Miranda's Algebraic Types |
| title_short | The Semantics of Miranda's Algebraic Types |
| title_sort | semantics of miranda s algebraic types |
| url | https://hdl.handle.net/1721.1/149135 |
| work_keys_str_mv | AT brucekimb thesemanticsofmirandasalgebraictypes AT rieckerjong thesemanticsofmirandasalgebraictypes AT brucekimb semanticsofmirandasalgebraictypes AT rieckerjong semanticsofmirandasalgebraictypes |