Safe Haskell	Safe-Inferred
Language	Haskell2010

Morley.Util.SizedList.Types

Contents

Base types
Utility type synonyms

Description

This module re-exports types from Morley.Util.SizedList

Since Morley.Util.SizedList is intended to be imported qualified, this module provides a convenient way to import only types, which are unlinkely to be ambiguous.

Synopsis

type SizedList (n :: Nat) a = SizedList' (ToPeano n) a
data SizedList' (n :: Peano) a where
- Nil :: SizedList' 'Z a
- (:<) :: ~a -> ~(SizedList' n a) -> SizedList' ('S n) a
- pattern (::<) :: a -> SizedList' n a -> SizedList' ('S n) a
- pattern Nil' :: SizedList' 'Z a
data SomeSizedList a where
- SomeSizedList :: SingNat n -> SizedList' n a -> SomeSizedList a
type SingIPeano (n :: Nat) = SingI (ToPeano n)
type IsoNatPeano (n :: Nat) (p :: Peano) = (n ~ FromPeano p, ToPeano n ~ p)

Base types

type SizedList (n :: Nat) a = SizedList' (ToPeano n) a Source #

The primary fixed-size list type. Parametrized by a type-level Nat as length and type as element type.

Internally powered by Peano numbers

data SizedList' (n :: Peano) a where Source #

Actual fixed-size list GADT, parametrized by Peano natural. You generally don't want to use this directly, since Peano is not very ergonomic. Prefer using SizedList unless writing utility functions that need to do type-level arithmetic.

Note that while this has the usual instances, Applicative and Monad are not the same as for regular lists: they implement "zipper" semantics, i.e. f <*> x is the same as zipWith ($) f x

Constructors

Nil
Fields :: SizedList' 'Z a Empty list
(:<) infixr 5
Fields :: ~a -> ~(SizedList' n a) -> SizedList' ('S n) a Cons

Bundled Patterns

pattern (::<) :: a -> SizedList' n a -> SizedList' ('S n) a infixr 5

Sized list cons pattern. Unlike :< this pattern can be used to auto-deduce the type of the result, e.g.

>>> a ::< b ::< c ::< Nil' = pure 'a'
>>> (a, b, c)
('a','a','a')

pattern Nil' :: SizedList' 'Z a

Sized list Nil pattern. Unlike Nil this pattern can be used to auto-deduce the type of the result, see ::<.

Instances

Instances details

Foldable (SizedList' n) Source #
Instance details Defined in Morley.Util.SizedList Methods fold :: Monoid m => SizedList' n m -> m # foldMap :: Monoid m => (a -> m) -> SizedList' n a -> m # foldMap' :: Monoid m => (a -> m) -> SizedList' n a -> m # foldr :: (a -> b -> b) -> b -> SizedList' n a -> b # foldr' :: (a -> b -> b) -> b -> SizedList' n a -> b # foldl :: (b -> a -> b) -> b -> SizedList' n a -> b # foldl' :: (b -> a -> b) -> b -> SizedList' n a -> b # foldr1 :: (a -> a -> a) -> SizedList' n a -> a # foldl1 :: (a -> a -> a) -> SizedList' n a -> a # toList :: SizedList' n a -> [a] # null :: SizedList' n a -> Bool # length :: SizedList' n a -> Int # elem :: Eq a => a -> SizedList' n a -> Bool # maximum :: Ord a => SizedList' n a -> a # minimum :: Ord a => SizedList' n a -> a # sum :: Num a => SizedList' n a -> a # product :: Num a => SizedList' n a -> a #
Traversable (SizedList' n) Source #
Instance details Defined in Morley.Util.SizedList Methods traverse :: Applicative f => (a -> f b) -> SizedList' n a -> f (SizedList' n b) # sequenceA :: Applicative f => SizedList' n (f a) -> f (SizedList' n a) # mapM :: Monad m => (a -> m b) -> SizedList' n a -> m (SizedList' n b) # sequence :: Monad m => SizedList' n (m a) -> m (SizedList' n a) #
SingI n => Applicative (SizedList' n) Source #
Instance details Defined in Morley.Util.SizedList Methods pure :: a -> SizedList' n a # (<>) :: SizedList' n (a -> b) -> SizedList' n a -> SizedList' n b # liftA2 :: (a -> b -> c) -> SizedList' n a -> SizedList' n b -> SizedList' n c # (>) :: SizedList' n a -> SizedList' n b -> SizedList' n b # (<*) :: SizedList' n a -> SizedList' n b -> SizedList' n a #
Functor (SizedList' n) Source #
Instance details Defined in Morley.Util.SizedList Methods fmap :: (a -> b) -> SizedList' n a -> SizedList' n b # (<$) :: a -> SizedList' n b -> SizedList' n a #
SingI n => Monad (SizedList' n) Source #
Instance details Defined in Morley.Util.SizedList Methods (>>=) :: SizedList' n a -> (a -> SizedList' n b) -> SizedList' n b # (>>) :: SizedList' n a -> SizedList' n b -> SizedList' n b # return :: a -> SizedList' n a #
Show a => Show (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList Methods showsPrec :: Int -> SizedList' n a -> ShowS # show :: SizedList' n a -> String # showList :: [SizedList' n a] -> ShowS #
Eq a => Eq (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList Methods (==) :: SizedList' n a -> SizedList' n a -> Bool # (/=) :: SizedList' n a -> SizedList' n a -> Bool #
Ord a => Ord (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList Methods compare :: SizedList' n a -> SizedList' n a -> Ordering # (<) :: SizedList' n a -> SizedList' n a -> Bool # (<=) :: SizedList' n a -> SizedList' n a -> Bool # (>) :: SizedList' n a -> SizedList' n a -> Bool # (>=) :: SizedList' n a -> SizedList' n a -> Bool # max :: SizedList' n a -> SizedList' n a -> SizedList' n a # min :: SizedList' n a -> SizedList' n a -> SizedList' n a #
Ord k => ToBigMap (SizedList' n (k, v)) Source #
Instance details Defined in Morley.Michelson.Typed.Haskell.Value Associated Types type ToBigMapKey (SizedList' n (k, v)) Source # type ToBigMapValue (SizedList' n (k, v)) Source # Methods mkBigMap :: SizedList' n (k, v) -> BigMap (ToBigMapKey (SizedList' n (k, v))) (ToBigMapValue (SizedList' n (k, v))) Source #
Buildable a => Buildable (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList Methods build :: SizedList' n a -> Doc buildList :: [SizedList' n a] -> Doc
Container (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList Associated Types type Element (SizedList' n a) # Methods toList :: SizedList' n a -> [Element (SizedList' n a)] # null :: SizedList' n a -> Bool # foldr :: (Element (SizedList' n a) -> b -> b) -> b -> SizedList' n a -> b # foldl :: (b -> Element (SizedList' n a) -> b) -> b -> SizedList' n a -> b # foldl' :: (b -> Element (SizedList' n a) -> b) -> b -> SizedList' n a -> b # length :: SizedList' n a -> Int # elem :: Element (SizedList' n a) -> SizedList' n a -> Bool # foldMap :: Monoid m => (Element (SizedList' n a) -> m) -> SizedList' n a -> m # fold :: SizedList' n a -> Element (SizedList' n a) # foldr' :: (Element (SizedList' n a) -> b -> b) -> b -> SizedList' n a -> b # notElem :: Element (SizedList' n a) -> SizedList' n a -> Bool # all :: (Element (SizedList' n a) -> Bool) -> SizedList' n a -> Bool # any :: (Element (SizedList' n a) -> Bool) -> SizedList' n a -> Bool # and :: SizedList' n a -> Bool # or :: SizedList' n a -> Bool # find :: (Element (SizedList' n a) -> Bool) -> SizedList' n a -> Maybe (Element (SizedList' n a)) # safeHead :: SizedList' n a -> Maybe (Element (SizedList' n a)) # safeMaximum :: SizedList' n a -> Maybe (Element (SizedList' n a)) # safeMinimum :: SizedList' n a -> Maybe (Element (SizedList' n a)) # safeFoldr1 :: (Element (SizedList' n a) -> Element (SizedList' n a) -> Element (SizedList' n a)) -> SizedList' n a -> Maybe (Element (SizedList' n a)) # safeFoldl1 :: (Element (SizedList' n a) -> Element (SizedList' n a) -> Element (SizedList' n a)) -> SizedList' n a -> Maybe (Element (SizedList' n a)) #
n ~ 'S 'Z => One (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList Associated Types type OneItem (SizedList' n a) # Methods one :: OneItem (SizedList' n a) -> SizedList' n a #
type ToBigMapKey (SizedList' n (k, v)) Source #
Instance details Defined in Morley.Michelson.Typed.Haskell.Value type ToBigMapKey (SizedList' n (k, v)) = k
type ToBigMapValue (SizedList' n (k, v)) Source #
Instance details Defined in Morley.Michelson.Typed.Haskell.Value type ToBigMapValue (SizedList' n (k, v)) = v
type Element (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList type Element (SizedList' n a) = ElementDefault (SizedList' n a)
type OneItem (SizedList' n a) Source #
Instance details Defined in Morley.Util.SizedList type OneItem (SizedList' n a) = a

data SomeSizedList a where Source #

Existential capturing a fixed-size list whose length is only known at runtime.

In most cases, it's probably better to use regular lists, but this can be occasionally useful.

We do not provide the Applicative and Monad instances, since "zipper" applicative is ill-defined for lists of different length, and having inconsistent instances between this and SizedList is more confusing than useful.

Unlike regular sized list, SomeSizedList is a Semigroup and a Monoid:

>>> fromList "ab" <> fromList "de" <> mempty :: SomeSizedList Char
SomeSizedList (SS (SS (SS (SS SZ)))) ('a' :< 'b' :< 'd' :< 'e' :< Nil)

Constructors

SomeSizedList :: SingNat n -> SizedList' n a -> SomeSizedList a

Instances

Instances details

Foldable SomeSizedList Source #
Instance details Defined in Morley.Util.SizedList Methods fold :: Monoid m => SomeSizedList m -> m # foldMap :: Monoid m => (a -> m) -> SomeSizedList a -> m # foldMap' :: Monoid m => (a -> m) -> SomeSizedList a -> m # foldr :: (a -> b -> b) -> b -> SomeSizedList a -> b # foldr' :: (a -> b -> b) -> b -> SomeSizedList a -> b # foldl :: (b -> a -> b) -> b -> SomeSizedList a -> b # foldl' :: (b -> a -> b) -> b -> SomeSizedList a -> b # foldr1 :: (a -> a -> a) -> SomeSizedList a -> a # foldl1 :: (a -> a -> a) -> SomeSizedList a -> a # toList :: SomeSizedList a -> [a] # null :: SomeSizedList a -> Bool # length :: SomeSizedList a -> Int # elem :: Eq a => a -> SomeSizedList a -> Bool # maximum :: Ord a => SomeSizedList a -> a # minimum :: Ord a => SomeSizedList a -> a # sum :: Num a => SomeSizedList a -> a # product :: Num a => SomeSizedList a -> a #
Traversable SomeSizedList Source #
Instance details Defined in Morley.Util.SizedList Methods traverse :: Applicative f => (a -> f b) -> SomeSizedList a -> f (SomeSizedList b) # sequenceA :: Applicative f => SomeSizedList (f a) -> f (SomeSizedList a) # mapM :: Monad m => (a -> m b) -> SomeSizedList a -> m (SomeSizedList b) # sequence :: Monad m => SomeSizedList (m a) -> m (SomeSizedList a) #
Functor SomeSizedList Source #
Instance details Defined in Morley.Util.SizedList Methods fmap :: (a -> b) -> SomeSizedList a -> SomeSizedList b # (<$) :: a -> SomeSizedList b -> SomeSizedList a #
Monoid (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList Methods mempty :: SomeSizedList a # mappend :: SomeSizedList a -> SomeSizedList a -> SomeSizedList a # mconcat :: [SomeSizedList a] -> SomeSizedList a #
Semigroup (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList Methods (<>) :: SomeSizedList a -> SomeSizedList a -> SomeSizedList a # sconcat :: NonEmpty (SomeSizedList a) -> SomeSizedList a # stimes :: Integral b => b -> SomeSizedList a -> SomeSizedList a #
Show a => Show (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList Methods showsPrec :: Int -> SomeSizedList a -> ShowS # show :: SomeSizedList a -> String # showList :: [SomeSizedList a] -> ShowS #
Buildable a => Buildable (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList Methods build :: SomeSizedList a -> Doc buildList :: [SomeSizedList a] -> Doc
Container (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList Associated Types type Element (SomeSizedList a) # Methods toList :: SomeSizedList a -> [Element (SomeSizedList a)] # null :: SomeSizedList a -> Bool # foldr :: (Element (SomeSizedList a) -> b -> b) -> b -> SomeSizedList a -> b # foldl :: (b -> Element (SomeSizedList a) -> b) -> b -> SomeSizedList a -> b # foldl' :: (b -> Element (SomeSizedList a) -> b) -> b -> SomeSizedList a -> b # length :: SomeSizedList a -> Int # elem :: Element (SomeSizedList a) -> SomeSizedList a -> Bool # foldMap :: Monoid m => (Element (SomeSizedList a) -> m) -> SomeSizedList a -> m # fold :: SomeSizedList a -> Element (SomeSizedList a) # foldr' :: (Element (SomeSizedList a) -> b -> b) -> b -> SomeSizedList a -> b # notElem :: Element (SomeSizedList a) -> SomeSizedList a -> Bool # all :: (Element (SomeSizedList a) -> Bool) -> SomeSizedList a -> Bool # any :: (Element (SomeSizedList a) -> Bool) -> SomeSizedList a -> Bool # and :: SomeSizedList a -> Bool # or :: SomeSizedList a -> Bool # find :: (Element (SomeSizedList a) -> Bool) -> SomeSizedList a -> Maybe (Element (SomeSizedList a)) # safeHead :: SomeSizedList a -> Maybe (Element (SomeSizedList a)) # safeMaximum :: SomeSizedList a -> Maybe (Element (SomeSizedList a)) # safeMinimum :: SomeSizedList a -> Maybe (Element (SomeSizedList a)) # safeFoldr1 :: (Element (SomeSizedList a) -> Element (SomeSizedList a) -> Element (SomeSizedList a)) -> SomeSizedList a -> Maybe (Element (SomeSizedList a)) # safeFoldl1 :: (Element (SomeSizedList a) -> Element (SomeSizedList a) -> Element (SomeSizedList a)) -> SomeSizedList a -> Maybe (Element (SomeSizedList a)) #
FromList (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList Associated Types type ListElement (SomeSizedList a) # type FromListC (SomeSizedList a) # Methods fromList :: [ListElement (SomeSizedList a)] -> SomeSizedList a #
type Element (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList type Element (SomeSizedList a) = ElementDefault (SomeSizedList a)
type FromListC (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList type FromListC (SomeSizedList a) = ()
type ListElement (SomeSizedList a) Source #
Instance details Defined in Morley.Util.SizedList type ListElement (SomeSizedList a) = a

Utility type synonyms

type SingIPeano (n :: Nat) = SingI (ToPeano n) Source #

A synonym for SingI (ToPeano n). Essentially requires that we can construct a Peano singleton for a given Nat

type IsoNatPeano (n :: Nat) (p :: Peano) = (n ~ FromPeano p, ToPeano n ~ p) Source #

A constraint asserting that GHC's Nat n and Peano p are the same (up to an isomorphism)