Agdarsec - total parser combinators

Guillaume Allais

Agdarsec - total parser combinators

Guillaume Allais^*

^*Corresponding author for this work

Research output: Contribution to conference › Paper › peer-review

2 Citations (Scopus)

32 Downloads (Pure)

Abstract

Parser combinator libraries represent parsers as functions and, using higher-order functions, define a DSL of combinators allowing users to quickly put together programs capable of handling complex recursive grammars. When moving to total functional languages such as Agda, these programs cannot be directly ported: there is nothing in the original definitions guaranteeing termination. In this paper, we will introduce a 'guarded' modal operator acting on types and show how it allows us to give more precise types to existing combinators thus guaranteeing totality.

Original language	English
Pages	45-59
Number of pages	15
Publication status	Published - 12 Feb 2018
Event	Vingt-neuviemes Journees Francophones des Langages Applicatifs, JFLA 2018 - 29th French-Speaking Conference on Applicative Languages, JFLA 2018 - Banyuls-sur-Mer, France Duration: 24 Jan 2018 → 27 Jan 2018

Conference

Conference	Vingt-neuviemes Journees Francophones des Langages Applicatifs, JFLA 2018 - 29th French-Speaking Conference on Applicative Languages, JFLA 2018
Country/Territory	France
City	Banyuls-sur-Mer
Period	24/01/18 → 27/01/18

Keywords

total parser combinators
higher-order functions
total functional languages

Access to Document

Allais-JFLA2018-Agdarsec-total-parser-combinatorsFinal published version, 310 KB

https://inria.hal.science/hal-01707376/

Cite this

@conference{fe80a50c376c4e50acd24e1ceb554e14,

title = "Agdarsec - total parser combinators",

abstract = "Parser combinator libraries represent parsers as functions and, using higher-order functions, define a DSL of combinators allowing users to quickly put together programs capable of handling complex recursive grammars. When moving to total functional languages such as Agda, these programs cannot be directly ported: there is nothing in the original definitions guaranteeing termination. In this paper, we will introduce a 'guarded' modal operator acting on types and show how it allows us to give more precise types to existing combinators thus guaranteeing totality.",

keywords = "total parser combinators, higher-order functions, total functional languages",

author = "Guillaume Allais",

note = "Publisher Copyright: {\textcopyright} JFLA 2018 - Journees Francophones des Langages Applicatifs. All rights reserved. Sylvie Boldo, Nicolas Magaud. Journ{\'e}es Francophones des Langages Applicatifs 2018. Sylvie Boldo; Nicolas Magaud. Journ{\'e}es Francophones des Langages Applicatifs 2018, Jan 2018, Banyuls-sur-Mer, France. publi{\'e} par les auteurs, 2018. ⟨hal-01707376⟩; Vingt-neuviemes Journees Francophones des Langages Applicatifs, JFLA 2018 - 29th French-Speaking Conference on Applicative Languages, JFLA 2018 ; Conference date: 24-01-2018 Through 27-01-2018",

year = "2018",

month = feb,

day = "12",

language = "English",

pages = "45--59",

}

TY - CONF

T1 - Agdarsec - total parser combinators

AU - Allais, Guillaume

N1 - Publisher Copyright: © JFLA 2018 - Journees Francophones des Langages Applicatifs. All rights reserved. Sylvie Boldo, Nicolas Magaud. Journées Francophones des Langages Applicatifs 2018. Sylvie Boldo; Nicolas Magaud. Journées Francophones des Langages Applicatifs 2018, Jan 2018, Banyuls-sur-Mer, France. publié par les auteurs, 2018. ⟨hal-01707376⟩

PY - 2018/2/12

Y1 - 2018/2/12

N2 - Parser combinator libraries represent parsers as functions and, using higher-order functions, define a DSL of combinators allowing users to quickly put together programs capable of handling complex recursive grammars. When moving to total functional languages such as Agda, these programs cannot be directly ported: there is nothing in the original definitions guaranteeing termination. In this paper, we will introduce a 'guarded' modal operator acting on types and show how it allows us to give more precise types to existing combinators thus guaranteeing totality.

AB - Parser combinator libraries represent parsers as functions and, using higher-order functions, define a DSL of combinators allowing users to quickly put together programs capable of handling complex recursive grammars. When moving to total functional languages such as Agda, these programs cannot be directly ported: there is nothing in the original definitions guaranteeing termination. In this paper, we will introduce a 'guarded' modal operator acting on types and show how it allows us to give more precise types to existing combinators thus guaranteeing totality.

KW - total parser combinators

KW - higher-order functions

KW - total functional languages

UR - https://gallais.github.io/pdf/agdarsec18.pdf

M3 - Paper

AN - SCOPUS:85093875701

SP - 45

EP - 59

T2 - Vingt-neuviemes Journees Francophones des Langages Applicatifs, JFLA 2018 - 29th French-Speaking Conference on Applicative Languages, JFLA 2018

Y2 - 24 January 2018 through 27 January 2018

ER -

Agdarsec - total parser combinators

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this