Как порядок неявных аргументов влияет на idris?

Question

Это не удается:

> the ({A : Type} -> A -> {B : Type} -> B -> (A, B)) MkPair
(input):1:5:When checking argument value to function Prelude.Basics.the:
        Type mismatch between
                A -> B1 -> (A, B1) (Type of MkPair)
        and
                A1 -> B -> (A1, B) (Expected type)

        Specifically:
                Type mismatch between
                        Pair A
                and
                        \uv => uv -> uv

Это работает:

> ({A : Type} -> {B : Type} -> A -> B -> (A, B)) MkPair
\A1, B1 => MkPair : A -> B -> (A, B)

Как ни странно:

q : {A : Type} -> A -> {B : Type} -> B -> (A, B)
q a b = MkPair a b

> :t q
q : A -> B -> (A, B)

> :t MkPair
MkPair : A -> B -> (A, B)

Почему q а также MkPair Похоже, имеют тот же тип? Они действительно имеют один и тот же тип? Почему порядок неявных аргументов имеет значение?

Answer 1

В некотором смысле неявные аргументы ничем не отличаются от неявных. Компилятор выводит их для вас большую часть времени, но они все еще являются аргументами и должны присутствовать, потому что на уровне основного языка нет неявных аргументов. Вы можете попросить REPL показать последствия для вас:

λΠ> :set showimplicits
λΠ> :t MkPair
Builtins.MkPair : {A : Type} -> {B : Type} -> (a : A) -> (b : B) -> (A, B)
λΠ> :t q
Main.q : {A : Type} -> A -> {B : Type} -> B -> (A, B)

Если вы замените обычные скобки на фигурные скобки в указанных выше типах, вы увидите, что типы MkPair а также q отличаются из-за разного порядка их параметров.