# type-level-sets: Type-level sets and finite maps (with value-level counterparts)

This package provides type-level sets (no duplicates, sorted to provide a normal form) via `Set`

and type-level
finite maps via `Map`

, with value-level counterparts.

Described in the paper "Embedding effect systems in Haskell" by Dominic Orchard and Tomas Petricek http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation.

Here is a brief example for finite maps:

import Data.Type.Map -- Specify how to combine duplicate key-value pairs for Int values type instance Combine Int Int = Int instance Combinable Int Int where combine x y = x + y foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int] foo = Ext (Var :: (Var "x")) 2 $ Ext (Var :: (Var "z")) True $ Ext (Var :: (Var "w")) 5 $ Empty bar :: Map '["y" :-> Int, "w" :-> Int] bar = Ext (Var :: (Var "y")) 3 $ Ext (Var :: (Var "w")) 1 $ Empty -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool] foobar = foo `union` bar

The `Map`

type for `foobar`

here shows the normalised form (sorted with no duplicates).
The type signatures is commented out as it can be infered. Running the example we get:

>>> foobar {w :-> 6, x :-> 2, y :-> 3, z :-> True}

Thus, we see that the values for "w" are added together. For sets, here is an example:

import GHC.TypeLits import Data.Type.Set type instance Cmp (Natural n) (Natural m) = CmpNat n m data Natural (a :: Nat) where Z :: Natural 0 S :: Natural n -> Natural (n + 1) -- foo :: Set '[Natural 0, Natural 1, Natural 3] foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty)) -- bar :: Set '[Natural 1, Natural 2] bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty)) -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3] foobar = foo `union` bar

Note the types here are all inferred.

Versions [faq] | 0.5, 0.6, 0.6.1, 0.7, 0.8.0.0, 0.8.5.0, 0.8.6.0, 0.8.7.0, 0.8.9.0 |
---|---|

Dependencies | base (<5), ghc-prim [details] |

License | BSD-3-Clause |

Copyright | 2013-18 University of Kent |

Author | Dominic Orchard |

Maintainer | Dominic Orchard |

Revised | Revision 1 made by GeorgeWilson at Thu Dec 20 05:40:13 UTC 2018 |

Category | Type System, Data Structures |

Source repo | head: git clone https://github.com/dorchard/type-level-sets |

Uploaded | by DominicOrchard at Thu Nov 29 11:44:02 UTC 2018 |

Distributions | NixOS:0.8.9.0 |

Downloads | 3712 total (136 in the last 30 days) |

Rating | 2.0 (votes: 1) [estimated by rule of succession] |

Your Rating | |

Status | Docs available [build log] Last success reported on 2018-11-29 [all 1 reports] |

## Downloads

- type-level-sets-0.8.9.0.tar.gz [browse] (Cabal source package)
- Package description (revised from the package)

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.