A Map type where the value type is dependent on the key type?

Question

I wonder if it is possible to implement something like contrib's Data.SortedMapwhere, as an example, the key type could be Key n and the value type be Value n where n is the same Nat?

For a Map (Key n) (Value n) (which fails with "No such variable n") some usual functions would then have types like these

Key    : Nat -> Type
Value  : Nat -> Type
lookup : {n : Nat} -> Key n -> WonderMap Key Value -> Maybe (Value n)
insert : {n : Nat} -> Key n -> Value n -> WonderMap Key Value -> WonderMap Key Value

I tried the following using dependent pairs

MyMap : Type
MyMap = SortedMap (n ** Key n) (n **Value n)

but I think the ns here are not the same one so it is interpreted like

MyMap = SortedMap (n ** Key n) (x ** Value x)

in other words, the Key and Value types are not "connected" in the way I would like, i.e. a Value n can only be stored underKey n and lookup for a Key n always returns a Value n.

And

MyOtherMap : Nat -> Type
MyOtherMap n = SortedMap (Key n) (Value n)

should create a map type indexed by n : Nat so I could not store Value 1 values under Key 1 keys and Value 7 values under Key 7 keys in the same map.

Is it possible to implement the map type I want where a family of key types are used to store a corresponding family of value types? (Other than having one MyOtherMap for each n : Nat and then have all those bundled up in a larger structure, see my answer)

Higemaru Higemaru · Accepted Answer · 2020-01-12T17:58:16

This answer isn't really a solution to my problem, it is more just a way to show what I want to achieve (and it is not even the most general case). So please do not dismiss my question as already answered. ;-) Thank you!

I thought I'd try to implement the naive approach. This can't be the easiest way.

import Data.SortedMap

-- pretty much a Vector
data Key : Type -> Nat -> Type where
  KNil  : Key a 0
  KCons : a -> Key a n -> Key a (S n)

Eq a => Eq (Key a n) where
  KNil == KNil = True
  (KCons x xs) == (KCons y ys) = x == y && xs == ys

Ord a => Ord (Key a n) where
  compare KNil KNil = EQ
  compare (KCons x xs) (KCons y ys) = case compare x y of
                                        EQ => compare xs ys
                                        x  => x

-- same as Key
data Value : Type -> Nat -> Type where
  VNil  : Value a 0
  VCons : a -> Value a n -> Value a (S n)

-- Map for keys and values of a fixed length
NatIndexedMap : (Nat -> Type) -> (Nat -> Type) -> Nat -> Type
NatIndexedMap k v n = SortedMap (k n) (v n)

nim2 : NatIndexedMap (Key Nat) (Value String) 2
nim2 = SortedMap.fromList [(KCons 0 (KCons 0 KNil), VCons "a" (VCons "a" VNil))]

nim3 : NatIndexedMap (Key Nat) (Value String) 3
nim3 = SortedMap.fromList [(KCons 0 (KCons 0 (KCons 0 KNil)), VCons "a" (VCons "a" (VCons "a" VNil)))]

-- List of maps with keys and values which increase in length
data WonderMap : (Nat -> Type) -> (Nat -> Type) -> Nat -> Type where
  WonderMapNil : {k : Nat -> Type} -> {v : Nat -> Type} -> WonderMap k v 0
  WonderMapCons : {n : Nat} -> {k : Nat -> Type} -> {v : Nat -> Type}
    -> NatIndexedMap k v (S n) -> WonderMap k v n -> WonderMap k v (S n)

wm : WonderMap (Key Nat) (Value String) 3
wm = WonderMapCons nim3 (WonderMapCons nim2 (WonderMapCons SortedMap.empty WonderMapNil))

-- will return Nothing if Key n > Map n
lookup : {n : Nat} -> {m : Nat} -> {k : Nat -> Type} -> {v : Nat -> Type} -> k n -> WonderMap k v m -> Maybe (v n)
lookup {n = Z} _ WonderMapNil = Nothing
lookup {m = Z} _ _ = Nothing
lookup {n = S n'} {m = S m'} key (WonderMapCons map maps) =
  case decEq (S n') (S m') of
    Yes prf => SortedMap.lookup key (rewrite prf in map)
    No  _   => if (S n') < (S m')
                 then lookup key maps
                 else Nothing

This way we need an empty map for every empty key length. It's also not quite as general as it should be.

$ idris -p contrib WonderMap.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.1
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
*WonderMap> :t wm
wm : WonderMap (Key Nat) (Value String) 3
*WonderMap> lookup (KCons 0 KNil) wm                                    -- there are no key/value pairs for n = 0
Nothing : Maybe (Value String 1)
*WonderMap> lookup (KCons 0 (KCons 0 KNil)) wm
Just (VCons "a" (VCons "a" VNil)) : Maybe (Value String 2)
*WonderMap> lookup (KCons 0 (KCons 0 (KCons 0 KNil))) wm
Just (VCons "a" (VCons "a" (VCons "a" VNil))) : Maybe (Value String 3)
*WonderMap> lookup (KCons 0 (KCons 0 (KCons 1 KNil))) wm                -- good n, bad key
Nothing : Maybe (Value String 3)
*WonderMap> lookup (KCons 0 (KCons 0 (KCons 0 (KCons 0 KNil)))) wm      -- wm only has key/value pairs for n <= 3
Nothing : Maybe (Value String 4)

A Map type where the value type is dependent on the key type?

1 Answers