Идрис: Неявные параметры в записях

Когда я пытаюсь скомпилировать этот пример

record R where
    f: () -> {t: Type} -> t

Я получаю эту ошибку:

Type mismatch between
        () -> t1 (Type of f)
and
        () -> t (Expected type)

Specifically:
        Type mismatch between
                t1
        and
                t

С другой стороны, этот пример

record R where
    f: {t: Type} -> () -> t

работает просто отлично. Можете ли вы сказать мне, что не так с первым?


idris
person Gregg54654    schedule 16.09.2017    source источник
comment
Я не уверен, но я полагаю, что неявные параметры должны стоять перед неявными.   -  person marcosh    schedule 17.09.2017
comment
Да, может быть. Это немного странно, потому что это не проблема с эквивалентным определением, использующим данные: data D: Type where MkD: (f: () -> {t: Type} -> t) -> D   -  person Gregg54654    schedule 17.09.2017
comment
У меня также были проблемы с созданием экземпляра такой записи. У меня не было проблем с данными. К сожалению, у меня нет простого примера для этого.   -  person Gregg54654    schedule 17.09.2017
comment
Вы не можете создать экземпляр такой записи, потому что это невозможно. Эта часть {t: Type} -> t типа функции говорит, что для заданного типа любого вы можете построить терм этого типа. Но это невозможно, например. для пустого типа (Void).   -  person Anton Trunov    schedule 18.09.2017
comment
Да, это верно для этого примера. Это утверждение было связано с другим более сложным примером, где это не проблема. Но тем временем я пришел к выводу, что это была моя вина и это было просто связано с умозаключением.   -  person Gregg54654    schedule 18.09.2017

Ответы (1)


arrow_upward
1
arrow_downward

Это ошибка в Idris: иногда оператор -> не является правоассоциативным: issue #4077.

Чтобы увидеть это, мы можем очистить синтаксис записи:

data R : Type where
  MkR : (() -> {t : Type} -> t) -> R

Теперь нам нужно вручную реализовать проекцию f. Оказывается, что

f : R -> (() -> {t : Type} -> t)
f (MkR g) = g

не проверяет тип, но

f : R -> () -> {t : Type} -> t
f (MkR g) = g

делает.

Мне кажется, что Идрис использует первый вариант для удаления сахара из record в data, отсюда и наблюдаемая вами ошибка.

person Anton Trunov    schedule 18.09.2017