-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Sized sequence data-types -- -- A wrapper to make length-parametrized data-type from ListLike -- data-types. @package sized @version 0.2.0.0 -- | This module provides the functionality to make length-parametrized -- types from existing ListLike and Functor sequential -- types. -- -- Most of the complexity of operations for Sized f n a are the -- same as original operations for f. For example, !! is -- O(1) for Sized Vector n a but O(i) for Sized [] n a. -- -- This module also provides powerful view types and pattern synonyms to -- inspect the sized sequence. See Views and Patterns for more -- detail. module Data.Sized -- | Sized wraps a sequential type f and makes -- length-parametrized version. -- -- Here, f must be the instance of Functor and -- ListLike (f a) a for all a. This constraint -- is expressed by ListLikeF. Folding and traversing function such -- as all and foldl' is available via Foldable or -- Traversable class, if f is the instance of them. -- -- Since 0.2.0.0 data Sized (f :: Type -> Type) (n :: nat) a -- | Sized vector with the length is existentially quantified. This -- type is used mostly when the return type's length cannot be statically -- determined beforehand. -- -- SomeSized sn xs :: SomeSized f a stands for the Sized -- sequence xs of element type a and length -- sn. -- -- Since 0.1.0.0 data SomeSized f nat a [SomeSized] :: (ListLike (f a) a) => Sing n -> Sized f (n :: nat) a -> SomeSized f nat a instLL :: forall f a. ListLikeF f :- ListLike (f a) a instFunctor :: ListLikeF f :- Functor f -- | Functor f such that there is instance ListLike (f a) -- a for any a. -- -- Since 0.1.0.0 type ListLikeF f = (Functor f, Forall (LLF f)) withListLikeF :: forall pxy f a b. ListLikeF f => pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b withListLikeF' :: ListLikeF f => f a -> ((Functor f, ListLike (f a) a) => b) -> b -- | Returns the length of wrapped containers. If you use -- unsafeFromList or similar unsafe functions, this function may -- return different value from type-parameterized length. -- -- Since 0.1.0.0 length :: ListLike (f a) a => Sized f n a -> Int -- | Sing version of length. -- -- Since 0.2.0.0 sLength :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> Sing n -- | Test if the sequence is empty or not. -- -- Since 0.1.0.0 null :: ListLike (f a) a => Sized f n a -> Bool -- | (Unsafe) indexing with Ints. If you want to check boundary -- statically, use %!! or sIndex. -- -- Since 0.1.0.0 (!!) :: (ListLike (f a) a) => Sized f (Succ m) a -> Int -> a -- | Safe indexing with Ordinals. -- -- Since 0.1.0.0 (%!!) :: (HasOrdinal nat, ListLike (f c) c) => Sized f n c -> Ordinal (n :: nat) -> c -- | Flipped version of !!. -- -- Since 0.1.0.0 index :: (ListLike (f a) a) => Int -> Sized f (Succ m) a -> a -- | Flipped version of %!!. -- -- Since 0.1.0.0 sIndex :: (HasOrdinal nat, ListLike (f c) c) => Ordinal (n :: nat) -> Sized f n c -> c -- | Take the first element of non-empty sequence. If you want to make -- case-analysis for general sequence, see Views and Patterns -- section. -- -- Since 0.1.0.0 head :: (HasOrdinal nat, ListLike (f a) b, (Zero nat :< n) ~ True) => Sized f n a -> b -- | Take the last element of non-empty sequence. If you want to make -- case-analysis for general sequence, see Views and Patterns -- section. -- -- Since 0.1.0.0 last :: (HasOrdinal nat, (Zero nat :< n) ~ True, ListLike (f a) b) => Sized f n a -> b -- | Take the head and tail of non-empty sequence. If you -- want to make case-analysis for general sequence, see Views and -- Patterns section. -- -- Since 0.1.0.0 uncons :: ListLike (f a) b => Sized f (Succ n) a -> (b, Sized f n a) uncons' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (b, Sized f n a) -- | Take the init and last of non-empty sequence. If you -- want to make case-analysis for general sequence, see Views and -- Patterns section. -- -- Since 0.1.0.0 unsnoc :: ListLike (f a) b => Sized f (Succ n) a -> (Sized f n a, b) unsnoc' :: ListLike (f a) b => proxy n -> Sized f (Succ n) a -> (Sized f n a, b) -- | Take the tail of non-empty sequence. If you want to make case-analysis -- for general sequence, see Views and Patterns section. -- -- Since 0.1.0.0 tail :: (HasOrdinal nat, ListLike (f a) a) => Sized f (Succ n) a -> Sized f (n :: nat) a -- | Take the initial segment of non-empty sequence. If you want to make -- case-analysis for general sequence, see Views and Patterns -- section. -- -- Since 0.1.0.0 init :: ListLike (f a) a => Sized f (Succ n) a -> Sized f n a -- | take k xs takes first k element of xs where -- the length of xs should be larger than k. It is -- really sad, that this function takes at least O(k) regardless of base -- container. -- -- Since 0.1.0.0 take :: (ListLike (f a) a, (n :<= m) ~ True, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> Sized f n a -- | take k xs takes first k element of xs at -- most. It is really sad, that this function takes at least O(k) -- regardless of base container. -- -- Since 0.1.0.0 takeAtMost :: (ListLike (f a) a, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> Sized f (Min n m) a -- | drop k xs drops first k element of xs and -- returns the rest of sequence, where the length of xs should -- be larger than k. It is really sad, that this function takes -- at least O(k) regardless of base container. -- -- Since 0.1.0.0 drop :: (HasOrdinal nat, ListLike (f a) a, (n :<= m) ~ True) => Sing (n :: nat) -> Sized f m a -> Sized f (m :- n) a -- | splitAt k xs split xs at k, where the -- length of xs should be less than or equal to k. It -- is really sad, that this function takes at least O(k) regardless of -- base container. -- -- Since 0.1.0.0 splitAt :: (ListLike (f a) a, (n :<= m) ~ True, HasOrdinal nat) => Sing (n :: nat) -> Sized f m a -> (Sized f n a, Sized f (m :-. n) a) -- | splitAtMost k xs split xs at k. If -- k exceeds the length of xs, then the second result -- value become empty. It is really sad, that this function takes at -- least O(k) regardless of base container. -- -- Since 0.1.0.0 splitAtMost :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> Sized f m a -> (Sized f (Min n m) a, Sized f (m :-. n) a) -- | Empty sequence. -- -- Since 0.1.0.0 empty :: forall f a. (HasOrdinal nat, ListLike (f a) a) => Sized f (Zero nat :: nat) a -- | Sequence with one element. -- -- Since 0.1.0.0 singleton :: forall f a. ListLike (f a) a => a -> Sized f 1 a -- | Consruct the Sized sequence from base type, but the length -- parameter is dynamically determined and existentially quantified; see -- also SomeSized. -- -- Since 0.1.0.0 toSomeSized :: forall nat f a. (HasOrdinal nat, ListLike (f a) a) => f a -> SomeSized f nat a -- | Replicates the same value. -- -- Since 0.1.0.0 replicate :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sing n -> a -> Sized f n a -- | replicate with the length inferred. -- -- Since 0.1.0.0 replicate' :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => a -> Sized f n a -- | Append an element to the head of sequence. -- -- Since 0.1.0.0 cons :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a -- | Infix version of cons. -- -- Since 0.1.0.0 (<|) :: (ListLike (f a) b) => b -> Sized f n a -> Sized f (Succ n) a infixr 5 <| -- | Append an element to the tail of sequence. -- -- Since 0.1.0.0 snoc :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a -- | Infix version of snoc. -- -- Since 0.1.0.0 (|>) :: (ListLike (f a) b) => Sized f n a -> b -> Sized f (Succ n) a infixl 5 |> -- | Append two lists. -- -- Since 0.1.0.0 append :: ListLike (f a) a => Sized f n a -> Sized f m a -> Sized f (n :+ m) a -- | Infix version of append. -- -- Since 0.1.0.0 (++) :: (ListLike (f a) a) => Sized f n a -> Sized f m a -> Sized f (n :+ m) a infixr 5 ++ -- | Concatenates multiple sequences into one. -- -- Since 0.1.0.0 concat :: forall f f' m n a. (Functor f', Foldable f', ListLike (f a) a) => Sized f' m (Sized f n a) -> Sized f (m :* n) a -- | Zipping two sequences. Length is adjusted to shorter one. -- -- Since 0.1.0.0 zip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b) -- | zip for the sequences of the same length. -- -- Since 0.1.0.0 zipSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) => Sized f n a -> Sized f n b -> Sized f n (a, b) -- | Zipping two sequences with funtion. Length is adjusted to shorter one. -- -- Since 0.1.0.0 zipWith :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c -- | zipWith for the sequences of the same length. -- -- Since 0.1.0.0 zipWithSame :: (ListLike (f a) a, ListLike (f b) b, ListLike (f c) c) => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c -- | Unzipping the sequence of tuples. -- -- Since 0.1.0.0 unzip :: (ListLike (f a) a, ListLike (f b) b, ListLike (f (a, b)) (a, b)) => Sized f n (a, b) -> (Sized f n a, Sized f n b) -- | Map function. -- -- Since 0.1.0.0 map :: (ListLike (f a) a, ListLike (f b) b) => (a -> b) -> Sized f n a -> Sized f n b fmap :: forall f n a b. Functor f => (a -> b) -> Sized f n a -> Sized f n b -- | Reverse function. -- -- Since 0.1.0.0 reverse :: ListLike (f a) a => Sized f n a -> Sized f n a -- | Intersperces. -- -- Since 0.1.0.0 intersperse :: ListLike (f a) a => a -> Sized f n a -> Sized f ((FromInteger 2 :* n) :-. 1) a -- | Remove all duplicates. -- -- Since 0.1.0.0 nub :: (HasOrdinal nat, ListLike (f a) a, Eq a) => Sized f n a -> SomeSized f nat a -- | Sorting sequence by ascending order. -- -- Since 0.1.0.0 sort :: (ListLike (f a) a, Ord a) => Sized f n a -> Sized f n a -- | Generalized version of sort. -- -- Since 0.1.0.0 sortBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> Sized f n a -> Sized f n a -- | Insert new element into the presorted sequence. -- -- Since 0.1.0.0 insert :: (ListLike (f a) a, Ord a) => a -> Sized f n a -> Sized f (Succ n) a -- | Generalized version of insert. -- -- Since 0.1.0.0 insertBy :: (ListLike (f a) a) => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a -- | Convert to list. -- -- Since 0.1.0.0 toList :: ListLike (f a) a => Sized f n a -> [a] -- | If the given list is shorter than n, then returns -- Nothing Otherwise returns Sized f n a consisting of -- initial n element of given list. -- -- Since 0.1.0.0 fromList :: forall f n a. (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> [a] -> Maybe (Sized f n a) -- | fromList with the result length inferred. -- -- Since 0.1.0.0 fromList' :: (ListLike (f a) a, SingI (n :: Nat)) => [a] -> Maybe (Sized f n a) -- | Unsafe version of fromList. If the length of the given list -- does not equal to n, then something unusual happens. -- -- Since 0.1.0.0 unsafeFromList :: forall f n a. ListLike (f a) a => Sing n -> [a] -> Sized f n a -- | unsafeFromList with the result length inferred. -- -- Since 0.1.0.0 unsafeFromList' :: (SingI (n :: Nat), ListLike (f a) a) => [a] -> Sized f n a -- | Construct a Sized f n a by padding default value if the given -- list is short. -- -- Since 0.1.0.0 fromListWithDefault :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sing n -> a -> [a] -> Sized f n a -- | fromListWithDefault with the result length inferred. -- -- Since 0.1.0.0 fromListWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> [a] -> Sized f n a -- | Forget the length and obtain the wrapped base container. -- -- Since 0.1.0.0 unsized :: Sized f n a -> f a -- | If the length of the input is shorter than n, then returns -- Nothing. Otherwise returns Sized f n a consisting of -- initial n element of the input. -- -- Since 0.1.0.0 toSized :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> f a -> Maybe (Sized f n a) -- | toSized with the result length inferred. -- -- Since 0.1.0.0 toSized' :: (ListLike (f a) a, SingI (n :: Nat)) => f a -> Maybe (Sized f n a) -- | Unsafe version of toSized. If the length of the given list does -- not equal to n, then something unusual happens. -- -- Since 0.1.0.0 unsafeToSized :: Sing n -> f a -> Sized f n a -- | unsafeToSized with the result length inferred. -- -- Since 0.1.0.0 unsafeToSized' :: (SingI (n :: Nat), ListLike (f a) a) => f a -> Sized f n a -- | Construct a Sized f n a by padding default value if the given -- list is short. -- -- Since 0.1.0.0 toSizedWithDefault :: (HasOrdinal nat, ListLike (f a) a) => Sing (n :: nat) -> a -> f a -> Sized f n a -- | toSizedWithDefault with the result length inferred. -- -- Since 0.1.0.0 toSizedWithDefault' :: (SingI (n :: Nat), ListLike (f a) a) => a -> f a -> Sized f n a -- | The type Partitioned f n a represents partitioned sequence of -- length n. Value Partitioned lenL ls lenR rs stands -- for: -- -- -- -- Since 0.1.0.0 data Partitioned f n a [Partitioned] :: (ListLike (f a) a) => Sing n -> Sized f (n :: Nat) a -> Sing m -> Sized f (m :: Nat) a -> Partitioned f (n :+ m) a -- | Take the initial segment as long as elements satisfys the predicate. -- -- Since 0.1.0.0 takeWhile :: (HasOrdinal nat, ListLike (f a) a) => (a -> Bool) -> Sized f n a -> SomeSized f nat a -- | Drop the initial segment as long as elements satisfys the predicate. -- -- Since 0.1.0.0 dropWhile :: (HasOrdinal nat, ListLike (f a) a) => (a -> Bool) -> Sized f n a -> SomeSized f nat a -- | Invariant: ListLike (f a) a instance must be -- implemented to satisfy the following property: length (fst (span p -- xs)) + length (snd (span p xs)) == length xs Otherwise, this -- function introduces severe contradiction. -- -- Since 0.1.0.0 span :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a -- | Invariant: ListLike (f a) a instance must be -- implemented to satisfy the following property: length (fst (break -- p xs)) + length (snd (break p xs)) == length xs Otherwise, this -- function introduces severe contradiction. -- -- Since 0.1.0.0 break :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a -- | Invariant: ListLike (f a) a instance must be -- implemented to satisfy the following property: length (fst -- (partition p xs)) + length (snd (partition p xs)) == length xs -- Otherwise, this function introduces severe contradiction. -- -- Since 0.1.0.0 partition :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Partitioned f n a -- | Membership test; see also notElem. -- -- Since 0.1.0.0 elem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool -- | Negation of elem. -- -- Since 0.1.0.0 notElem :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> Bool -- | Find the element satisfying the predicate. -- -- Since 0.1.0.0 find :: Foldable f => (a -> Bool) -> Sized f n a -> Maybe a -- | Foldable version of find. findF :: (Foldable f) => (a -> Bool) -> Sized f n a -> Maybe a -- | findIndex p xs find the element satisfying p -- and returns its index if exists. -- -- Since 0.1.0.0 findIndex :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> Maybe Int -- | findIndex implemented in terms of -- FoldableWithIndex findIndexIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> Maybe i -- | Ordinal version of findIndex. -- -- Since 0.1.0.0 sFindIndex :: (SingI (n :: nat), ListLike (f a) a, HasOrdinal nat) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n) -- | sFindIndex implemented in terms of -- FoldableWithIndex sFindIndexIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> Maybe (Ordinal n) -- | findIndices p xs find all elements satisfying -- p and returns their indices. -- -- Since 0.1.0.0 findIndices :: ListLike (f a) a => (a -> Bool) -> Sized f n a -> [Int] -- | findIndices implemented in terms of -- FoldableWithIndex findIndicesIF :: (FoldableWithIndex i f) => (a -> Bool) -> Sized f n a -> [i] -- | Ordinal version of findIndices. -- -- Since 0.1.0.0 sFindIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a) => (a -> Bool) -> Sized f n a -> [Ordinal n] sFindIndicesIF :: (FoldableWithIndex i f, Integral i, HasOrdinal nat, SingI n) => (a -> Bool) -> Sized f (n :: nat) a -> [Ordinal n] -- | Returns the index of the given element in the list, if exists. -- -- Since 0.1.0.0 elemIndex :: (Eq a, ListLike (f a) a) => a -> Sized f n a -> Maybe Int -- | Ordinal version of elemIndex It statically checks boundary -- invariants. If you don't internal structure on Sized, -- then sUnsafeElemIndex is much faster and also safe for -- most cases. -- -- Since 0.1.0.0 sElemIndex :: forall (n :: nat) f a. (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n) sUnsafeElemIndex :: forall (n :: nat) f a. (SingI n, ListLike (f a) a, Eq a, HasOrdinal nat) => a -> Sized f n a -> Maybe (Ordinal n) -- | Returns all indices of the given element in the list. -- -- Since 0.1.0.0 elemIndices :: (ListLike (f a) a, Eq a) => a -> Sized f n a -> [Int] -- | Ordinal version of elemIndices -- -- Since 0.1.0.0 sElemIndices :: (HasOrdinal nat, SingI (n :: nat), ListLike (f a) a, Eq a) => a -> Sized f n a -> [Ordinal n] -- | Case analysis for the cons-side of sequence. -- -- Since 0.1.0.0 viewCons :: forall f a (n :: nat). (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> ConsView f n a -- | View of the left end of sequence (cons-side). -- -- Since 0.1.0.0 data ConsView f n a [NilCV] :: ConsView f (Zero nat) a [::-] :: SingI n => a -> Sized f n a -> ConsView f (Succ n) a -- | Case analysis for the snoc-side of sequence. -- -- Since 0.1.0.0 viewSnoc :: forall f (n :: nat) a. (HasOrdinal nat, ListLike (f a) a) => Sized f n a -> SnocView f n a -- | View of the left end of sequence (snoc-side). -- -- Since 0.1.0.0 data SnocView f n a [NilSV] :: SnocView f (Zero nat) a [:-::] :: SingI n => Sized f n a -> a -> SnocView f (Succ n) a -- | Pattern synonym for cons-side uncons. infixr 5 :< infixl 5 :> instance GHC.Show.Show (f a) => GHC.Show.Show (Data.Sized.SomeSized f nat a) instance GHC.Classes.Eq (f a) => GHC.Classes.Eq (Data.Sized.SomeSized f nat a) instance forall k (nat :: k) (f :: * -> *) nat1 (n :: nat1). (GHC.Base.Functor f, Data.Type.Ordinal.HasOrdinal nat1, Data.Singletons.SingI n, Data.Sized.Internal.ListLikeF f) => GHC.Base.Applicative (Data.Sized.Internal.Sized f n) -- | This module exports Sized type specialized to GHC's -- built-in type numeral Nat. module Data.Sized.Builtin type Ordinal (n :: Nat) = Ordinal n type Sized f (n :: Nat) = Sized f n infixr 5 :< infixl 5 :> module Data.Sized.Flipped -- | Wrapper for Sized which takes length as its last -- element, instead of the second. -- -- Since 0.2.0.0 newtype Flipped f a n Flipped :: Sized f n a -> Flipped f a n [runFlipped] :: Flipped f a n -> Sized f n a instance forall (f :: GHC.Types.Type -> *) a nat (n :: nat). Data.MonoTraversable.MonoFunctor (f a) => Data.MonoTraversable.MonoFunctor (Data.Sized.Flipped.Flipped f a n) instance forall (f :: GHC.Types.Type -> *) a nat (n :: nat). Data.MonoTraversable.MonoFoldable (f a) => Data.MonoTraversable.MonoFoldable (Data.Sized.Flipped.Flipped f a n) instance forall nat nat1 (f0 :: GHC.Types.Type -> GHC.Types.Type) a0 (n0 :: nat1) t0 (f1 :: GHC.Types.Type -> GHC.Types.Type) a1 (n1 :: nat). Data.Sized.Flipped.Flipped f0 a0 n0 ~ t0 => Control.Lens.Wrapped.Rewrapped (Data.Sized.Flipped.Flipped f1 a1 n1) t0 instance forall nat (f0 :: GHC.Types.Type -> GHC.Types.Type) a0 (n0 :: nat). Control.Lens.Wrapped.Wrapped (Data.Sized.Flipped.Flipped f0 a0 n0) instance forall nat (f :: GHC.Types.Type -> *) a (n :: nat). Data.MonoTraversable.MonoTraversable (f a) => Data.MonoTraversable.MonoTraversable (Data.Sized.Flipped.Flipped f a n) instance forall k (nat :: k) (f :: GHC.Types.Type -> GHC.Types.*) a nat1 (n :: nat1). (GHC.Real.Integral (Control.Lens.At.Index (f a)), Control.Lens.At.Ixed (f a), Data.Type.Ordinal.HasOrdinal nat1) => Control.Lens.At.Ixed (Data.Sized.Flipped.Flipped f a n) instance forall (f :: GHC.Types.Type -> GHC.Types.Type) a nat (n :: nat). Data.Hashable.Class.Hashable (f a) => Data.Hashable.Class.Hashable (Data.Sized.Flipped.Flipped f a n) instance forall (f :: GHC.Types.Type -> GHC.Types.Type) a nat (n :: nat). Control.DeepSeq.NFData (f a) => Control.DeepSeq.NFData (Data.Sized.Flipped.Flipped f a n) instance forall (f :: GHC.Types.Type -> GHC.Types.Type) a nat (n :: nat). GHC.Classes.Ord (f a) => GHC.Classes.Ord (Data.Sized.Flipped.Flipped f a n) instance forall (f :: GHC.Types.Type -> GHC.Types.Type) a nat (n :: nat). GHC.Classes.Eq (f a) => GHC.Classes.Eq (Data.Sized.Flipped.Flipped f a n) instance forall (f :: GHC.Types.Type -> GHC.Types.Type) a nat (n :: nat). GHC.Show.Show (f a) => GHC.Show.Show (Data.Sized.Flipped.Flipped f a n) -- | This module exports Sized type specialized to -- type-level Peano numeral Nat. module Data.Sized.Peano type Ordinal (n :: Nat) = Ordinal n type Sized f (n :: Nat) = Sized f n infixr 5 :< infixl 5 :>