<div dir="ltr"><div>Dear list,</div><div>Help me, please. I try to deal with combinatory logic via Agda, but I have some problems with defining of K-combinator. If I define K and S combinators like this</div><div><br></div><div>K : {a b : _} → {A : Set a} → {B : Set b} → A → B → A</div><div>K x _ = x</div><div><br></div><div>S : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A → B → C) → (A → B) → A → C</div><div>S x y z = x z (y z)</div><div><br></div><div>this leads to that Agda can not solve some constrains in this definition of I-combinator</div><div><br></div><div>I : {ℓ : _} → {A : Set ℓ} → A → A</div><div>I = S K K</div><div><br></div><div>Agda needs in prompt of this implicit argument</div><div>I = S K (K {_} {_} {_} {?})</div><div>but I don't know how to do this, because it doesn't matter (the second explicit argument of K is discarded by definition).</div><div><br></div><div>But if I define K-combinaor like this</div><div><br></div><div>K : {a : _} → {A : Set a} → A → {b : _} → {B : Set b} → B → A</div><div>K x _ = x</div><div><br></div><div>this leads to that Agda fails to type-check this definition of I-combinator</div><div><br></div><div>I : {ℓ : _} → {A : Set ℓ} → A → A</div><div>I = S K K</div><div><br></div><div>with report containing: "...because this would result in an invalid use of Setω..."</div><div><br></div><div>How I must to define S-K basis, enough right to define complex combinators with applicative by like (K K), (S (K S) K) and so on?</div><div><br></div><div>Generaly, tell me, please, is it good idea to implement something like combinatory logic via Agda?</div></div>