{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} -- | Type-level counting -- -- Intended for unqualified import. module Ouroboros.Consensus.Util.Counting ( AtMost (..) , Exactly (.., ExactlyNil, ExactlyCons) , NonEmpty (..) -- * Working with 'Exactly' , exactlyHead , exactlyOne , exactlyReplicate , exactlyTail , exactlyTwo , exactlyWeaken , exactlyWeakenNonEmpty , exactlyZip , exactlyZipFoldable -- * Working with 'AtMost' , atMostHead , atMostInit , atMostLast , atMostNonEmpty , atMostOne , atMostZipFoldable -- * Working with 'NonEmpty' , nonEmptyFromList , nonEmptyHead , nonEmptyInit , nonEmptyLast , nonEmptyMapOne , nonEmptyMapTwo , nonEmptyStrictPrefixes , nonEmptyToList , nonEmptyWeaken ) where import Control.Applicative import qualified Data.Foldable as Foldable import Data.Kind (Type) import Data.SOP.Dict import Data.SOP.Strict import Ouroboros.Consensus.Util.SOP {------------------------------------------------------------------------------- Types -------------------------------------------------------------------------------} newtype Exactly xs a = Exactly { Exactly xs a -> NP (K a) xs getExactly :: NP (K a) xs } -- | At most one value for each type level index data AtMost :: [Type] -> Type -> Type where AtMostNil :: AtMost xs a AtMostCons :: !a -> !(AtMost xs a) -> AtMost (x ': xs) a -- | Non-empty variation on 'AtMost' data NonEmpty :: [Type] -> Type -> Type where NonEmptyOne :: !a -> NonEmpty (x ': xs) a NonEmptyCons :: !a -> !(NonEmpty xs a) -> NonEmpty (x ': xs) a deriving instance Eq a => Eq (AtMost xs a) deriving instance Eq a => Eq (NonEmpty xs a) deriving instance Show a => Show (AtMost xs a) deriving instance Show a => Show (NonEmpty xs a) deriving instance Functor (AtMost xs) deriving instance Foldable (AtMost xs) deriving instance Traversable (AtMost xs) deriving instance Functor (NonEmpty xs) deriving instance Foldable (NonEmpty xs) deriving instance Traversable (NonEmpty xs) {------------------------------------------------------------------------------- Pattern synonyms for 'Exactly' -------------------------------------------------------------------------------} -- | Internal: view on 'Exactly' -- -- Used for the pattern synonyms only. data ExactlyView xs a where ENil :: ExactlyView '[] a ECons :: a -> Exactly xs a -> ExactlyView (x : xs) a -- | Internal: construct the view on 'Exactly' -- -- Used for the pattern synonyms only. exactlyView :: Exactly xs a -> ExactlyView xs a exactlyView :: Exactly xs a -> ExactlyView xs a exactlyView (Exactly (K a x :* NP (K a) xs xs)) = a -> Exactly xs a -> ExactlyView (x : xs) a forall a (xs :: [*]) x. a -> Exactly xs a -> ExactlyView (x : xs) a ECons a x (NP (K a) xs -> Exactly xs a forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly NP (K a) xs xs) exactlyView (Exactly NP (K a) xs Nil) = ExactlyView xs a forall a. ExactlyView '[] a ENil {-# COMPLETE ExactlyNil, ExactlyCons #-} pattern ExactlyCons :: () => xs' ~ (x ': xs) => a -> Exactly xs a -> Exactly xs' a pattern $bExactlyCons :: a -> Exactly xs a -> Exactly xs' a $mExactlyCons :: forall r (xs' :: [*]) a. Exactly xs' a -> (forall x (xs :: [*]). (xs' ~ (x : xs)) => a -> Exactly xs a -> r) -> (Void# -> r) -> r ExactlyCons x xs <- (exactlyView -> ECons x xs) where ExactlyCons a x Exactly xs a xs = NP (K a) (x : xs) -> Exactly (x : xs) a forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly (a -> K a x forall k a (b :: k). a -> K a b K a x K a x -> NP (K a) xs -> NP (K a) (x : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* (Exactly xs a -> NP (K a) xs forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs getExactly Exactly xs a xs)) pattern ExactlyNil :: () => xs ~ '[] => Exactly xs a pattern $bExactlyNil :: Exactly xs a $mExactlyNil :: forall r (xs :: [*]) a. Exactly xs a -> ((xs ~ '[]) => r) -> (Void# -> r) -> r ExactlyNil <- (exactlyView -> ENil) where ExactlyNil = NP (K a) '[] -> Exactly '[] a forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly NP (K a) '[] forall k (f :: k -> *). NP f '[] Nil {------------------------------------------------------------------------------- Type class instances for 'Exactly' For 'AtMost' and 'NonEmpty' we can just derive these, but for 'Exactly' we need to do a bit more work. -------------------------------------------------------------------------------} instance Functor (Exactly xs) where fmap :: (a -> b) -> Exactly xs a -> Exactly xs b fmap a -> b f (Exactly NP (K a) xs xs) = NP (K a) xs -> (SListI xs => Exactly xs b) -> Exactly xs b forall k (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (K a) xs xs ((SListI xs => Exactly xs b) -> Exactly xs b) -> (SListI xs => Exactly xs b) -> Exactly xs b forall a b. (a -> b) -> a -> b $ NP (K b) xs -> Exactly xs b forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly (NP (K b) xs -> Exactly xs b) -> NP (K b) xs -> Exactly xs b forall a b. (a -> b) -> a -> b $ (forall a. K a a -> K b a) -> NP (K a) xs -> NP (K b) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap ((a -> b) -> K a a -> K b a forall k1 k2 a b (c :: k1) (d :: k2). (a -> b) -> K a c -> K b d mapKK a -> b f) NP (K a) xs xs instance Foldable (Exactly xs) where foldMap :: (a -> m) -> Exactly xs a -> m foldMap a -> m f (Exactly NP (K a) xs xs) = NP (K a) xs -> (SListI xs => m) -> m forall k (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (K a) xs xs ((SListI xs => m) -> m) -> (SListI xs => m) -> m forall a b. (a -> b) -> a -> b $ (a -> m) -> [a] -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap a -> m f (NP (K a) xs -> CollapseTo NP a forall k l (h :: (k -> *) -> l -> *) (xs :: l) a. (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a hcollapse NP (K a) xs xs) instance Traversable (Exactly xs) where traverse :: (a -> f b) -> Exactly xs a -> f (Exactly xs b) traverse a -> f b f (Exactly NP (K a) xs xs) = NP (K a) xs -> (SListI xs => f (Exactly xs b)) -> f (Exactly xs b) forall k (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (K a) xs xs ((SListI xs => f (Exactly xs b)) -> f (Exactly xs b)) -> (SListI xs => f (Exactly xs b)) -> f (Exactly xs b) forall a b. (a -> b) -> a -> b $ (NP (K b) xs -> Exactly xs b) -> f (NP (K b) xs) -> f (Exactly xs b) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap NP (K b) xs -> Exactly xs b forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly (f (NP (K b) xs) -> f (Exactly xs b)) -> f (NP (K b) xs) -> f (Exactly xs b) forall a b. (a -> b) -> a -> b $ NP (f :.: K b) xs -> f (NP (K b) xs) forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *) (g :: k -> *). (HSequence h, SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs) hsequence' (NP (f :.: K b) xs -> f (NP (K b) xs)) -> NP (f :.: K b) xs -> f (NP (K b) xs) forall a b. (a -> b) -> a -> b $ (forall a. K a a -> (:.:) f (K b) a) -> NP (K a) xs -> NP (f :.: K b) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *). (SListIN (Prod h) xs, HAp h) => (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs hmap (\(K x) -> f (K b a) -> (:.:) f (K b) a forall l k (f :: l -> *) (g :: k -> l) (p :: k). f (g p) -> (:.:) f g p Comp (f (K b a) -> (:.:) f (K b) a) -> f (K b a) -> (:.:) f (K b) a forall a b. (a -> b) -> a -> b $ b -> K b a forall k a (b :: k). a -> K a b K (b -> K b a) -> f b -> f (K b a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> f b f a x) NP (K a) xs xs instance Show a => Show (Exactly xs a) where show :: Exactly xs a -> String show (Exactly NP (K a) xs xs) = NP (K a) xs -> (SListI xs => String) -> String forall k (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (K a) xs xs ((SListI xs => String) -> String) -> (SListI xs => String) -> String forall a b. (a -> b) -> a -> b $ case Dict (All (Compose Show (K a))) xs SListI xs => Dict (All (Compose Show (K a))) xs dict of Dict (All (Compose Show (K a))) xs Dict -> NP (K a) xs -> String forall a. Show a => a -> String show NP (K a) xs xs where dict :: SListI xs => Dict (All (Compose Show (K a))) xs dict :: Dict (All (Compose Show (K a))) xs dict = NP (Dict (Compose Show (K a))) xs -> Dict (All (Compose Show (K a))) xs forall k (c :: k -> Constraint) (xs :: [k]). NP (Dict c) xs -> Dict (All c) xs all_NP ((forall a. Dict (Compose Show (K a)) a) -> NP (Dict (Compose Show (K a))) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *). (HPure h, SListIN h xs) => (forall (a :: k). f a) -> h f xs hpure forall a. Dict (Compose Show (K a)) a forall k (c :: k -> Constraint) (a :: k). c a => Dict c a Dict) instance Eq a => Eq (Exactly xs a) where Exactly NP (K a) xs xs == :: Exactly xs a -> Exactly xs a -> Bool == Exactly NP (K a) xs xs' = NP (K a) xs -> (SListI xs => Bool) -> Bool forall k (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (K a) xs xs ((SListI xs => Bool) -> Bool) -> (SListI xs => Bool) -> Bool forall a b. (a -> b) -> a -> b $ case Dict (All (Compose Eq (K a))) xs SListI xs => Dict (All (Compose Eq (K a))) xs dict of Dict (All (Compose Eq (K a))) xs Dict -> NP (K a) xs xs NP (K a) xs -> NP (K a) xs -> Bool forall a. Eq a => a -> a -> Bool == NP (K a) xs xs' where dict :: SListI xs => Dict (All (Compose Eq (K a))) xs dict :: Dict (All (Compose Eq (K a))) xs dict = NP (Dict (Compose Eq (K a))) xs -> Dict (All (Compose Eq (K a))) xs forall k (c :: k -> Constraint) (xs :: [k]). NP (Dict c) xs -> Dict (All c) xs all_NP ((forall a. Dict (Compose Eq (K a)) a) -> NP (Dict (Compose Eq (K a))) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *). (HPure h, SListIN h xs) => (forall (a :: k). f a) -> h f xs hpure forall a. Dict (Compose Eq (K a)) a forall k (c :: k -> Constraint) (a :: k). c a => Dict c a Dict) {------------------------------------------------------------------------------- Working with 'Exactly' -------------------------------------------------------------------------------} -- | Singleton exactlyOne :: a -> Exactly '[x] a exactlyOne :: a -> Exactly '[x] a exactlyOne a a = NP (K a) '[x] -> Exactly '[x] a forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly (NP (K a) '[x] -> Exactly '[x] a) -> NP (K a) '[x] -> Exactly '[x] a forall a b. (a -> b) -> a -> b $ a -> K a x forall k a (b :: k). a -> K a b K a a K a x -> NP (K a) '[] -> NP (K a) '[x] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP (K a) '[] forall k (f :: k -> *). NP f '[] Nil -- | From a pair exactlyTwo :: a -> a -> Exactly '[x, y] a exactlyTwo :: a -> a -> Exactly '[x, y] a exactlyTwo a a1 a a2 = NP (K a) '[x, y] -> Exactly '[x, y] a forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly (NP (K a) '[x, y] -> Exactly '[x, y] a) -> NP (K a) '[x, y] -> Exactly '[x, y] a forall a b. (a -> b) -> a -> b $ a -> K a x forall k a (b :: k). a -> K a b K a a1 K a x -> NP (K a) '[y] -> NP (K a) '[x, y] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* a -> K a y forall k a (b :: k). a -> K a b K a a2 K a y -> NP (K a) '[] -> NP (K a) '[y] forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP (K a) '[] forall k (f :: k -> *). NP f '[] Nil -- | Analogue of 'head' exactlyHead :: Exactly (x ': xs) a -> a exactlyHead :: Exactly (x : xs) a -> a exactlyHead = K a x -> a forall k a (b :: k). K a b -> a unK (K a x -> a) -> (Exactly (x : xs) a -> K a x) -> Exactly (x : xs) a -> a forall b c a. (b -> c) -> (a -> b) -> a -> c . NP (K a) (x : xs) -> K a x forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x hd (NP (K a) (x : xs) -> K a x) -> (Exactly (x : xs) a -> NP (K a) (x : xs)) -> Exactly (x : xs) a -> K a x forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly (x : xs) a -> NP (K a) (x : xs) forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs getExactly -- | Analogue of 'tail' exactlyTail :: Exactly (x ': xs) a -> Exactly xs a exactlyTail :: Exactly (x : xs) a -> Exactly xs a exactlyTail = NP (K a) xs -> Exactly xs a forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly (NP (K a) xs -> Exactly xs a) -> (Exactly (x : xs) a -> NP (K a) xs) -> Exactly (x : xs) a -> Exactly xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . NP (K a) (x : xs) -> NP (K a) xs forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> NP f xs tl (NP (K a) (x : xs) -> NP (K a) xs) -> (Exactly (x : xs) a -> NP (K a) (x : xs)) -> Exactly (x : xs) a -> NP (K a) xs forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly (x : xs) a -> NP (K a) (x : xs) forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs getExactly -- | Analogue of 'zip' exactlyZip :: Exactly xs a -> Exactly xs b -> Exactly xs (a, b) exactlyZip :: Exactly xs a -> Exactly xs b -> Exactly xs (a, b) exactlyZip (Exactly NP (K a) xs np) (Exactly NP (K b) xs np') = NP (K (a, b)) xs -> Exactly xs (a, b) forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly (NP (K (a, b)) xs -> Exactly xs (a, b)) -> NP (K (a, b)) xs -> Exactly xs (a, b) forall a b. (a -> b) -> a -> b $ NP (K a) xs -> (SListI xs => NP (K (a, b)) xs) -> NP (K (a, b)) xs forall k (a :: k -> *) (xs :: [k]) r. NP a xs -> (SListI xs => r) -> r npToSListI NP (K a) xs np ((SListI xs => NP (K (a, b)) xs) -> NP (K (a, b)) xs) -> (SListI xs => NP (K (a, b)) xs) -> NP (K (a, b)) xs forall a b. (a -> b) -> a -> b $ (forall a. K a a -> K b a -> K (a, b) a) -> Prod NP (K a) xs -> NP (K b) xs -> NP (K (a, b)) xs forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *) (f' :: k -> *) (f'' :: k -> *). (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall (a :: k). f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs hzipWith (\(K x) (K y) -> (a, b) -> K (a, b) a forall k a (b :: k). a -> K a b K (a x, b y)) Prod NP (K a) xs NP (K a) xs np NP (K b) xs np' -- | Analogue of 'zip' where the length of second argument is unknown exactlyZipFoldable :: Foldable t => Exactly xs a -> t b -> AtMost xs (a, b) exactlyZipFoldable :: Exactly xs a -> t b -> AtMost xs (a, b) exactlyZipFoldable = \(Exactly NP (K a) xs as) t b bs -> NP (K a) xs -> [b] -> AtMost xs (a, b) forall a (xs :: [*]) b. NP (K a) xs -> [b] -> AtMost xs (a, b) go NP (K a) xs as (t b -> [b] forall (t :: * -> *) a. Foldable t => t a -> [a] Foldable.toList t b bs) where go :: NP (K a) xs -> [b] -> AtMost xs (a, b) go :: NP (K a) xs -> [b] -> AtMost xs (a, b) go NP (K a) xs _ [] = AtMost xs (a, b) forall (xs :: [*]) a. AtMost xs a AtMostNil go NP (K a) xs Nil [b] _ = AtMost xs (a, b) forall (xs :: [*]) a. AtMost xs a AtMostNil go (K a a :* NP (K a) xs as) (b b:[b] bs) = (a, b) -> AtMost xs (a, b) -> AtMost (x : xs) (a, b) forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a AtMostCons (a a, b b) (AtMost xs (a, b) -> AtMost (x : xs) (a, b)) -> AtMost xs (a, b) -> AtMost (x : xs) (a, b) forall a b. (a -> b) -> a -> b $ NP (K a) xs -> [b] -> AtMost xs (a, b) forall a (xs :: [*]) b. NP (K a) xs -> [b] -> AtMost xs (a, b) go NP (K a) xs as [b] bs exactlyWeaken :: Exactly xs a -> AtMost xs a exactlyWeaken :: Exactly xs a -> AtMost xs a exactlyWeaken = NP (K a) xs -> AtMost xs a forall a (xs :: [*]). NP (K a) xs -> AtMost xs a go (NP (K a) xs -> AtMost xs a) -> (Exactly xs a -> NP (K a) xs) -> Exactly xs a -> AtMost xs a forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly xs a -> NP (K a) xs forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs getExactly where go :: NP (K a) xs -> AtMost xs a go :: NP (K a) xs -> AtMost xs a go NP (K a) xs Nil = AtMost xs a forall (xs :: [*]) a. AtMost xs a AtMostNil go (K a x :* NP (K a) xs xs) = a -> AtMost xs a -> AtMost (x : xs) a forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a AtMostCons a x (NP (K a) xs -> AtMost xs a forall a (xs :: [*]). NP (K a) xs -> AtMost xs a go NP (K a) xs xs) exactlyWeakenNonEmpty :: Exactly (x ': xs) a -> NonEmpty (x ': xs) a exactlyWeakenNonEmpty :: Exactly (x : xs) a -> NonEmpty (x : xs) a exactlyWeakenNonEmpty = NP (K a) (x : xs) -> NonEmpty (x : xs) a forall a x (xs :: [*]). NP (K a) (x : xs) -> NonEmpty (x : xs) a go (NP (K a) (x : xs) -> NonEmpty (x : xs) a) -> (Exactly (x : xs) a -> NP (K a) (x : xs)) -> Exactly (x : xs) a -> NonEmpty (x : xs) a forall b c a. (b -> c) -> (a -> b) -> a -> c . Exactly (x : xs) a -> NP (K a) (x : xs) forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs getExactly where go :: NP (K a) (x ': xs) -> NonEmpty (x ': xs) a go :: NP (K a) (x : xs) -> NonEmpty (x : xs) a go (K a x :* NP (K a) xs Nil) = a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne a x go (K a x :* xs :: NP (K a) xs xs@(K a x _ :* NP (K a) xs _)) = a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x (NP (K a) (x : xs) -> NonEmpty (x : xs) a forall a x (xs :: [*]). NP (K a) (x : xs) -> NonEmpty (x : xs) a go NP (K a) xs NP (K a) (x : xs) xs) -- | Analogue of 'replicate' -- -- In CPS style because the @xs@ type parameter is not statically known. exactlyReplicate :: forall a r. Word -> a -> (forall xs. Exactly xs a -> r) -> r exactlyReplicate :: Word -> a -> (forall (xs :: [*]). Exactly xs a -> r) -> r exactlyReplicate = \Word n a a forall (xs :: [*]). Exactly xs a -> r k -> Word -> a -> (forall (xs :: [*]). NP (K a) xs -> r) -> r go Word n a a (Exactly xs a -> r forall (xs :: [*]). Exactly xs a -> r k (Exactly xs a -> r) -> (NP (K a) xs -> Exactly xs a) -> NP (K a) xs -> r forall b c a. (b -> c) -> (a -> b) -> a -> c . NP (K a) xs -> Exactly xs a forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a Exactly) where go :: Word -> a -> (forall xs. NP (K a) xs -> r) -> r go :: Word -> a -> (forall (xs :: [*]). NP (K a) xs -> r) -> r go Word 0 a _ forall (xs :: [*]). NP (K a) xs -> r k = NP (K a) '[] -> r forall (xs :: [*]). NP (K a) xs -> r k NP (K a) '[] forall k (f :: k -> *). NP f '[] Nil go Word n a a forall (xs :: [*]). NP (K a) xs -> r k = Word -> a -> (forall (xs :: [*]). NP (K a) xs -> r) -> r go (Word n Word -> Word -> Word forall a. Num a => a -> a -> a - Word 1) a a ((forall (xs :: [*]). NP (K a) xs -> r) -> r) -> (forall (xs :: [*]). NP (K a) xs -> r) -> r forall a b. (a -> b) -> a -> b $ \NP (K a) xs xs -> NP (K a) (Any : xs) -> r forall (xs :: [*]). NP (K a) xs -> r k (a -> K a Any forall k a (b :: k). a -> K a b K a a K a Any -> NP (K a) xs -> NP (K a) (Any : xs) forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NP f xs -> NP f (x : xs) :* NP (K a) xs xs) {------------------------------------------------------------------------------- Working with 'AtMost' -------------------------------------------------------------------------------} -- | Singleton atMostOne :: a -> AtMost (x ': xs) a atMostOne :: a -> AtMost (x : xs) a atMostOne a x = a -> AtMost xs a -> AtMost (x : xs) a forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a AtMostCons a x AtMost xs a forall (xs :: [*]) a. AtMost xs a AtMostNil -- | Analogue of 'init' -- -- For simplicity we don't shrink the type-level index. atMostInit :: AtMost xs a -> Maybe (AtMost xs a, a) atMostInit :: AtMost xs a -> Maybe (AtMost xs a, a) atMostInit = AtMost xs a -> Maybe (AtMost xs a, a) forall (xs :: [*]) a. AtMost xs a -> Maybe (AtMost xs a, a) go where go :: AtMost xs a -> Maybe (AtMost xs a, a) go :: AtMost xs a -> Maybe (AtMost xs a, a) go AtMost xs a AtMostNil = Maybe (AtMost xs a, a) forall a. Maybe a Nothing go (AtMostCons a a AtMost xs a as) = (AtMost (x : xs) a, a) -> Maybe (AtMost (x : xs) a, a) forall a. a -> Maybe a Just ((AtMost (x : xs) a, a) -> Maybe (AtMost (x : xs) a, a)) -> (AtMost (x : xs) a, a) -> Maybe (AtMost (x : xs) a, a) forall a b. (a -> b) -> a -> b $ case AtMost xs a -> Maybe (AtMost xs a, a) forall (xs :: [*]) a. AtMost xs a -> Maybe (AtMost xs a, a) go AtMost xs a as of Maybe (AtMost xs a, a) Nothing -> (AtMost (x : xs) a forall (xs :: [*]) a. AtMost xs a AtMostNil, a a) Just (AtMost xs a as', a a') -> (a -> AtMost xs a -> AtMost (x : xs) a forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a AtMostCons a a AtMost xs a as', a a') -- | Analogue of 'head' atMostHead :: AtMost xs a -> Maybe a atMostHead :: AtMost xs a -> Maybe a atMostHead AtMost xs a AtMostNil = Maybe a forall a. Maybe a Nothing atMostHead (AtMostCons a x AtMost xs a _) = a -> Maybe a forall a. a -> Maybe a Just a x -- | Analogue of 'last' atMostLast :: AtMost xs a -> Maybe a atMostLast :: AtMost xs a -> Maybe a atMostLast = ((AtMost xs a, a) -> a) -> Maybe (AtMost xs a, a) -> Maybe a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (AtMost xs a, a) -> a forall a b. (a, b) -> b snd (Maybe (AtMost xs a, a) -> Maybe a) -> (AtMost xs a -> Maybe (AtMost xs a, a)) -> AtMost xs a -> Maybe a forall b c a. (b -> c) -> (a -> b) -> a -> c . AtMost xs a -> Maybe (AtMost xs a, a) forall (xs :: [*]) a. AtMost xs a -> Maybe (AtMost xs a, a) atMostInit atMostZipFoldable :: Foldable t => AtMost xs a -> t b -> AtMost xs (a, b) atMostZipFoldable :: AtMost xs a -> t b -> AtMost xs (a, b) atMostZipFoldable = \AtMost xs a as t b bs -> AtMost xs a -> [b] -> AtMost xs (a, b) forall (xs :: [*]) a b. AtMost xs a -> [b] -> AtMost xs (a, b) go AtMost xs a as (t b -> [b] forall (t :: * -> *) a. Foldable t => t a -> [a] Foldable.toList t b bs) where go :: AtMost xs a -> [b] -> AtMost xs (a, b) go :: AtMost xs a -> [b] -> AtMost xs (a, b) go AtMost xs a AtMostNil [b] _ = AtMost xs (a, b) forall (xs :: [*]) a. AtMost xs a AtMostNil go AtMost xs a _ [] = AtMost xs (a, b) forall (xs :: [*]) a. AtMost xs a AtMostNil go (AtMostCons a a AtMost xs a as) (b b:[b] bs) = (a, b) -> AtMost xs (a, b) -> AtMost (x : xs) (a, b) forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a AtMostCons (a a, b b) (AtMost xs a -> [b] -> AtMost xs (a, b) forall (xs :: [*]) a b. AtMost xs a -> [b] -> AtMost xs (a, b) go AtMost xs a as [b] bs) atMostNonEmpty :: AtMost (x ': xs) a -> Maybe (NonEmpty (x ': xs) a) atMostNonEmpty :: AtMost (x : xs) a -> Maybe (NonEmpty (x : xs) a) atMostNonEmpty = \case AtMost (x : xs) a AtMostNil -> Maybe (NonEmpty (x : xs) a) forall a. Maybe a Nothing AtMostCons a x AtMost xs a xs -> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a) forall a. a -> Maybe a Just (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)) -> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a) forall a b. (a -> b) -> a -> b $ a -> AtMost xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> AtMost xs a -> NonEmpty (x : xs) a go a x AtMost xs a xs where go :: a -> AtMost xs a -> NonEmpty (x ': xs) a go :: a -> AtMost xs a -> NonEmpty (x : xs) a go a x AtMost xs a AtMostNil = a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne a x go a x (AtMostCons a y AtMost xs a zs) = a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x (a -> AtMost xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> AtMost xs a -> NonEmpty (x : xs) a go a y AtMost xs a zs) {------------------------------------------------------------------------------- Working with 'NonEmpty' -------------------------------------------------------------------------------} instance IsNonEmpty xs => Applicative (NonEmpty xs) where pure :: a -> NonEmpty xs a pure a x = case Proxy xs -> ProofNonEmpty xs forall a (xs :: [a]) (proxy :: [a] -> *). IsNonEmpty xs => proxy xs -> ProofNonEmpty xs isNonEmpty (Proxy xs forall k (t :: k). Proxy t Proxy @xs) of ProofNonEmpty{} -> a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne a x <*> :: NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b (<*>) = NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b forall (xs' :: [*]) a b. NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b go where go :: NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b go :: NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b go (NonEmptyOne a -> b f) (NonEmptyOne a x) = b -> NonEmpty (x : xs) b forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (a -> b f a x) go (NonEmptyCons a -> b f NonEmpty xs (a -> b) _) (NonEmptyOne a x) = b -> NonEmpty (x : xs) b forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (a -> b f a x) go (NonEmptyOne a -> b f) (NonEmptyCons a x NonEmpty xs a _) = b -> NonEmpty (x : xs) b forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (a -> b f a x) go (NonEmptyCons a -> b f NonEmpty xs (a -> b) fs) (NonEmptyCons a x NonEmpty xs a xs) = b -> NonEmpty xs b -> NonEmpty (x : xs) b forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons (a -> b f a x) (NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b forall (xs' :: [*]) a b. NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b go NonEmpty xs (a -> b) fs NonEmpty xs a NonEmpty xs a xs) -- | Analogue of 'head' nonEmptyHead :: NonEmpty xs a -> a nonEmptyHead :: NonEmpty xs a -> a nonEmptyHead (NonEmptyOne a x) = a x nonEmptyHead (NonEmptyCons a x NonEmpty xs a _) = a x -- | Analogue of 'last' nonEmptyLast :: NonEmpty xs a -> a nonEmptyLast :: NonEmpty xs a -> a nonEmptyLast = (Maybe (NonEmpty xs a), a) -> a forall a b. (a, b) -> b snd ((Maybe (NonEmpty xs a), a) -> a) -> (NonEmpty xs a -> (Maybe (NonEmpty xs a), a)) -> NonEmpty xs a -> a forall b c a. (b -> c) -> (a -> b) -> a -> c . NonEmpty xs a -> (Maybe (NonEmpty xs a), a) forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a) nonEmptyInit -- | Analogue of 'init' nonEmptyInit :: NonEmpty xs a -> (Maybe (NonEmpty xs a), a) nonEmptyInit :: NonEmpty xs a -> (Maybe (NonEmpty xs a), a) nonEmptyInit (NonEmptyOne a x) = (Maybe (NonEmpty xs a) forall a. Maybe a Nothing, a x) nonEmptyInit (NonEmptyCons a x NonEmpty xs a xs) = case NonEmpty xs a -> (Maybe (NonEmpty xs a), a) forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a) nonEmptyInit NonEmpty xs a xs of (Maybe (NonEmpty xs a) Nothing , a final) -> (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a) forall a. a -> Maybe a Just (a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne a x) , a final) (Just NonEmpty xs a xs' , a final) -> (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a) forall a. a -> Maybe a Just (a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x NonEmpty xs a xs') , a final) -- | Build a 'NonEmpty' from a list. Returns 'Nothing' when the list is empty -- or when it's longer than @xs@. nonEmptyFromList :: forall xs a. SListI xs => [a] -> Maybe (NonEmpty xs a) nonEmptyFromList :: [a] -> Maybe (NonEmpty xs a) nonEmptyFromList = SList xs -> [a] -> Maybe (NonEmpty xs a) forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a) go (SListI xs => SList xs forall k (xs :: [k]). SListI xs => SList xs sList @xs) where go :: forall xs'. SList xs' -> [a] -> Maybe (NonEmpty xs' a) go :: SList xs' -> [a] -> Maybe (NonEmpty xs' a) go SList xs' s [a] ys = case (SList xs' s, [a] ys) of (SList xs' SCons, [a y]) -> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a) forall a. a -> Maybe a Just (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)) -> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a) forall a b. (a -> b) -> a -> b $ a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne a y (SList xs' SCons, a y:[a] ys') -> a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a y (NonEmpty xs a -> NonEmpty (x : xs) a) -> Maybe (NonEmpty xs a) -> Maybe (NonEmpty (x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> SList xs -> [a] -> Maybe (NonEmpty xs a) forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a) go SList xs forall k (xs :: [k]). SListI xs => SList xs sList [a] ys' (SList xs' SCons, []) -> Maybe (NonEmpty xs' a) forall a. Maybe a Nothing (SList xs' SNil, [a] _) -> Maybe (NonEmpty xs' a) forall a. Maybe a Nothing -- | Convert a 'NonEmpty' to a list. nonEmptyToList :: forall xs a. NonEmpty xs a -> [a] nonEmptyToList :: NonEmpty xs a -> [a] nonEmptyToList = NonEmpty xs a -> [a] forall (xs' :: [*]). NonEmpty xs' a -> [a] go where go :: forall xs'. NonEmpty xs' a -> [a] go :: NonEmpty xs' a -> [a] go (NonEmptyOne a x) = a x a -> [a] -> [a] forall a. a -> [a] -> [a] : [] go (NonEmptyCons a x NonEmpty xs a xs) = a x a -> [a] -> [a] forall a. a -> [a] -> [a] : NonEmpty xs a -> [a] forall (xs' :: [*]). NonEmpty xs' a -> [a] go NonEmpty xs a xs nonEmptyWeaken :: NonEmpty xs a -> AtMost xs a nonEmptyWeaken :: NonEmpty xs a -> AtMost xs a nonEmptyWeaken = NonEmpty xs a -> AtMost xs a forall (xs :: [*]) a. NonEmpty xs a -> AtMost xs a go where go :: NonEmpty xs a -> AtMost xs a go :: NonEmpty xs a -> AtMost xs a go (NonEmptyOne a x) = a -> AtMost xs a -> AtMost (x : xs) a forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a AtMostCons a x AtMost xs a forall (xs :: [*]) a. AtMost xs a AtMostNil go (NonEmptyCons a x NonEmpty xs a xs) = a -> AtMost xs a -> AtMost (x : xs) a forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a AtMostCons a x (NonEmpty xs a -> AtMost xs a forall (xs :: [*]) a. NonEmpty xs a -> AtMost xs a go NonEmpty xs a xs) -- | A strict prefixes -- -- > nonEmptyStrictPrefixes (fromJust (nonEmptyFromList [1..4])) -- > == [ NonEmptyOne 1 -- > , NonEmptyCons 1 $ NonEmptyOne 2 -- > , NonEmptyCons 1 $ NonEmptyCons 2 $ NonEmptyOne 3 -- > ] nonEmptyStrictPrefixes :: NonEmpty xs a -> [NonEmpty xs a] nonEmptyStrictPrefixes :: NonEmpty xs a -> [NonEmpty xs a] nonEmptyStrictPrefixes = NonEmpty xs a -> [NonEmpty xs a] forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a] go where go :: NonEmpty xs a -> [NonEmpty xs a] go :: NonEmpty xs a -> [NonEmpty xs a] go (NonEmptyOne a _) = [] go (NonEmptyCons a x NonEmpty xs a xs) = a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne a x NonEmpty (x : xs) a -> [NonEmpty (x : xs) a] -> [NonEmpty (x : xs) a] forall a. a -> [a] -> [a] : (NonEmpty xs a -> NonEmpty (x : xs) a) -> [NonEmpty xs a] -> [NonEmpty (x : xs) a] forall a b. (a -> b) -> [a] -> [b] map (a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x) (NonEmpty xs a -> [NonEmpty xs a] forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a] go NonEmpty xs a xs) -- | Apply the specified function to exactly one element nonEmptyMapOne :: forall m xs a. Alternative m => (a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a) nonEmptyMapOne :: (a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a) nonEmptyMapOne a -> m a f = NonEmpty xs a -> m (NonEmpty xs a) forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a) go where go :: NonEmpty xs' a -> m (NonEmpty xs' a) go :: NonEmpty xs' a -> m (NonEmpty xs' a) go (NonEmptyOne a x) = a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (a -> NonEmpty (x : xs) a) -> m a -> m (NonEmpty (x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> m a f a x go (NonEmptyCons a x NonEmpty xs a xs) = [m (NonEmpty (x : xs) a)] -> m (NonEmpty (x : xs) a) forall (t :: * -> *) (f :: * -> *) a. (Foldable t, Alternative f) => t (f a) -> f a Foldable.asum [ (\a x' -> a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x' NonEmpty xs a xs) (a -> NonEmpty (x : xs) a) -> m a -> m (NonEmpty (x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> m a f a x , a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x (NonEmpty xs a -> NonEmpty (x : xs) a) -> m (NonEmpty xs a) -> m (NonEmpty (x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NonEmpty xs a -> m (NonEmpty xs a) forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a) go NonEmpty xs a xs ] -- | Variation on 'nonEmptyMapOne' where we try to apply the function to -- /pairs/ of elements nonEmptyMapTwo :: forall m xs a. Alternative m => (a -> m a) -- Used when we reached the end of the list -> (a -> a -> m (a, a)) -> NonEmpty xs a -> m (NonEmpty xs a) nonEmptyMapTwo :: (a -> m a) -> (a -> a -> m (a, a)) -> NonEmpty xs a -> m (NonEmpty xs a) nonEmptyMapTwo a -> m a f a -> a -> m (a, a) g = NonEmpty xs a -> m (NonEmpty xs a) forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a) go where go :: NonEmpty xs' a -> m (NonEmpty xs' a) go :: NonEmpty xs' a -> m (NonEmpty xs' a) go (NonEmptyOne a x) = a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne (a -> NonEmpty (x : xs) a) -> m a -> m (NonEmpty (x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> m a f a x go (NonEmptyCons a x xs :: NonEmpty xs a xs@(NonEmptyOne a y)) = [m (NonEmpty (x : x : xs) a)] -> m (NonEmpty (x : x : xs) a) forall (t :: * -> *) (f :: * -> *) a. (Foldable t, Alternative f) => t (f a) -> f a Foldable.asum [ (\(a x', a y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x' (a -> NonEmpty (x : xs) a forall a x (xs :: [*]). a -> NonEmpty (x : xs) a NonEmptyOne a y')) ((a, a) -> NonEmpty (x : x : xs) a) -> m (a, a) -> m (NonEmpty (x : x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> a -> m (a, a) g a x a y , a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x (NonEmpty xs a -> NonEmpty (x : xs) a) -> m (NonEmpty xs a) -> m (NonEmpty (x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NonEmpty xs a -> m (NonEmpty xs a) forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a) go NonEmpty xs a xs ] go (NonEmptyCons a x xs :: NonEmpty xs a xs@(NonEmptyCons a y NonEmpty xs a zs)) = [m (NonEmpty (x : x : xs) a)] -> m (NonEmpty (x : x : xs) a) forall (t :: * -> *) (f :: * -> *) a. (Foldable t, Alternative f) => t (f a) -> f a Foldable.asum [ (\(a x', a y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x' (a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a y' NonEmpty xs a zs)) ((a, a) -> NonEmpty (x : x : xs) a) -> m (a, a) -> m (NonEmpty (x : x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> a -> a -> m (a, a) g a x a y , a -> NonEmpty xs a -> NonEmpty (x : xs) a forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a NonEmptyCons a x (NonEmpty xs a -> NonEmpty (x : xs) a) -> m (NonEmpty xs a) -> m (NonEmpty (x : xs) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> NonEmpty xs a -> m (NonEmpty xs a) forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a) go NonEmpty xs a xs ]