值类型依赖于键类型的 Map 类型？

Question

我想知道是否可以实现类似contrib的Data.SortedMapwhere，例如，键类型可以是Key n，值类型是Value n，其中n是相同的Nat?

对于Map (Key n) (Value n)（以“No such variable n”失败），一些常用函数将具有类似这些类型

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

我使用依赖对尝试了以下操作

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

但我认为这里的ns 不是同一个，所以它被解释为

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

换句话说，Key 和 Value 类型没有按照我想要的方式“连接”，即 Value n 只能存储在 Key n 和 lookup 下，对于 Key n 总是返回 @ 987654337@。

和

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

应该创建一个由n : Nat 索引的映射类型，因此我无法将Value 1 值存储在Key 1 键下和 Value 7 值在同一映射中的Key 7 键下。

是否可以实现我想要的映射类型，其中键类型族用于存储相应的值类型族？ （除了每个n : Nat 有一个MyOtherMap，然后将所有这些捆绑在一个更大的结构中，请参阅我的答案）

Answer 1

这个答案并不能真正解决我的问题，它只是一种展示我想要实现的目标的方式（它甚至不是最普遍的情况）。 所以请不要像已经回答的那样拒绝我的问题。 ;-) 谢谢！

我想我会尝试实施这种幼稚的方法。这不是最简单的方法。

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

这样，我们需要为每个空键长度创建一个空映射。它也没有应有的一般性。

$ 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)