v0ιd

2018-02-17 09:37:35 UTC

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.

Termination checking failed for the following functions:

zip-with

Problematic calls:

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?

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.

Termination checking failed for the following functions:

zip-with

Problematic calls:

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?