TyDe '18: "Typing, Representing, and ..."
Typing, Representing, and Abstracting Control: Functional Pearl
Philipp Schuster and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany)
A well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a family of control operators shifti and reseti. This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n control operators for the entire program upfront, but we allow different parts of the program to live at different levels. It turns out that taking shift0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. The translation avoids administrative beta- and eta-redexes at all levels of the CPS hierarchy, by iterating well-known techniques for the non-iterated CPS translation.
@InProceedings{TyDe18p14,
author = {Philipp Schuster and Jonathan Immanuel Brachthäuser},
title = {Typing, Representing, and Abstracting Control: Functional Pearl},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {14--24},
doi = {10.1145/3240719.3241788},
year = {2018},
}
Publisher's Version
TyDe '18: "Authenticated Modular Maps ..."
Authenticated Modular Maps in Haskell
Victor Cacciari Miraldo, Harold Carr, Alex Kogan, Mark Moir, and Maurice Herlihy
(Utrecht University, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; Brown University, USA)
We present hamm, a Haskell library that enables programmers to easily configure authenticated map (key-value store) implementations. We use type level programming techniques to establish an extensible foundation, and provide an example base map and several example “add on” transformers supporting features such as caches, Bloom filters and paging structures. Another add-on enables a prover to provide—and a verifier to verify—a “summary” containing only a small subset of the map’s data, and a verifier to receive and verify additional data only if needed. Preliminary performance results demonstrate significant potential for authenticated maps configured using hamm to support our goal of enabling participants to join blockchain networks faster.
@InProceedings{TyDe18p1,
author = {Victor Cacciari Miraldo and Harold Carr and Alex Kogan and Mark Moir and Maurice Herlihy},
title = {Authenticated Modular Maps in Haskell},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3240719.3241790},
year = {2018},
}
Publisher's Version
TyDe '18: "Extensible Type-Directed Editing ..."
Extensible Type-Directed Editing
Joomy Korkut and David Thrane Christiansen
(Wesleyan University, USA; Galois, USA)
Dependently typed programming languages, such as Idris and Agda, feature rich interactive environments that use informative types to assist users with the construction of programs. However, these environments have been provided by the authors of the language, and users have not had an easy way to extend and customize them. We address this problem by extending Idris's metaprogramming facilities with primitives for describing new type-directed editing features, making Idris's editors as extensible as its elaborator.
@InProceedings{TyDe18p38,
author = {Joomy Korkut and David Thrane Christiansen},
title = {Extensible Type-Directed Editing},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {38--50},
doi = {10.1145/3240719.3241791},
year = {2018},
}
Publisher's Version
TyDe '18: "Authenticated Modular Maps ..."
Authenticated Modular Maps in Haskell
Victor Cacciari Miraldo, Harold Carr, Alex Kogan, Mark Moir, and Maurice Herlihy
(Utrecht University, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; Brown University, USA)
We present hamm, a Haskell library that enables programmers to easily configure authenticated map (key-value store) implementations. We use type level programming techniques to establish an extensible foundation, and provide an example base map and several example “add on” transformers supporting features such as caches, Bloom filters and paging structures. Another add-on enables a prover to provide—and a verifier to verify—a “summary” containing only a small subset of the map’s data, and a verifier to receive and verify additional data only if needed. Preliminary performance results demonstrate significant potential for authenticated maps configured using hamm to support our goal of enabling participants to join blockchain networks faster.
@InProceedings{TyDe18p1,
author = {Victor Cacciari Miraldo and Harold Carr and Alex Kogan and Mark Moir and Maurice Herlihy},
title = {Authenticated Modular Maps in Haskell},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3240719.3241790},
year = {2018},
}
Publisher's Version
TyDe '18: "Authenticated Modular Maps ..."
Authenticated Modular Maps in Haskell
Victor Cacciari Miraldo, Harold Carr, Alex Kogan, Mark Moir, and Maurice Herlihy
(Utrecht University, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; Brown University, USA)
We present hamm, a Haskell library that enables programmers to easily configure authenticated map (key-value store) implementations. We use type level programming techniques to establish an extensible foundation, and provide an example base map and several example “add on” transformers supporting features such as caches, Bloom filters and paging structures. Another add-on enables a prover to provide—and a verifier to verify—a “summary” containing only a small subset of the map’s data, and a verifier to receive and verify additional data only if needed. Preliminary performance results demonstrate significant potential for authenticated maps configured using hamm to support our goal of enabling participants to join blockchain networks faster.
@InProceedings{TyDe18p1,
author = {Victor Cacciari Miraldo and Harold Carr and Alex Kogan and Mark Moir and Maurice Herlihy},
title = {Authenticated Modular Maps in Haskell},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3240719.3241790},
year = {2018},
}
Publisher's Version
TyDe '18: "Extensible Type-Directed Editing ..."
Extensible Type-Directed Editing
Joomy Korkut and David Thrane Christiansen
(Wesleyan University, USA; Galois, USA)
Dependently typed programming languages, such as Idris and Agda, feature rich interactive environments that use informative types to assist users with the construction of programs. However, these environments have been provided by the authors of the language, and users have not had an easy way to extend and customize them. We address this problem by extending Idris's metaprogramming facilities with primitives for describing new type-directed editing features, making Idris's editors as extensible as its elaborator.
@InProceedings{TyDe18p38,
author = {Joomy Korkut and David Thrane Christiansen},
title = {Extensible Type-Directed Editing},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {38--50},
doi = {10.1145/3240719.3241791},
year = {2018},
}
Publisher's Version
TyDe '18: "First Class Dynamic Effect ..."
First Class Dynamic Effect Handlers: or, Polymorphic Heaps with Dynamic Effect Handlers
Daan Leijen
(Microsoft Research, USA)
Algebraic effect handlers are a powerful abstraction mechanism that can express many complex control-flow mechanisms. This article extends basic algebraic effect handlers with first class dynamic effects. Dynamic effects add a lot more expressiveness but surprisingly only need minimal changes to the original semantics. As such, dynamic effects are a powerful abstraction but can still be understood and reasoned about as regular effect handlers. We illustrate the expressiveness of dynamic effects with first class event streams in CorrL and also model full polymorphic heap references without requiring any further primitives.
@InProceedings{TyDe18p51,
author = {Daan Leijen},
title = {First Class Dynamic Effect Handlers: or, Polymorphic Heaps with Dynamic Effect Handlers},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {51--64},
doi = {10.1145/3240719.3241789},
year = {2018},
}
Publisher's Version
TyDe '18: "Sums of Products for Mutually ..."
Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming
Victor Cacciari Miraldo and Alejandro Serrano
(Utrecht University, Netherlands)
Generic programming for mutually recursive families of datatypes is hard. On the other hand, most interesting abstract syntax trees are described by a mutually recursive family of datatypes. We could give up on using that mutually recursive structure, but then we lose the ability to use those generic operations which take advantage of that same structure. We present a new approach to generic programming that uses modern Haskell features to handle mutually recursive families with explicit sum-of-products structure. This additional structure allows us to remove much of the complexity previously associated with generic programming over these types.
@InProceedings{TyDe18p65,
author = {Victor Cacciari Miraldo and Alejandro Serrano},
title = {Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {65--77},
doi = {10.1145/3240719.3241786},
year = {2018},
}
Publisher's Version
TyDe '18: "Authenticated Modular Maps ..."
Authenticated Modular Maps in Haskell
Victor Cacciari Miraldo, Harold Carr, Alex Kogan, Mark Moir, and Maurice Herlihy
(Utrecht University, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; Brown University, USA)
We present hamm, a Haskell library that enables programmers to easily configure authenticated map (key-value store) implementations. We use type level programming techniques to establish an extensible foundation, and provide an example base map and several example “add on” transformers supporting features such as caches, Bloom filters and paging structures. Another add-on enables a prover to provide—and a verifier to verify—a “summary” containing only a small subset of the map’s data, and a verifier to receive and verify additional data only if needed. Preliminary performance results demonstrate significant potential for authenticated maps configured using hamm to support our goal of enabling participants to join blockchain networks faster.
@InProceedings{TyDe18p1,
author = {Victor Cacciari Miraldo and Harold Carr and Alex Kogan and Mark Moir and Maurice Herlihy},
title = {Authenticated Modular Maps in Haskell},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3240719.3241790},
year = {2018},
}
Publisher's Version
TyDe '18: "Authenticated Modular Maps ..."
Authenticated Modular Maps in Haskell
Victor Cacciari Miraldo, Harold Carr, Alex Kogan, Mark Moir, and Maurice Herlihy
(Utrecht University, Netherlands; Oracle Labs, USA; Oracle Labs, New Zealand; Brown University, USA)
We present hamm, a Haskell library that enables programmers to easily configure authenticated map (key-value store) implementations. We use type level programming techniques to establish an extensible foundation, and provide an example base map and several example “add on” transformers supporting features such as caches, Bloom filters and paging structures. Another add-on enables a prover to provide—and a verifier to verify—a “summary” containing only a small subset of the map’s data, and a verifier to receive and verify additional data only if needed. Preliminary performance results demonstrate significant potential for authenticated maps configured using hamm to support our goal of enabling participants to join blockchain networks faster.
@InProceedings{TyDe18p1,
author = {Victor Cacciari Miraldo and Harold Carr and Alex Kogan and Mark Moir and Maurice Herlihy},
title = {Authenticated Modular Maps in Haskell},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3240719.3241790},
year = {2018},
}
Publisher's Version
TyDe '18: "Implementing Resource-Aware ..."
Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL
Ilya Yanok and Nathaniel Nystrom
(USI Lugano, Switzerland)
We present construction of resource-aware safe typed assembly language as an EDSL in dependently-typed Idris language. We use this assembly language to compile Linux kernel probes — small pieces of instrumentation code injected directly into the kernel and thus having to satisfy strict safety properties. We believe that the techniques presented can be generally applied to embedding a typed assembly language into a functional language with dependent types.
@InProceedings{TyDe18p25,
author = {Ilya Yanok and Nathaniel Nystrom},
title = {Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {25--37},
doi = {10.1145/3240719.3241792},
year = {2018},
}
Publisher's Version
TyDe '18: "Typing, Representing, and ..."
Typing, Representing, and Abstracting Control: Functional Pearl
Philipp Schuster and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany)
A well known technique to implement programming languages with delimited control operators shift and reset is to translate programs into continuation passing style (CPS). We can iterate the CPS translation to obtain the CPS hierarchy and to implement a family of control operators shifti and reseti. This functional pearl retells the story of a family of delimited control operators and their translation to lambda calculus via the CPS hierarchy. Prior work on the CPS hierarchy fixes a level of n control operators for the entire program upfront, but we allow different parts of the program to live at different levels. It turns out that taking shift0 rather than shift as the basis for the family of control operators is essential for this. Our source language is a typed embedding in the dependently typed language Idris. Our target language is a HOAS embedding in Idris. The translation avoids administrative beta- and eta-redexes at all levels of the CPS hierarchy, by iterating well-known techniques for the non-iterated CPS translation.
@InProceedings{TyDe18p14,
author = {Philipp Schuster and Jonathan Immanuel Brachthäuser},
title = {Typing, Representing, and Abstracting Control: Functional Pearl},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {14--24},
doi = {10.1145/3240719.3241788},
year = {2018},
}
Publisher's Version
TyDe '18: "Sums of Products for Mutually ..."
Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming
Victor Cacciari Miraldo and Alejandro Serrano
(Utrecht University, Netherlands)
Generic programming for mutually recursive families of datatypes is hard. On the other hand, most interesting abstract syntax trees are described by a mutually recursive family of datatypes. We could give up on using that mutually recursive structure, but then we lose the ability to use those generic operations which take advantage of that same structure. We present a new approach to generic programming that uses modern Haskell features to handle mutually recursive families with explicit sum-of-products structure. This additional structure allows us to remove much of the complexity previously associated with generic programming over these types.
@InProceedings{TyDe18p65,
author = {Victor Cacciari Miraldo and Alejandro Serrano},
title = {Sums of Products for Mutually Recursive Datatypes: The Appropriationist’s View on Generic Programming},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {65--77},
doi = {10.1145/3240719.3241786},
year = {2018},
}
Publisher's Version
TyDe '18: "From Algebra to Abstract Machine: ..."
From Algebra to Abstract Machine: A Verified Generic Construction
Carlos Tomé Cortiñas and Wouter Swierstra
(Utrecht University, Netherlands)
Many functions over algebraic datatypes can be expressed in terms of a fold. Doing so, however, has one notable drawback: folds are not tail-recursive. As a result, a function defined in terms of a fold may raise a stack overflow when executed. This paper defines a datatype generic, tail-recursive higher-order function that is guaranteed to produce the same result as the fold. Doing so combines the compositional nature of folds and the performance benefits of a hand-written tail-recursive function in a single setting.
@InProceedings{TyDe18p78,
author = {Carlos Tomé Cortiñas and Wouter Swierstra},
title = {From Algebra to Abstract Machine: A Verified Generic Construction},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {78--90},
doi = {10.1145/3240719.3241787},
year = {2018},
}
Publisher's Version
TyDe '18: "From Algebra to Abstract Machine: ..."
From Algebra to Abstract Machine: A Verified Generic Construction
Carlos Tomé Cortiñas and Wouter Swierstra
(Utrecht University, Netherlands)
Many functions over algebraic datatypes can be expressed in terms of a fold. Doing so, however, has one notable drawback: folds are not tail-recursive. As a result, a function defined in terms of a fold may raise a stack overflow when executed. This paper defines a datatype generic, tail-recursive higher-order function that is guaranteed to produce the same result as the fold. Doing so combines the compositional nature of folds and the performance benefits of a hand-written tail-recursive function in a single setting.
@InProceedings{TyDe18p78,
author = {Carlos Tomé Cortiñas and Wouter Swierstra},
title = {From Algebra to Abstract Machine: A Verified Generic Construction},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {78--90},
doi = {10.1145/3240719.3241787},
year = {2018},
}
Publisher's Version
TyDe '18: "Implementing Resource-Aware ..."
Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL
Ilya Yanok and Nathaniel Nystrom
(USI Lugano, Switzerland)
We present construction of resource-aware safe typed assembly language as an EDSL in dependently-typed Idris language. We use this assembly language to compile Linux kernel probes — small pieces of instrumentation code injected directly into the kernel and thus having to satisfy strict safety properties. We believe that the techniques presented can be generally applied to embedding a typed assembly language into a functional language with dependent types.
@InProceedings{TyDe18p25,
author = {Ilya Yanok and Nathaniel Nystrom},
title = {Implementing Resource-Aware Safe Assembly for Kernel Probes as a Dependently-Typed DSL},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {25--37},
doi = {10.1145/3240719.3241792},
year = {2018},
}
Publisher's Version