Как написать правильную подпись типа для Vect в Идрисе?

Недавно я исследовал зависимые типы в Идрисе. Однако я столкнулся с проблемой, которая довольно раздражает, а именно в Идрисе: я должен запускать свою программу с сигнатурой типа. Итак, проблема в том, Как я могу написать краткую подпись типа в Идрисе?

Например,

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String))
get_member store idx = Vect.mapMaybe maybe_member (Vect.fromList idx)
  where
    maybe_member : (x : Fin n) -> Maybe (Nat, String)
-- The below line should be type corrected
-- maybe_member x = Just (Data.Fin.finToNat x, Vect.index x store)

Если я прокомментирую последнюю строку, компиляция проверит указанную выше функцию, но если я сделаю последнюю строку выражением, компиляция будет жаловаться.

When checking right hand side of VecSort.get_member, maybe_member with expected type
        Maybe (Nat, String)
When checking an application of function Data.Vect.index:
        Type mismatch between
                Vect n1 String (Type of store)
        and
                Vect n String (Expected type)

        Specifically:
                Type mismatch between
                        n1
                and
                        n

Но я делаю это как лямбда-функцию,

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String))
get_member store idx = Vect.mapMaybe (\x => Just (Data.Fin.finToNat x, Vect.index x store)) (Vect.fromList idx)

это также будет проверка типа.

Итак, вопрос в том, как мне определить тип Vect с правильной длиной в сигнатуре типа?


dependent-type purely-functional idris
person gostriderful    schedule 13.08.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Я не уверен, правильно ли мое объяснение, но следующие проверки типов:

get_member : (store : Vect n String) -> (idx : List (Fin n)) -> (m : Nat ** Vect m (Nat, String))
get_member store idx {n} = Vect.mapMaybe (maybe_member) (Vect.fromList idx)
    where
      maybe_member : (x : Fin n) -> Maybe (Nat, String)
      maybe_member x = Just (Data.Fin.finToNat x, Vect.index x store)

Разница в том, что вы получаете неявный параметр n в свою область видимости. Эти {n} и x: Fin x относятся к одному и тому же n. Без использования неявного n в вашей области действия idris не может предположить, что оба n действительно одинаковы, и будет жаловаться с сообщением об ошибке, что не знает, совпадают ли n1 и n.

person Markus    schedule 14.08.2017