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

[ bsd3, data-structures, library, type-system ] [ Propose Tags ]

This package provides type-level sets (no duplicates, sorted to provide a normal form) via Set and type-level 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)

Here is a brief example:

import Data.Type.Map

foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
foo = Ext ((Var :: (Var "x")) :-> 2) $
        Ext ((Var :: (Var "z")) :-> 4) $
          Ext ((Var :: (Var "w")) :-> 5) $
            Empty

bar :: Set '["y" :-> Int, "w" :-> Int]
bar = Ext ((Var :: (Var "y")) :-> 3) $
        Ext ((Var :: (Var "w")) :-> 1) $
          Empty

-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
foobar = foo `union` bar

The Set 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
[(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]

Thus, we see that the first value paired with the "w" variable is dropped.

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 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 (>=4.7.0.0 && <5), ghc-prim [details]
License BSD-3-Clause
Copyright 2013-14 University of Cambridge
Author Dominic Orchard
Maintainer Dominic Orchard
Category Type System, Data Structures
Source repo head: git clone https://github.com/dorchard/type-level-sets
Uploaded by DominicOrchard at 2016-01-05T17:29:48Z
Distributions
Reverse Dependencies 5 direct, 0 indirect [details]
Downloads 6768 total (36 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2016-11-28 [all 1 reports]