Тип карты, где тип значения зависит от типа ключа? - PullRequest
Новая
       5

Тип карты, где тип значения зависит от типа ключа?

1 голос
/ 12 января 2020

Интересно, можно ли реализовать что-то вроде contrib Data.SortedMap, где, например, тип ключа может быть Key n, а тип значения - Value n, где n - это то же самое Nat?

. Для Map (Key n) (Value n) (который завершается ошибкой с "Нет такой переменной 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)

, но я думаю, что n здесь не то же самое, поэтому он интерпретируется как 

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

другими словами, ключ и типы значений не «связаны» так, как мне бы хотелось, т. е. Value n может храниться только в Key n и lookup, поскольку Key n всегда возвращает Value n.

И 

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

должны создать тип карты с индексом n : Nat, поэтому я не смог сохранить значения Value 1 под Key 1 keys и Value 7 значения в ключах Key 7 на той же карте.

Возможно ли реализовать нужный тип карты, если семейство типов ключей используется для хранения соответствующего семейства типов значений? (Если не считать одного MyOtherMap для каждого n : Nat, а затем объединить все эти элементы в более крупную структуру, см. Мой ответ)

1 Ответ

1 голос
/ 12 января 2020

Этот ответ на самом деле не является решением моей проблемы, это скорее просто способ показать, чего я хочу достичь (и это даже не самый общий случай). Поэтому, пожалуйста, не отклоняйте мой вопрос, как уже ответили. ;-) Спасибо!

Я думал, что попробую реализовать наивный подход. Это не может быть самым простым способом. 

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