Data.Witness.WitnessFDict

Documentation

newtype WitnessFDict w f

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

MkWitnessFDict [AnyF w f]

emptyWitnessFDict :: WitnessFDict w f

An empty dictionary.

witnessFDictLookup :: TestEquality w => w a -> WitnessFDict w f -> Maybe (f a)

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

witnessFDictModify :: TestEquality w => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f

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

witnessFDictReplace :: TestEquality w => w a -> f a -> WitnessFDict w f -> WitnessFDict w f

Replace the first value in the dictionary that matches the witness

witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f

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

witnessFDictRemove :: TestEquality w => w a -> WitnessFDict w f -> WitnessFDict w f

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

witnessFDictFromList :: [AnyF w f] -> WitnessFDict w f

Create a dictionary from a list of witness/value pairs