Data.Witness.WitnessDict

Documentation

newtype WitnessDict w

A dictionary that is heterogenous up to its simple witness type w. Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.

Constructors

MkWitnessDict [Any w]

emptyWitnessDict :: WitnessDict w

An empty dictionary.

witnessDictLookup :: TestEquality w => w a -> WitnessDict w -> Maybe a

Look up the first value in the dictionary that matches the given witness.

witnessDictModify :: TestEquality w => w a -> (a -> a) -> WitnessDict w -> WitnessDict w

Modify the first value in the dictionary that matches a particular witness.

witnessDictReplace :: TestEquality w => w a -> a -> WitnessDict w -> WitnessDict w

Replace the first value in the dictionary that matches the witness

witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w

Add a witness and value as the first entry in the dictionary.

witnessDictRemove :: TestEquality w => w a -> WitnessDict w -> WitnessDict w

Remove the first entry in the dictionary that matches the given witness.

witnessDictFromList :: [Any w] -> WitnessDict w

Create a dictionary from a list of witness/value pairs