隐式参数的顺序如何影响 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 的类型因参数顺序不同而有所不同。

隐式参数的顺序如何影响 idris？

How does the order of implicit arguments affect idris?

idris