File Download
There are no files associated with this item.
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1007/978-3-319-47958-3_14
- Scopus: eid_2-s2.0-84992472503
- WOS: WOS:000916326200014
Supplementary
- Citations:
- Appears in Collections:
Conference Paper: Unified Syntax with Iso-types
Title | Unified Syntax with Iso-types |
---|---|
Authors | |
Keywords | Typing Rule Functional Language Language Construct Parallel Reduction Type Check |
Issue Date | 2016 |
Publisher | Springer. |
Citation | Proceedings of the 14th Asian Symposium on Programming Languages and Systems (APLAS) 2016, Hanoi, Vietnam, 21-23 November 2016, p. 251-270 How to Cite? |
Abstract | Traditional designs for functional languages (such as Haskell or ML) have separate sorts of syntax for terms and types. In contrast, many dependently typed languages use a unified syntax that accounts for both terms and types. Unified syntax has some interesting advantages over separate syntax, including less duplication of concepts, and added expressiveness. However, integrating unrestricted general recursion in calculi with unified syntax is challenging when some level of type-level computation is present, as decidable type-checking is easily lost.
This paper argues that the advantages of unified syntax also apply to traditional functional languages, and there is no need to give up decidable type-checking. We present a dependently typed calculus that uses unified syntax, supports general recursion and has decidable type-checking. The key to retain decidable type-checking is a generalization of iso-recursive types called iso-types. Iso-types replace the conversion rule typically used in dependently typed calculus, and make every computation explicit via cast operators. We study two variants of the calculus that differ on the reduction strategy employed by the cast operators, and give different trade-offs in terms of simplicity and expressiveness. |
Persistent Identifier | http://hdl.handle.net/10722/301412 |
ISBN | |
ISI Accession Number ID | |
Series/Report no. | Lecture Notes in Computer Science (LNCS) ; v. 10017 |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Yang, Y | - |
dc.contributor.author | Bi, X | - |
dc.contributor.author | Dos Santos Oliveira, BC | - |
dc.date.accessioned | 2021-07-27T08:10:41Z | - |
dc.date.available | 2021-07-27T08:10:41Z | - |
dc.date.issued | 2016 | - |
dc.identifier.citation | Proceedings of the 14th Asian Symposium on Programming Languages and Systems (APLAS) 2016, Hanoi, Vietnam, 21-23 November 2016, p. 251-270 | - |
dc.identifier.isbn | 9783319479576 | - |
dc.identifier.uri | http://hdl.handle.net/10722/301412 | - |
dc.description.abstract | Traditional designs for functional languages (such as Haskell or ML) have separate sorts of syntax for terms and types. In contrast, many dependently typed languages use a unified syntax that accounts for both terms and types. Unified syntax has some interesting advantages over separate syntax, including less duplication of concepts, and added expressiveness. However, integrating unrestricted general recursion in calculi with unified syntax is challenging when some level of type-level computation is present, as decidable type-checking is easily lost. This paper argues that the advantages of unified syntax also apply to traditional functional languages, and there is no need to give up decidable type-checking. We present a dependently typed calculus that uses unified syntax, supports general recursion and has decidable type-checking. The key to retain decidable type-checking is a generalization of iso-recursive types called iso-types. Iso-types replace the conversion rule typically used in dependently typed calculus, and make every computation explicit via cast operators. We study two variants of the calculus that differ on the reduction strategy employed by the cast operators, and give different trade-offs in terms of simplicity and expressiveness. | - |
dc.language | eng | - |
dc.publisher | Springer. | - |
dc.relation.ispartof | Proceedings of the 14th Asian Symposium on Programming Languages and Systems (APLAS) 2016 | - |
dc.relation.ispartofseries | Lecture Notes in Computer Science (LNCS) ; v. 10017 | - |
dc.subject | Typing Rule | - |
dc.subject | Functional Language | - |
dc.subject | Language Construct | - |
dc.subject | Parallel Reduction | - |
dc.subject | Type Check | - |
dc.title | Unified Syntax with Iso-types | - |
dc.type | Conference_Paper | - |
dc.identifier.email | Dos Santos Oliveira, BC: bruno@cs.hku.hk | - |
dc.identifier.authority | Dos Santos Oliveira, BC=rp01786 | - |
dc.description.nature | link_to_subscribed_fulltext | - |
dc.identifier.doi | 10.1007/978-3-319-47958-3_14 | - |
dc.identifier.scopus | eid_2-s2.0-84992472503 | - |
dc.identifier.hkuros | 323713 | - |
dc.identifier.spage | 251 | - |
dc.identifier.epage | 270 | - |
dc.identifier.isi | WOS:000916326200014 | - |
dc.publisher.place | Cham | - |