Sorry I couldn't think of a less confusing way to put this.
I'm trying to build something like a map that can be safely accessed without returning a maybe, because all of its keys are contained in its type and querying for a key that isn't contained in its list of keys will throw a type error.
data SafeMap : (keys : List k) -> Type -> Type where
Nil : SafeMap [] v
(::) : Pair k v -> SafeMap ks v -> SafeMap (newKey :: ks) v
empty : SafeMap Nil v
empty = Nil
add : k -> v -> SafeMap ks v -> SafeMap (k :: ks) v
add k v l = (k,v) :: l
myDict : SafeMap ["test"] Nat
myDict = add "test" 234 Nil
-- ^^^^^^^^^^^^^^^^^^^ error here
The error message is
While processing right hand side of myDict. When unifying:
SafeMap [?k] Nat
and:
SafeMap [fromString "test"] Nat
Mismatch between: Type and String.
Why does it think that ?k
is of type Type
?
By contrast, if I replace k
with an explicit String
everything works and there's no type error.
data SafeMap : (keys : List String) -> Type -> Type where
-- ^^^^^^ changed here
Nil : SafeMap [] v
(::) : Pair k v -> SafeMap ks v -> SafeMap (newKey :: ks) v
empty : SafeMap Nil v
empty = Nil
add : (k : String) -> v -> SafeMap ks v -> SafeMap (k :: ks) v
-- ^^^^^^ and here
add k v l = (k,v) :: l
myDict : SafeMap ["test"] Nat
myDict = add "test" 234 Nil
-- No error here! ^
Your mistake is here:
add : k -> v -> SafeMap ks v -> SafeMap (k :: ks) v
You want:
add : (k : _) -> v -> SafeMap ks v -> SafeMap (k :: ks) v
In (v : t) ->
, v
is the name of an argument of type t
.