Scientific Writing

We present an approach for automatic function inversion in Haskell. The inverse functions we generate are based on an extension of Haskell’s computational model with non-determinism and free variables. We implement this functional logic extension of Haskell via a monadic lifting of functions and type declarations. Using inverse functions, we additionally show how Haskell’s pattern matching can be augmented with support for functional patterns, which enable arbitrarily deep pattern matching in data structures. Finally, we provide a plugin for the Glasgow Haskell Compiler to seamlessly integrate inverses and functional patterns into the language, covering almost all of the Haskell2010 language standard.

@inproceedings{10.1145/3471874.3472982,
author = {Teegen, Finn and Prott, Kai-Oliver and Bunkenburg, Niels},
title = {Haskell⁻¹: Automatic Function Inversion in Haskell},
year = {2021},
isbn = {9781450386159},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3471874.3472982},
doi = {10.1145/3471874.3472982},
abstract = {We present an approach for automatic function inversion in Haskell. The inverse functions we generate are based on an extension of Haskell's computational model with non-determinism and free variables. We implement this functional logic extension of Haskell via a monadic lifting of functions and type declarations. Using inverse functions, we additionally show how Haskell's pattern matching can be augmented with support for functional patterns, which enable arbitrarily deep pattern matching in data structures. Finally, we provide a plugin for the Glasgow Haskell Compiler to seamlessly integrate inverses and functional patterns into the language, covering almost all of the Haskell2010 language standard.},
booktitle = {Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell},
pages = {41–55},
numpages = {15},
keywords = {inversion, pattern matching, Haskell, partial inversion, GHC plugin, monadic transformation},
location = {Virtual, Republic of Korea},
series = {Haskell 2021}
}

We show how various Haskell language features that are related to implicit effects can be modeled in Coq. For this purpose we build on previous work that demonstrates how to reason about existing Haskell programs by translating them into monadic Coq programs. A model of Haskell programs in Coq that is polymorphic over an arbitrary monad results in non-strictly positive types when transforming recursive data types likes lists. Such non-strictly positive types are not accepted by Coq’s termination checker. Therefore, instead of a model that is generic over any monad, the approach we build on uses a concrete monad instance, namely the free monad in combination with containers, to model various kinds of effects. This model allows effect-generic proofs.

In this paper we consider ambient effects that may occur in Haskell, namely partiality, errors, and tracing, in detail. We observe that, while proving propositions that hold for all kinds of effects is attractive, not all propositions of interest hold for all kinds of effects. Some propositions fail for certain effects because the usual monadic translation models call-by-name and not call-by-need. Since modeling the evaluation semantics of call-by-need in the presence of effects like partiality is complex and not necessary to prove propositions for a variety of effects, we identify a specific class of effects for which we cannot distinguish between call-by-name and call-by-need denotationally. Using this class of effects we can prove propositions for all effects that do not require a model of call-by-need.

@inproceedings{Christiansen:2019:VEH:3331545.3342592,
 author = {Christiansen, Jan and Dylus, Sandra and Bunkenburg, Niels},
 title = {Verifying Effectful Haskell Programs in Coq},
 booktitle = {Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell},
 series = {Haskell 2019},
 year = {2019},
 isbn = {978-1-4503-6813-1},
 location = {Berlin, Germany},
 pages = {125--138},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/3331545.3342592},
 doi = {10.1145/3331545.3342592},
 acmid = {3342592},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Coq, Haskell, free monad, monads, verification},
}

Curry is a functional logic programming language that features non-strict non-determinism based on Haskell-like syntax. These properties make Curry an interesting object of software verification.

The approach of formalizing Haskell programs in a proof assistant like Coq, as described by Dylus et al., cannot be applied directly to Curry due to the interaction of non-determinism with sharing. These so-called call-time choice semantics therefore necessitate explicit modeling of sharing as effect.

In this thesis, Curry’s call-time choice semantics are modeled using a combination of the free monad and effect handlers as presented by Wu et al.. We explore different aspects of explicit sharing and multiple approaches for modeling scoped effects. Finally, we prove some properties – similar to the laws of sharing introduced by Fischer et al. – of the model in Coq.

@MastersThesis{bunkenburg2019modeling,
  author  = {Niels Bunkenburg},
  title   = {Modeling Call-Time Choice as Effect using Scoped Free Monads},
  school  = {Kiel University},
  address = {Germany},
  year    = {2019},
}

In a nutshell, Curry is a functional logic programming language based on Haskell. This means that – in addition to Haskell’s functional language aspects – Curry inherits non-determinism and free variables from logic languages like Prolog.

Curry’s static type system can be represented by means of inference systems. In my thesis, I have explored two different representations of Curry programs and how the corrsponding type systems can be formalized in Coq.

@MastersThesis{bunkenburg2019modeling,
  author  = {Niels Bunkenburg},
  title   = {Formalizing inference systems in Coq by means of type systems for Curry},
  school  = {Kiel University},
  address = {Germany},
  year    = {2016},
}