Haskell '20: "Composing Effects into Tasks ..."
Composing Effects into Tasks and Workflows
Yves Parès, Jean-Philippe Bernardy, and Richard A. Eisenberg
(Tweag I/O, France; University of Gothenburg, Sweden; Bryn Mawr College, USA)
Data science applications tend to be built by composing tasks: discrete manipulations of data. These tasks are arranged in directed acyclic graphs, and many frameworks exist within the data science community supporting such a structure, which is called a workflow. In realistic applications, we want to be able to both analyze a workflow in the absence of data, and to execute the workflow with data.
This paper combines effect handlers with arrow-like structures to abstract out data science tasks. This combination of techniques enables a modular design of workflows. Additionally, these workflows can both be analyzed prior to running (e.g., to provide early failure) and run conveniently. Our work is directly motivated by real-world scenarios, and we believe that our approach is applicable to new data science and machine learning applications and frameworks.
@InProceedings{Haskell20p80,
author = {Yves Parès and Jean-Philippe Bernardy and Richard A. Eisenberg},
title = {Composing Effects into Tasks and Workflows},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {80--94},
doi = {10.1145/3406088.3409023},
year = {2020},
}
Publisher's Version
Haskell '20: "Towards Secure IoT Programming ..."
Towards Secure IoT Programming in Haskell
Nachiappan Valliappan, Robert Krook, Alejandro Russo, and Koen Claessen
(Chalmers University of Technology, Sweden)
IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language in Haskell (eDSL) for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C’s pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern-matching in Haskell to write Haski programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on Zephyr OS.
@InProceedings{Haskell20p136,
author = {Nachiappan Valliappan and Robert Krook and Alejandro Russo and Koen Claessen},
title = {Towards Secure IoT Programming in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {136--150},
doi = {10.1145/3406088.3409027},
year = {2020},
}
Publisher's Version
Haskell '20: "Finger Trees Explained Anew, ..."
Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)
Koen Claessen
(Chalmers University of Technology, Sweden)
We explicitly motivate the subtle intricacies of Hinze and Paterson's Finger Tree datastructure, by step-wise refining a naive implementation. The result is a new explanation of how Finger Trees work and why they have the particular structure they have, and also a small simplification of the original implementation.
@InProceedings{Haskell20p31,
author = {Koen Claessen},
title = {Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {31--38},
doi = {10.1145/3406088.3409026},
year = {2020},
}
Publisher's Version
Haskell '20: "Describing Microservices using ..."
Describing Microservices using Modern Haskell (Experience Report)
Alejandro Serrano and Flavio Corpa
(47 Degrees, Spain)
We present Mu, a domain specific language to describe and develop microservices in Haskell. At its core, Mu provides a type level representation of schemas, which we leverage in various ways. These schemas can be automatically imported from industry-standard interface definition languages.
Mu uses many of the type level extensions to GHC, and techniques such as (data type) generic programming and attribute grammars. Apart from the description of the library, we discuss a series of shortcomings in current GHC/Haskell, mostly related to the friendliness of the exposed library interface once complex types enter the scene.
@InProceedings{Haskell20p1,
author = {Alejandro Serrano and Flavio Corpa},
title = {Describing Microservices using Modern Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {1--8},
doi = {10.1145/3406088.3409018},
year = {2020},
}
Publisher's Version
Haskell '20: "Stitch: The Sound Type-Indexed ..."
Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
Richard A. Eisenberg
(Tweag I/O, France; Bryn Mawr College, USA)
A classic example of the power of generalized algebraic datatypes (GADTs) to verify a delicate implementation is the type-indexed expression AST. This functional pearl refreshes this example, casting it in modern Haskell using many of GHC's bells and whistles. The Stitch interpreter is a full executable interpreter, with a parser, type checker, common-subexpression elimination, and a REPL. Making heavy use of GADTs and type indices, the Stitch implementation is clean Haskell code and serves as an existence proof that Haskell's type system is advanced enough for the use of fancy types in a practical setting. The paper focuses on guiding the reader through these advanced topics, enabling them to adopt the techniques demonstrated here.
@InProceedings{Haskell20p39,
author = {Richard A. Eisenberg},
title = {Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {39--53},
doi = {10.1145/3406088.3409015},
year = {2020},
}
Publisher's Version
Haskell '20: "Composing Effects into Tasks ..."
Composing Effects into Tasks and Workflows
Yves Parès, Jean-Philippe Bernardy, and Richard A. Eisenberg
(Tweag I/O, France; University of Gothenburg, Sweden; Bryn Mawr College, USA)
Data science applications tend to be built by composing tasks: discrete manipulations of data. These tasks are arranged in directed acyclic graphs, and many frameworks exist within the data science community supporting such a structure, which is called a workflow. In realistic applications, we want to be able to both analyze a workflow in the absence of data, and to execute the workflow with data.
This paper combines effect handlers with arrow-like structures to abstract out data science tasks. This combination of techniques enables a modular design of workflows. Additionally, these workflows can both be analyzed prior to running (e.g., to provide early failure) and run conveniently. Our work is directly motivated by real-world scenarios, and we believe that our approach is applicable to new data science and machine learning applications and frameworks.
@InProceedings{Haskell20p80,
author = {Yves Parès and Jean-Philippe Bernardy and Richard A. Eisenberg},
title = {Composing Effects into Tasks and Workflows},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {80--94},
doi = {10.1145/3406088.3409023},
year = {2020},
}
Publisher's Version
Haskell '20: "Assessing the Quality of Evolving ..."
Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality
Sander Kamps, Bastiaan Heeren, and Johan Jeuring
(Open University of the Netherlands, Netherlands)
Software metrics are used to measure the quality of a software system, and to understand the evolution of the system's quality over time. In this paper we report on an empirical study that investigates whether structural degradation in Haskell systems is related to decreasing software quality. For our study we use three metrics that measure internal attributes at the level of Haskell modules: intra-modular complexity (cohesion), inter-modular complexity (coupling), and module size. For these metrics, we calculate the Gini coefficient, which is a measure of the inequality in a distribution of values within a certain population, and the deviation of the population's central tendency from an empirically established ideal value. We develop a method to track the evolution, and measure the correlation between the calculated system-level information and post-release defects.
The results show that: (1) post-release defects are significantly correlated with the degree of inequality between the size of modules, (2) the inequality measure is able to indicate significant structural shifts in Haskell source code, and (3) the deviation of a population's central tendency from an ideal value can serve as a benchmark to evaluate the structural characteristics of a Haskell system. The results, however, do not show that a combined measure for inequality and ideal value deviation increases the ability to indicate the defect proneness of Haskell source code.
@InProceedings{Haskell20p67,
author = {Sander Kamps and Bastiaan Heeren and Johan Jeuring},
title = {Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {67--79},
doi = {10.1145/3406088.3409014},
year = {2020},
}
Publisher's Version
Haskell '20: "A Graded Monad for Deadlock-Free ..."
A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)
Andrej Ivašković and Alan Mycroft
(University of Cambridge, UK)
We present a new type-oriented framework for writing shared memory multithreaded programs that the Haskell type system guarantees are deadlock-free. The implementation wraps all concurrent computation inside a graded monad and assumes a total order is defined between locks. The grades within the type of such a computation specify which locks it acquires and releases. This information is drawn from an algebra that ensures that types can, in principle, be inferred in polynomial time.
@InProceedings{Haskell20p17,
author = {Andrej Ivašković and Alan Mycroft},
title = {A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {17--30},
doi = {10.1145/3406088.3409024},
year = {2020},
}
Publisher's Version
Haskell '20: "Assessing the Quality of Evolving ..."
Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality
Sander Kamps, Bastiaan Heeren, and Johan Jeuring
(Open University of the Netherlands, Netherlands)
Software metrics are used to measure the quality of a software system, and to understand the evolution of the system's quality over time. In this paper we report on an empirical study that investigates whether structural degradation in Haskell systems is related to decreasing software quality. For our study we use three metrics that measure internal attributes at the level of Haskell modules: intra-modular complexity (cohesion), inter-modular complexity (coupling), and module size. For these metrics, we calculate the Gini coefficient, which is a measure of the inequality in a distribution of values within a certain population, and the deviation of the population's central tendency from an empirically established ideal value. We develop a method to track the evolution, and measure the correlation between the calculated system-level information and post-release defects.
The results show that: (1) post-release defects are significantly correlated with the degree of inequality between the size of modules, (2) the inequality measure is able to indicate significant structural shifts in Haskell source code, and (3) the deviation of a population's central tendency from an ideal value can serve as a benchmark to evaluate the structural characteristics of a Haskell system. The results, however, do not show that a combined measure for inequality and ideal value deviation increases the ability to indicate the defect proneness of Haskell source code.
@InProceedings{Haskell20p67,
author = {Sander Kamps and Bastiaan Heeren and Johan Jeuring},
title = {Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {67--79},
doi = {10.1145/3406088.3409014},
year = {2020},
}
Publisher's Version
Haskell '20: "Assessing the Quality of Evolving ..."
Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality
Sander Kamps, Bastiaan Heeren, and Johan Jeuring
(Open University of the Netherlands, Netherlands)
Software metrics are used to measure the quality of a software system, and to understand the evolution of the system's quality over time. In this paper we report on an empirical study that investigates whether structural degradation in Haskell systems is related to decreasing software quality. For our study we use three metrics that measure internal attributes at the level of Haskell modules: intra-modular complexity (cohesion), inter-modular complexity (coupling), and module size. For these metrics, we calculate the Gini coefficient, which is a measure of the inequality in a distribution of values within a certain population, and the deviation of the population's central tendency from an empirically established ideal value. We develop a method to track the evolution, and measure the correlation between the calculated system-level information and post-release defects.
The results show that: (1) post-release defects are significantly correlated with the degree of inequality between the size of modules, (2) the inequality measure is able to indicate significant structural shifts in Haskell source code, and (3) the deviation of a population's central tendency from an ideal value can serve as a benchmark to evaluate the structural characteristics of a Haskell system. The results, however, do not show that a combined measure for inequality and ideal value deviation increases the ability to indicate the defect proneness of Haskell source code.
@InProceedings{Haskell20p67,
author = {Sander Kamps and Bastiaan Heeren and Johan Jeuring},
title = {Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {67--79},
doi = {10.1145/3406088.3409014},
year = {2020},
}
Publisher's Version
Haskell '20: "Towards Secure IoT Programming ..."
Towards Secure IoT Programming in Haskell
Nachiappan Valliappan, Robert Krook, Alejandro Russo, and Koen Claessen
(Chalmers University of Technology, Sweden)
IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language in Haskell (eDSL) for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C’s pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern-matching in Haskell to write Haski programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on Zephyr OS.
@InProceedings{Haskell20p136,
author = {Nachiappan Valliappan and Robert Krook and Alejandro Russo and Koen Claessen},
title = {Towards Secure IoT Programming in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {136--150},
doi = {10.1145/3406088.3409027},
year = {2020},
}
Publisher's Version
Haskell '20: "Effect Handlers in Haskell, ..."
Effect Handlers in Haskell, Evidently
Ningning Xie and Daan Leijen
(Microsoft Research, USA)
Algebraic effect handlers offer an alternative to monads to incorporate effects in Haskell. In recent work Xie _et al._ show how to give semantics to effect handlers in terms of plain polymorphic lambda calculus through _evidence translation_. Besides giving precise semantics, this translation also allows for potentially more efficient implementations. Here we present the first implementation of this technique as a library for effect handlers in Haskell. We show how the design naturally leads to a concise effect interface and how evidence translation enables evaluating _tail resumptive_ operations _in-place_. We give detailed benchmark results where our library performs well with respect to other approaches.
@InProceedings{Haskell20p95,
author = {Ningning Xie and Daan Leijen},
title = {Effect Handlers in Haskell, Evidently},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {95--108},
doi = {10.1145/3406088.3409022},
year = {2020},
}
Publisher's Version
Haskell '20: "Staged Sums of Products ..."
Staged Sums of Products
Matthew Pickering, Andres Löh, and Nicolas Wu
(University of Bristol, UK; Well-Typed LLP, UK; Imperial College London, UK)
Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.
@InProceedings{Haskell20p122,
author = {Matthew Pickering and Andres Löh and Nicolas Wu},
title = {Staged Sums of Products},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {122--135},
doi = {10.1145/3406088.3409021},
year = {2020},
}
Publisher's Version
Haskell '20: "A Graded Monad for Deadlock-Free ..."
A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)
Andrej Ivašković and Alan Mycroft
(University of Cambridge, UK)
We present a new type-oriented framework for writing shared memory multithreaded programs that the Haskell type system guarantees are deadlock-free. The implementation wraps all concurrent computation inside a graded monad and assumes a total order is defined between locks. The grades within the type of such a computation specify which locks it acquires and releases. This information is drawn from an algebra that ensures that types can, in principle, be inferred in polynomial time.
@InProceedings{Haskell20p17,
author = {Andrej Ivašković and Alan Mycroft},
title = {A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {17--30},
doi = {10.1145/3406088.3409024},
year = {2020},
}
Publisher's Version
Haskell '20: "Type Your Matrices for Great ..."
Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)
Armando Santos and José N. Oliveira
(University of Minho, Portugal; INESC TEC, Portugal)
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory.
@InProceedings{Haskell20p54,
author = {Armando Santos and José N. Oliveira},
title = {Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {54--66},
doi = {10.1145/3406088.3409019},
year = {2020},
}
Publisher's Version
Haskell '20: "Composing Effects into Tasks ..."
Composing Effects into Tasks and Workflows
Yves Parès, Jean-Philippe Bernardy, and Richard A. Eisenberg
(Tweag I/O, France; University of Gothenburg, Sweden; Bryn Mawr College, USA)
Data science applications tend to be built by composing tasks: discrete manipulations of data. These tasks are arranged in directed acyclic graphs, and many frameworks exist within the data science community supporting such a structure, which is called a workflow. In realistic applications, we want to be able to both analyze a workflow in the absence of data, and to execute the workflow with data.
This paper combines effect handlers with arrow-like structures to abstract out data science tasks. This combination of techniques enables a modular design of workflows. Additionally, these workflows can both be analyzed prior to running (e.g., to provide early failure) and run conveniently. Our work is directly motivated by real-world scenarios, and we believe that our approach is applicable to new data science and machine learning applications and frameworks.
@InProceedings{Haskell20p80,
author = {Yves Parès and Jean-Philippe Bernardy and Richard A. Eisenberg},
title = {Composing Effects into Tasks and Workflows},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {80--94},
doi = {10.1145/3406088.3409023},
year = {2020},
}
Publisher's Version
Haskell '20: "Staged Sums of Products ..."
Staged Sums of Products
Matthew Pickering, Andres Löh, and Nicolas Wu
(University of Bristol, UK; Well-Typed LLP, UK; Imperial College London, UK)
Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.
@InProceedings{Haskell20p122,
author = {Matthew Pickering and Andres Löh and Nicolas Wu},
title = {Staged Sums of Products},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {122--135},
doi = {10.1145/3406088.3409021},
year = {2020},
}
Publisher's Version
Haskell '20: "Towards Secure IoT Programming ..."
Towards Secure IoT Programming in Haskell
Nachiappan Valliappan, Robert Krook, Alejandro Russo, and Koen Claessen
(Chalmers University of Technology, Sweden)
IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language in Haskell (eDSL) for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C’s pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern-matching in Haskell to write Haski programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on Zephyr OS.
@InProceedings{Haskell20p136,
author = {Nachiappan Valliappan and Robert Krook and Alejandro Russo and Koen Claessen},
title = {Towards Secure IoT Programming in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {136--150},
doi = {10.1145/3406088.3409027},
year = {2020},
}
Publisher's Version
Haskell '20: "Type Your Matrices for Great ..."
Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)
Armando Santos and José N. Oliveira
(University of Minho, Portugal; INESC TEC, Portugal)
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory.
@InProceedings{Haskell20p54,
author = {Armando Santos and José N. Oliveira},
title = {Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {54--66},
doi = {10.1145/3406088.3409019},
year = {2020},
}
Publisher's Version
Haskell '20: "Describing Microservices using ..."
Describing Microservices using Modern Haskell (Experience Report)
Alejandro Serrano and Flavio Corpa
(47 Degrees, Spain)
We present Mu, a domain specific language to describe and develop microservices in Haskell. At its core, Mu provides a type level representation of schemas, which we leverage in various ways. These schemas can be automatically imported from industry-standard interface definition languages.
Mu uses many of the type level extensions to GHC, and techniques such as (data type) generic programming and attribute grammars. Apart from the description of the library, we discuss a series of shortcomings in current GHC/Haskell, mostly related to the friendliness of the exposed library interface once complex types enter the scene.
@InProceedings{Haskell20p1,
author = {Alejandro Serrano and Flavio Corpa},
title = {Describing Microservices using Modern Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {1--8},
doi = {10.1145/3406088.3409018},
year = {2020},
}
Publisher's Version
Haskell '20: "Scripted Signal Functions ..."
Scripted Signal Functions
David A. Stuart
Programming time-dependent signals like animations involves expressing both continuous and discrete changes in signal values. The method of functional reactive programming (FRP) represents this simply and effectively as discrete modes of an otherwise continuous signal. In variants of FRP based on arrows, programs are composed not of signals but rather functions on signals. Accordingly, these signal functions can switch between discrete modes of operation. However, the literature emphasizes expressions of mode switching that are unnecessarily limited. An analysis of their limitations indicates the need for two new, primitive transformations of signal functions. These transformations help to define a monad that represents signal function modes, and this allows programmers to express switching in an imperative, script-like style. This scripting interface gains flexibility and power from several novel operations, including a general-purpose mapping between modes and a combination that mixes two concurrent modes into one. We demonstrate its usefulness with several examples.
@InProceedings{Haskell20p109,
author = {David A. Stuart},
title = {Scripted Signal Functions},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {109--121},
doi = {10.1145/3406088.3409016},
year = {2020},
}
Publisher's Version
Haskell '20: "Towards Secure IoT Programming ..."
Towards Secure IoT Programming in Haskell
Nachiappan Valliappan, Robert Krook, Alejandro Russo, and Koen Claessen
(Chalmers University of Technology, Sweden)
IoT applications are often developed in programming languages with low-level abstractions, where a seemingly innocent mistake might lead to severe security vulnerabilities. Current IoT development tools make it hard to identify these vulnerabilities as they do not provide end-to-end guarantees about how data flows within and between appliances. In this work we present Haski, an embedded domain specific language in Haskell (eDSL) for secure programming of IoT devices. Haski enables developers to write Haskell programs that generate C code without falling into many of C’s pitfalls. Haski is designed after the synchronous programming language Lustre, and sports a backwards compatible information-flow control extension to restrict how sensitive data is propagated and modified within the application. We present a novel eDSL design which uses recursive monadic bindings and allows a natural use of functions and pattern-matching in Haskell to write Haski programs. To showcase Haski, we implement a simple smart house controller where communication is done via low-energy Bluetooth on Zephyr OS.
@InProceedings{Haskell20p136,
author = {Nachiappan Valliappan and Robert Krook and Alejandro Russo and Koen Claessen},
title = {Towards Secure IoT Programming in Haskell},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {136--150},
doi = {10.1145/3406088.3409027},
year = {2020},
}
Publisher's Version
Haskell '20: "Staged Sums of Products ..."
Staged Sums of Products
Matthew Pickering, Andres Löh, and Nicolas Wu
(University of Bristol, UK; Well-Typed LLP, UK; Imperial College London, UK)
Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.
@InProceedings{Haskell20p122,
author = {Matthew Pickering and Andres Löh and Nicolas Wu},
title = {Staged Sums of Products},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {122--135},
doi = {10.1145/3406088.3409021},
year = {2020},
}
Publisher's Version
Haskell '20: "Effect Handlers in Haskell, ..."
Effect Handlers in Haskell, Evidently
Ningning Xie and Daan Leijen
(Microsoft Research, USA)
Algebraic effect handlers offer an alternative to monads to incorporate effects in Haskell. In recent work Xie _et al._ show how to give semantics to effect handlers in terms of plain polymorphic lambda calculus through _evidence translation_. Besides giving precise semantics, this translation also allows for potentially more efficient implementations. Here we present the first implementation of this technique as a library for effect handlers in Haskell. We show how the design naturally leads to a concise effect interface and how evidence translation enables evaluating _tail resumptive_ operations _in-place_. We give detailed benchmark results where our library performs well with respect to other approaches.
@InProceedings{Haskell20p95,
author = {Ningning Xie and Daan Leijen},
title = {Effect Handlers in Haskell, Evidently},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {95--108},
doi = {10.1145/3406088.3409022},
year = {2020},
}
Publisher's Version
Haskell '20: "Eliminating Bugs with Dependent ..."
Eliminating Bugs with Dependent Haskell (Experience Report)
Noam Zilberstein
(Facebook, USA)
Using dependent types in production code is a practical way to eliminate errors. While there are many examples of using dependent Haskell to prove invariants about code, few of these are applied to large scale production systems. Critics claim that dependent types are only useful in toy examples and that they are impractical for use in the real world. This experience report analyzes real world examples where dependent types have enabled us to find and eliminate bugs in production Haskell code.
@InProceedings{Haskell20p9,
author = {Noam Zilberstein},
title = {Eliminating Bugs with Dependent Haskell (Experience Report)},
booktitle = {Proc.\ Haskell},
publisher = {ACM},
pages = {9--16},
doi = {10.1145/3406088.3409020},
year = {2020},
}
Publisher's Version