Do you need the recursive call? I started implementing the same

function using Vec instead of List to make the size invariant

clearer and after a bit of cleaning up I got an implementation

which is just using two folds (which makes sense: the first one

performs the induction, the second one is merely used to do a

case analysis)

================================================================

open import Agda.Builtin.Nat

id : {a : _} â {A : Set a} â A â A

id x = x

data Vec {a} (A : Set a) : Nat â Set a where

Â nil : Vec A 0

Â cons : â {n} â A â Vec A n â Vec A (suc n)

module _ {a b} {A : Set a} (B : Nat â Set b) where

Â fold : â {n} â Vec A n â (â {n} â A â Vec A n â B n â B (suc n)) â B 0

â B n

Â fold nilÂ Â Â Â Â Â Â Â c n = n

Â fold (cons x xs) c n = c x xs (fold xs c n)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c}Â where

Â zip-with : â {n} â (A â B â C) â Vec A n â Vec B n â Vec C n

Â zip-with f xs ys = fold P xs step base ys where

Â P : Nat â Set _

Â P n = Vec B n â Vec C n

Â step : â {n} â A â Vec A n â P n â P (suc n)

Â step x xs rec yys = fold (Vec C) yys (Î» y ys â cons (f x y)) nil

Â base : P 0

Â base _ = nil

================================================================

Cheers,

*Post by v0Î¹d*Dear list,

I try to define a zip-with function without pattern matching through

universal constructor eliminator for Lists.

idÂ : {a : _} â {A : Set a} â A â A

idÂ x = x

data List {a} (A : Set a) : Set a where

Â nil : List A

Â cons : A â List A â List A

fold : {a b c : _} â {A : Set a} â {B : Set b} â {C : Set c} â List A

â (A â List A â ((B â C) â B â C) â (B â C) â B â C) â (B â C) â B â C

fold nil _ fs s = fs s

fold (cons x xs) f = f x xs (fold xs f)

zip-with : {a b c : _} â {A : Set a} â {B : Set b} â {C : Set c} â (A

â B â C) â List A â List B â List C

zip-with f x y = fold x (Î» ÎŸ ÎŸs _ _ _ â fold y (Î» Î· Î·s _ _ _ â cons (f

ÎŸ Î·) (zip-with f ÎŸs Î·s)) id nil) id nil

But it fails termination checking.

Â zip-with

Â zip-with f ÎŸs Î·s

I would not want to suppressÂ termination checking at all withÂ {-#

TERMINATING #-}.

What can I do here? Maybe it makes sense somehow to

improveÂ termination checker for so obvious cases?

_______________________________________________

Agda mailing list

https://lists.chalmers.se/mailman/listinfo/agda