------------------------------------------------------------------------
-- The Agda standard library
--
-- Nondependent N-ary functions manipulating lists
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Nary.NonDependent where
open import Data.Nat.Base using (zero; suc)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.Product.Base as Product using (_,_)
open import Data.Product.Nary.NonDependent using (Product)
open import Function.Nary.NonDependent.Base using (Arrows; Sets; _<$>_)
------------------------------------------------------------------------
-- n-ary smart constructors
nilₙ : ∀ n {ls} {as : Sets n ls} → Product n (List <$> as)
nilₙ 0 = _
nilₙ 1 = []
nilₙ (suc n@(suc _)) = [] , nilₙ n
consₙ : ∀ n {ls} {as : Sets n ls} →
Product n as → Product n (List <$> as) → Product n (List <$> as)
consₙ 0 _ _ = _
consₙ 1 a as = a ∷ as
consₙ (suc n@(suc _)) (a , xs) (as , xss) = a ∷ as , consₙ n xs xss
------------------------------------------------------------------------
-- n-ary zipWith-like operations
zipWith : ∀ n {ls} {as : Sets n ls} {r} {R : Set r} →
Arrows n as R → Arrows n (List <$> as) (List R)
zipWith 0 f = []
zipWith 1 f xs = List.map f xs
zipWith (suc n@(suc _)) f xs ys =
zipWith n (Product.uncurry f) (List.zipWith _,_ xs ys)
unzipWith : ∀ n {ls} {as : Sets n ls} {a} {A : Set a} →
(A → Product n as) → (List A → Product n (List <$> as))
unzipWith n f [] = nilₙ n
unzipWith n f (a ∷ as) = consₙ n (f a) (unzipWith n f as)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4