module Data.Product import Data.List.Elem %default total infix 10 ^ infix 5 ++ -- Definitions public export data (^) : (0 _ : a -> Type) -> List a -> Type where Nil : x ^ [] (::) : {0 x : a -> Type} -> x i -> x ^ is -> x ^ (i :: is) public export ary : List Type -> Type -> Type ary [] y = y ary (x :: xs) y = x -> ary xs y -- Conversions public export uncurry : map x is `ary` a -> x ^ is -> a uncurry f [] = f uncurry f (x :: xs) = uncurry (f x) xs -- Destructors public export head : x ^ (i :: is) -> x i head (x :: xs) = x public export tail : x ^ (i :: is) -> x ^ is tail (x :: xs) = xs public export consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs consHeadTail (x :: xs) = Refl public export index : x ^ is -> Elem i is -> x i index xs Here = head xs index xs (There elem) = index (tail xs) elem -- Constructors public export tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is tabulate {is = []} f = [] tabulate {is = (i :: is)} f = f Here :: tabulate (f . There) public export indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is) -> index (tabulate f) elem = f elem indexTabulate f Here = Refl indexTabulate f (There elem) = indexTabulate (f . There) elem -- Operations public export map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is map f [] = [] map f (x :: xs) = f _ x :: map f xs public export indexMap : forall x, y . {0 f : (i : a) -> x i -> y i} -> (xs : x ^ is) -> (elem : Elem i is) -> index (map f xs) elem = f i (index xs elem) indexMap (x :: xs) Here = Refl indexMap (x :: xs) (There elem) = indexMap xs elem public export mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs mapId [] = Refl mapId (x :: xs) = cong ((::) x) $ mapId xs public export mapComp : forall x, y, z . {0 f : (i : a) -> y i -> z i} -> {0 g : (i : a) -> x i -> y i} -> (xs : x ^ is) -> map (\i => f i . g i) xs = map f (map g xs) mapComp [] = Refl mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs public export (++) : x ^ is -> x ^ js -> x ^ (is ++ js) (++) [] ys = ys (++) (x :: xs) ys = x :: (xs ++ ys) public export wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is wrap f [] = [] wrap f (x :: xs) = x :: wrap f xs public export mapWrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> (xs : (x . g) ^ is) -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs) mapWrap g [] = Refl mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs public export unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is unwrap f {is = []} [] = [] unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs public export mapUnwrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is) -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs) mapUnwrap g {is = []} [] = Refl mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs public export unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs unwrapWrap u [] = Refl unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs public export wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs wrapUnwrap {is = []} [] = Refl wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs