Идрис не уменьшает поиск по карте - PullRequest
Новая
       9

Идрис не уменьшает поиск по карте

0 голосов
/ 19 января 2019

Почему не уменьшить вызов функции? Как я могу проверить во время компиляции, что карта содержит пару ключ-значение? 

import Data.SortedMap

N : SortedMap String Type
N = fromList
    [ ("a", Nat)
    , ("b", String)
    ]

t : lookup "a" N = Just Nat
t = Refl

Type mismatch between
        Just Nat = Just Nat (Type of Refl)
and
        lookup "a" (fromList [("a", Nat), ("b", String)]) = Just Nat (Expected type)

Specifically:
        Type mismatch between
                Just Nat
        and
                lookup "a" (fromList [("a", Nat), ("b", String)])

1 Ответ

0 голосов
/ 21 января 2019

Это должно быть связано с реализацией SortedMap, так как версия, использующая простой List, работает как положено: 

N : List (String, Type)
N =
    [ ("a", Nat)
    , ("b", String)
    ]

t : lookup "a" N = Just Nat
t = Refl

Согласно документам Data.SortedMap.lookup также является полным, поэтому его следует уменьшить. Возможно, причина в том, что функции и типы данных в SortedMap, похоже, имеют спецификатор экспорта, тогда как в Data.List используются public export.

...