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 (>=4.9 && <5), constraints-extras (>= && <0.4), containers (>= && <0.7), dependent-sum (>=0.6.1 && <0.8) [details]
License LicenseRef-OtherLicense
Author James Cook <>
Maintainer Obsidian Systems, LLC <>
Category Data, Dependent Types
Home page
Source repo head: git clone
Uploaded by 3noch at 2020-03-27T02:06:15Z
Distributions Debian:, LTSHaskell:, NixOS:, Stackage:
Downloads 14840 total (320 in the last 30 days)
Rating 2.5 (votes: 3) [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-

[back to package description]

dependent-map Build Status Hackage

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

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module Example where

import Data.Constraint.Extras.TH (deriveArgDict)
import Data.Dependent.Map (DMap, fromList, singleton, union, unionWithKey)
import Data.Dependent.Sum ((==>))
import Data.Functor.Identity (Identity(..))
import Data.GADT.Compare.TH (deriveGCompare, deriveGEq)
import Data.GADT.Show.TH (deriveGShow)

data Tag a where
  StringKey :: Tag String
  IntKey    :: Tag Int
  DoubleKey :: Tag Double
deriveGEq ''Tag
deriveGCompare ''Tag
deriveGShow ''Tag
deriveArgDict ''Tag

x :: DMap Tag Identity
x = fromList [DoubleKey ==> pi, StringKey ==> "hello there"]

y :: DMap Tag Identity
y = singleton IntKey (Identity 42)

z :: DMap Tag Identity
z = y `union` fromList [DoubleKey ==> -1.1415926535897931]

addFoo :: Tag v -> Identity v -> Identity v -> Identity v
addFoo IntKey (Identity x) (Identity y) = Identity $ x + y
addFoo DoubleKey (Identity x) (Identity y) = Identity $ x + y
addFoo _ x _ = x

main :: IO ()
main = mapM_ print
  [ x, y, z
  , unionWithKey addFoo x z