Safe Haskell	None
Language	Haskell2010

Agda.Utils.Zip

Description

Overloaded zip and zipWith.

This module provides the Zip class to overload zipping functions for variants of the list type ('[]', List1, List2, ListInf).

Motivation: In practice, we often zip a finite list with an infinite list, e.g. zipWith f xs (ys ++ repeat z). We can know statically in this case that the resulting considers each xs by rewriting this to zipWith f xs (ListInf.pad ys z) statically exposing the infinite nature of the second list. To avoid cluttering the namespace with 4*4 variants of zipWith for all combination of our list types, we introduce an overloaded version.

Import this module as follows:

import Prelude hiding (zip, zipWith)
import Agda.Utils.Zip

Documentation

class Zip (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type) | f g -> h where Source #

Minimal complete definition

zipWith

Methods

zip :: f a -> g b -> h (a, b) Source #

zipWith :: (a -> b -> c) -> f a -> g b -> h c Source #

Instances

Instances details

Zip List1 List1 List1 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List1 a -> List1 b -> List1 (a, b) Source # zipWith :: (a -> b -> c) -> List1 a -> List1 b -> List1 c Source #
Zip List1 List2 List1 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List1 a -> List2 b -> List1 (a, b) Source # zipWith :: (a -> b -> c) -> List1 a -> List2 b -> List1 c Source #
Zip List1 ListInf List1 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List1 a -> ListInf b -> List1 (a, b) Source # zipWith :: (a -> b -> c) -> List1 a -> ListInf b -> List1 c Source #
Zip List1 [] [] Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List1 a -> [b] -> [(a, b)] Source # zipWith :: (a -> b -> c) -> List1 a -> [b] -> [c] Source #
Zip List2 List1 List1 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List2 a -> List1 b -> List1 (a, b) Source # zipWith :: (a -> b -> c) -> List2 a -> List1 b -> List1 c Source #
Zip List2 List2 List2 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List2 a -> List2 b -> List2 (a, b) Source # zipWith :: (a -> b -> c) -> List2 a -> List2 b -> List2 c Source #
Zip List2 ListInf List2 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List2 a -> ListInf b -> List2 (a, b) Source # zipWith :: (a -> b -> c) -> List2 a -> ListInf b -> List2 c Source #
Zip List2 [] [] Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: List2 a -> [b] -> [(a, b)] Source # zipWith :: (a -> b -> c) -> List2 a -> [b] -> [c] Source #
Zip ListInf List1 List1 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: ListInf a -> List1 b -> List1 (a, b) Source # zipWith :: (a -> b -> c) -> ListInf a -> List1 b -> List1 c Source #
Zip ListInf List2 List2 Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: ListInf a -> List2 b -> List2 (a, b) Source # zipWith :: (a -> b -> c) -> ListInf a -> List2 b -> List2 c Source #
Zip ListInf ListInf ListInf Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: ListInf a -> ListInf b -> ListInf (a, b) Source # zipWith :: (a -> b -> c) -> ListInf a -> ListInf b -> ListInf c Source #
Zip ListInf [] [] Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: ListInf a -> [b] -> [(a, b)] Source # zipWith :: (a -> b -> c) -> ListInf a -> [b] -> [c] Source #
Zip [] List1 [] Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: [a] -> List1 b -> [(a, b)] Source # zipWith :: (a -> b -> c) -> [a] -> List1 b -> [c] Source #
Zip [] List2 [] Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: [a] -> List2 b -> [(a, b)] Source # zipWith :: (a -> b -> c) -> [a] -> List2 b -> [c] Source #
Zip [] ListInf [] Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: [a] -> ListInf b -> [(a, b)] Source # zipWith :: (a -> b -> c) -> [a] -> ListInf b -> [c] Source #
Zip [] [] [] Source #
Instance details Defined in Agda.Utils.Zip Methods zip :: [a] -> [b] -> [(a, b)] Source # zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] Source #