暗黙的な引数の順序はどのように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の種類が原因の異なる順序で異なっていることがわかります彼らパラメーター。