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]

Downloads

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'.

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1, 0.1.1, 0.1.1.1, 0.1.1.2, 0.1.1.3, 0.2.0.1, 0.2.1.0, 0.2.2.0, 0.2.3.0, 0.2.4.0, 0.3, 0.3.1.0, 0.4.0.0
Change log ChangeLog.md
Dependencies base (>=4.9 && <5), constraints-extras (>=0.2.3.0 && <0.5), containers (>=0.5.7.1 && <0.8), dependent-sum (>=0.6.1 && <0.8) [details]
License LicenseRef-OtherLicense
Author James Cook <mokus@deepbondi.net>
Maintainer Obsidian Systems, LLC <maintainer@obsidian.systems>
Revised Revision 2 made by abrar at 2024-05-27T23:58:43Z
Category Data, Dependent Types
Home page https://github.com/obsidiansystems/dependent-map
Source repo head: git clone https://github.com/obsidiansystems/dependent-map
Uploaded by 3noch at 2020-03-27T02:06:15Z
Distributions Arch:0.4.0.0, Debian:0.4.0.0, LTSHaskell:0.4.0.0, NixOS:0.4.0.0, Stackage:0.4.0.0
Reverse Dependencies 39 direct, 130 indirect [details]
Downloads 29305 total (155 in the last 30 days)
Rating 2.5 (votes: 4) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for dependent-map-0.4.0.0

[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 GADTs #-}
{-# 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
  ]