[Agda] Some problems with K-S basis

[Andreas Abel]

Agda does not infer non-unique values for hidden arguments, even if they 
do not matter.  Since the second argument of K is unused, its type can 
sometimes not be inferred, and you have to give it manually.

For instance, this works (but there are infinitely many other solutions).

   I : {ℓ : _} → {A : Set ℓ} → A → A
   I {A = A} = S K (K {B = A})

Best,
Andreas

On 24.07.2017 10:32, v0id_NULL wrote:
> Dear list,
> 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
> 
> K : {a b : _} → {A : Set a} → {B : Set b} → A → B → A
> K x _ = x
> 
> S : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A → B → C) 
> → (A → B) → A → C
> S x y z = x z (y z)
> 
> this leads to that Agda can not solve some constrains in this definition 
> of I-combinator
> 
> I : {ℓ : _} → {A : Set ℓ} → A → A
> I = S K K
> 
> Agda needs in prompt of this implicit argument
> I = S K (K {_} {_} {_} {?})
> but I don't know how to do this, because it doesn't matter (the second 
> explicit argument of K is discarded by definition).
> 
> But if I define K-combinaor like this
> 
> K : {a : _} → {A : Set a} → A → {b : _} → {B : Set b} → B → A
> K x _ = x
> 
> this leads to that Agda fails to type-check this definition of I-combinator
> 
> I : {ℓ : _} → {A : Set ℓ} → A → A
> I = S K K
> 
> with report containing: "...because this would result in an invalid use 
> of Setω..."
> 
> 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?
> 
> Generaly, tell me, please, is it good idea to implement something like 
> combinatory logic via Agda?
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/