No-go theorems for distributive laws
Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some principles for constructing distributive laws. However, until now there have been n...
Main Authors: | , |
---|---|
Format: | Conference item |
Published: |
IEEE
2019
|
_version_ | 1826276897137360896 |
---|---|
author | Zwart, M Marsden, D |
author_facet | Zwart, M Marsden, D |
author_sort | Zwart, M |
collection | OXFORD |
description | Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some principles for constructing distributive laws. However, until now there have been no general techniques for establishing when no such law exists. We present two families of theorems for showing when there can be no distributive law for two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second family is entirely novel, encompassing various new practical situations. For example, it negatively resolves the open question of whether the list monad distributes over itself, and also reveals a previously unobserved error in the literature. |
first_indexed | 2024-03-06T23:20:45Z |
format | Conference item |
id | oxford-uuid:68a5d72f-7c72-4357-a409-edad6d1d4e33 |
institution | University of Oxford |
last_indexed | 2024-03-06T23:20:45Z |
publishDate | 2019 |
publisher | IEEE |
record_format | dspace |
spelling | oxford-uuid:68a5d72f-7c72-4357-a409-edad6d1d4e332022-03-26T18:46:13ZNo-go theorems for distributive lawsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:68a5d72f-7c72-4357-a409-edad6d1d4e33Symplectic Elements at OxfordIEEE2019Zwart, MMarsden, D Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some principles for constructing distributive laws. However, until now there have been no general techniques for establishing when no such law exists. We present two families of theorems for showing when there can be no distributive law for two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second family is entirely novel, encompassing various new practical situations. For example, it negatively resolves the open question of whether the list monad distributes over itself, and also reveals a previously unobserved error in the literature. |
spellingShingle | Zwart, M Marsden, D No-go theorems for distributive laws |
title | No-go theorems for distributive laws |
title_full | No-go theorems for distributive laws |
title_fullStr | No-go theorems for distributive laws |
title_full_unstemmed | No-go theorems for distributive laws |
title_short | No-go theorems for distributive laws |
title_sort | no go theorems for distributive laws |
work_keys_str_mv | AT zwartm nogotheoremsfordistributivelaws AT marsdend nogotheoremsfordistributivelaws |