암시 적 인수의 순서는 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

암시 적 인수는 암시 적 인수와 다르지 않습니다. 컴파일러는 대부분 당신을 위해 그들을 추론하지만, 여전히 핵심적인 언어의 수준에서 암시 적 인수가 없기 때문에 인수가 존재해야합니다. 당신은 당신을 위해 implicits을 보여 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의 종류 때문에의 다른 순서의 다른 것을 볼 수 있습니다 자신의 매개 변수.