dependent-map: Dependent finite maps (partial dependent products)

[ data, dependent-types, library ] [ Propose Tags ]

Provides a type called DMap which generalizes Data.Map.Map, allowing keys to specify the type of value that can be associated with them.

[Skip to Readme]
Versions [faq] 0.1, 0.1.1,,,,,,,,, 0.3
Change log
Dependencies base (>=3 && <5), constraints-extras (>= && <0.4), containers (==0.6.*), dependent-sum (>=0.6.1 && <0.7) [details]
License LicenseRef-OtherLicense
Author James Cook <>
Maintainer James Cook <>
Category Data, Dependent Types
Home page
Source repo head: git clone git://
Uploaded by abrar at Sun Aug 4 23:15:57 UTC 2019
Distributions Debian:, LTSHaskell:, NixOS:0.3, Stackage:
Downloads 11062 total (489 in the last 30 days)
Rating 2.25 (votes: 2) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs uploaded by user
Build status unknown [no reports yet]


[Index] [Quick Jump]


Maintainer's Corner

For package maintainers and hackage trustees

Readme for dependent-map-0.3

[back to package description]

dependent-map Build Status

This library defines a dependently-typed finite map type. It is derived from Data.Map.Map in the containers package, but rather than (conceptually) storing pairs indexed by the first component, it stores DSums (from the dependent-sum package) indexed by tag. For example (using the types from the dependent-sum package's FooGADT example):

import FooGADT
import Data.Dependent.Map

x = fromList [Foo :=> pi, Baz :=> "hello there"]
y = singleton Bar 42
z = union y (read "fromList [Foo :=> (-1.1415926535897931)]")

addFoo :: Foo v -> v -> v -> v
addFoo Foo x y = x + y
addFoo _   x _ = x

main = mapM_ print
    [ x, y, z
    , unionWithKey addFoo x z

Which prints:

fromList [Foo :=> 3.141592653589793,Baz :=> "hello there"]
fromList [Bar :=> 42]
fromList [Foo :=> -1.1415926535897931,Bar :=> 42]
fromList [Foo :=> 2.0,Bar :=> 42,Baz :=> "hello there"]

This library can be found on Hackage: