{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} -- | Intended for qualified import -- -- > import Data.SOP.Tails (Tails(..)) -- > import qualified Data.SOP.Tails as Tails module Data.SOP.Tails ( Tails (..) -- * Convenience constructors , mk1 , mk2 , mk3 -- * SOP-like operators , hcmap , hcpure , hmap , hpure ) where import Data.Kind (Type) import Data.Proxy import Data.SOP.Constraint import Data.SOP.Sing import Data.SOP.Strict hiding (hcmap, hcpure, hmap, hpure) import qualified Data.SOP.Strict as SOP {------------------------------------------------------------------------------- Tails -------------------------------------------------------------------------------} -- | For every tail @(x ': xs)@ of the list, an @f x y@ for every @y@ in @xs@ type Tails :: (k -> k -> Type) -> [k] -> Type data Tails f xs where TNil :: Tails f '[] TCons :: NP (f x) xs -> Tails f xs -> Tails f (x ': xs) {------------------------------------------------------------------------------- Convenience constructors -------------------------------------------------------------------------------} mk1 :: Tails f '[x] mk1 :: forall {k} (f :: k -> k -> *) (x :: k). Tails f '[x] mk1 = NP (f x) '[] -> Tails f '[] -> Tails f '[x] forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons NP (f x) '[] forall {k} (f :: k -> *). NP f '[] Nil Tails f '[] forall {k} (f :: k -> k -> *). Tails f '[] TNil mk2 :: f x y -> Tails f '[x, y] mk2 :: forall {k} (f :: k -> k -> *) (x :: k) (y :: k). f x y -> Tails f '[x, y] mk2 f x y xy = NP (f x) '[y] -> Tails f '[y] -> Tails f '[x, y] forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (f x y xy f x y -> NP (f x) '[] -> NP (f x) '[y] forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NP f xs1 -> NP f (x : xs1) :* NP (f x) '[] forall {k} (f :: k -> *). NP f '[] Nil) Tails f '[y] forall {k} (f :: k -> k -> *) (x :: k). Tails f '[x] mk1 mk3 :: f x y -> f x z -> f y z -> Tails f '[x, y, z] mk3 :: forall {k} (f :: k -> k -> *) (x :: k) (y :: k) (z :: k). f x y -> f x z -> f y z -> Tails f '[x, y, z] mk3 f x y xy f x z xz f y z yz = NP (f x) '[y, z] -> Tails f '[y, z] -> Tails f '[x, y, z] forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (f x y xy f x y -> NP (f x) '[z] -> NP (f x) '[y, z] forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NP f xs1 -> NP f (x : xs1) :* f x z xz f x z -> NP (f x) '[] -> NP (f x) '[z] forall {k} (f :: k -> *) (x :: k) (xs1 :: [k]). f x -> NP f xs1 -> NP f (x : xs1) :* NP (f x) '[] forall {k} (f :: k -> *). NP f '[] Nil) (f y z -> Tails f '[y, z] forall {k} (f :: k -> k -> *) (x :: k) (y :: k). f x y -> Tails f '[x, y] mk2 f y z yz) {------------------------------------------------------------------------------- SOP-like operators -------------------------------------------------------------------------------} hmap :: SListI xs => (forall x y. f x y -> g x y) -> Tails f xs -> Tails g xs hmap :: forall {k} (xs :: [k]) (f :: k -> k -> *) (g :: k -> k -> *). SListI xs => (forall (x :: k) (y :: k). f x y -> g x y) -> Tails f xs -> Tails g xs hmap = Proxy Top -> (forall (x :: k) (y :: k). (Top x, Top y) => f x y -> g x y) -> Tails f xs -> Tails g xs forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (f :: k -> k -> *) (g :: k -> k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y) -> Tails f xs -> Tails g xs hcmap (forall {k} (t :: k). Proxy t forall (t :: k -> Constraint). Proxy t Proxy @Top) hcmap :: forall proxy c f g xs. All c xs => proxy c -> (forall x y. (c x, c y) => f x y -> g x y) -> Tails f xs -> Tails g xs hcmap :: forall {k} (proxy :: (k -> Constraint) -> *) (c :: k -> Constraint) (f :: k -> k -> *) (g :: k -> k -> *) (xs :: [k]). All c xs => proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y) -> Tails f xs -> Tails g xs hcmap proxy c p forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y g = Tails f xs -> Tails g xs forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs' go where go :: All c xs' => Tails f xs' -> Tails g xs' go :: forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs' go Tails f xs' TNil = Tails g xs' Tails g '[] forall {k} (f :: k -> k -> *). Tails f '[] TNil go (TCons NP (f x) xs fs Tails f xs fss) = NP (g x) xs -> Tails g xs -> Tails g (x : xs) forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (proxy c -> (forall (a :: k). c a => f x a -> g x a) -> NP (f x) xs -> NP (g x) xs forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *). (AllN (Prod h) c xs, HAp h) => proxy c -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs SOP.hcmap proxy c p f x a -> g x a forall (a :: k). c a => f x a -> g x a forall (x :: k) (y :: k). (c x, c y) => f x y -> g x y g NP (f x) xs fs) (Tails f xs -> Tails g xs forall (xs' :: [k]). All c xs' => Tails f xs' -> Tails g xs' go Tails f xs fss) hpure :: SListI xs => (forall x y. f x y) -> Tails f xs hpure :: forall {k} (xs :: [k]) (f :: k -> k -> *). SListI xs => (forall (x :: k) (y :: k). f x y) -> Tails f xs hpure = Proxy Top -> (forall (x :: k) (y :: k). (Top x, Top y) => f x y) -> Tails f xs forall {k} (proxy :: (k -> Constraint) -> *) (f :: k -> k -> *) (c :: k -> Constraint) (xs :: [k]). All c xs => proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> Tails f xs hcpure (forall {k} (t :: k). Proxy t forall (t :: k -> Constraint). Proxy t Proxy @Top) hcpure :: forall proxy f c xs. All c xs => proxy c -> (forall x y. (c x, c y) => f x y) -> Tails f xs hcpure :: forall {k} (proxy :: (k -> Constraint) -> *) (f :: k -> k -> *) (c :: k -> Constraint) (xs :: [k]). All c xs => proxy c -> (forall (x :: k) (y :: k). (c x, c y) => f x y) -> Tails f xs hcpure proxy c p forall (x :: k) (y :: k). (c x, c y) => f x y f = SList xs -> Tails f xs forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs' go SList xs forall {k} (xs :: [k]). SListI xs => SList xs sList where go :: All c xs' => SList xs' -> Tails f xs' go :: forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs' go SList xs' SNil = Tails f xs' Tails f '[] forall {k} (f :: k -> k -> *). Tails f '[] TNil go SList xs' SCons = NP (f x) xs -> Tails f xs -> Tails f (x : xs) forall {k} (f :: k -> k -> *) (x :: k) (xs :: [k]). NP (f x) xs -> Tails f xs -> Tails f (x : xs) TCons (proxy c -> (forall (a :: k). c a => f x a) -> NP (f x) xs forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint) (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *). (HPure h, AllN h c xs) => proxy c -> (forall (a :: k). c a => f a) -> h f xs forall (c :: k -> Constraint) (xs :: [k]) (proxy :: (k -> Constraint) -> *) (f :: k -> *). AllN NP c xs => proxy c -> (forall (a :: k). c a => f a) -> NP f xs SOP.hcpure proxy c p f x a forall (a :: k). c a => f x a forall (x :: k) (y :: k). (c x, c y) => f x y f) (SList xs -> Tails f xs forall (xs' :: [k]). All c xs' => SList xs' -> Tails f xs' go SList xs forall {k} (xs :: [k]). SListI xs => SList xs sList)