Morley.Util.SizedList

Defines lists with length fixed on the type level

Base types

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

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

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

Foldable (SizedList' n)

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)

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)

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)

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)

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)

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)

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)

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))

Defined in Morley.Michelson.Typed.Haskell.Value

Associated Types

type ToBigMapKey (SizedList' n (k, v))

type ToBigMapValue (SizedList' n (k, v))

Methods

mkBigMap :: SizedList' n (k, v) -> BigMap (ToBigMapKey (SizedList' n (k, v))) (ToBigMapValue (SizedList' n (k, v)))

Buildable a => Buildable (SizedList' n a)

Defined in Morley.Util.SizedList

Methods

build :: SizedList' n a -> Doc

buildList :: [SizedList' n a] -> Doc

Container (SizedList' n a)

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)

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))

Defined in Morley.Michelson.Typed.Haskell.Value

type ToBigMapKey (SizedList' n (k, v)) = k

type ToBigMapValue (SizedList' n (k, v))

Defined in Morley.Michelson.Typed.Haskell.Value

type ToBigMapValue (SizedList' n (k, v)) = v

type Element (SizedList' n a)

Defined in Morley.Util.SizedList

type Element (SizedList' n a) = ElementDefault (SizedList' n a)

type OneItem (SizedList' n a)

Defined in Morley.Util.SizedList

type OneItem (SizedList' n a) = a

data SomeSizedList a where

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

Foldable SomeSizedList

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

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

Defined in Morley.Util.SizedList

Methods

fmap :: (a -> b) -> SomeSizedList a -> SomeSizedList b

(<$) :: a -> SomeSizedList b -> SomeSizedList a

Monoid (SomeSizedList a)

Defined in Morley.Util.SizedList

Methods

mempty :: SomeSizedList a

mappend :: SomeSizedList a -> SomeSizedList a -> SomeSizedList a

mconcat :: [SomeSizedList a] -> SomeSizedList a

Semigroup (SomeSizedList a)

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)

Defined in Morley.Util.SizedList

Methods

showsPrec :: Int -> SomeSizedList a -> ShowS

show :: SomeSizedList a -> String

showList :: [SomeSizedList a] -> ShowS

Buildable a => Buildable (SomeSizedList a)

Defined in Morley.Util.SizedList

Methods

build :: SomeSizedList a -> Doc

buildList :: [SomeSizedList a] -> Doc

Container (SomeSizedList a)

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)

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)

Defined in Morley.Util.SizedList

type Element (SomeSizedList a) = ElementDefault (SomeSizedList a)

type FromListC (SomeSizedList a)

Defined in Morley.Util.SizedList

type FromListC (SomeSizedList a) = ()

type ListElement (SomeSizedList a)

Defined in Morley.Util.SizedList

type ListElement (SomeSizedList a) = a

Utility type synonyms (re-exports)

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

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)

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

Basic

append :: SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a infixr 5

Append two sized lists.

>>> generate @3 (+1) `append` generate @3 (+11)
1 :< 2 :< 3 :< 11 :< 12 :< 13 :< Nil

reverse :: forall n a. SingI n => SizedList' n a -> SizedList' n a

Reverse a SizedList

>>> reverse $ generate @3 (+1)
3 :< 2 :< 1 :< Nil

head :: SizedList' ('S n) a -> a

Get the first element of a non-empty list

tail :: SizedList' ('S n) a -> SizedList' n a

Get elements after the first

Construction

withNonEmpty :: forall a r. NonEmpty a -> (forall n. SingNat ('S n) -> SizedList' ('S n) a -> r) -> r

Run some computation with a NonEmpty list converted to SizedList. Similar to pattern-matching on SomeSizedList, but asserts on the type level that list is in fact not empty.

withList :: forall a r. [a] -> (forall n. SingNat n -> SizedList' n a -> r) -> r

Run some computation with a list converted to SizedList. The same as pattern-matching on SomeSizedList.

fromList :: forall a. [a] -> SomeSizedList a

fromListMaybe :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => [a] -> Maybe (SizedList n a)

Try to make a fixed-size list from a regular list, given a Nat. Returns Nothing if the regular list has incorrect length.

>>> fromListMaybe @3 [1, 2, 3]
Just (1 :< 2 :< 3 :< Nil)

>>> fromListMaybe @4 [1, 2, 3]
Nothing

fromListMaybe' :: SingNat m -> [a] -> Maybe (SizedList' m a)

Same as fromListMaybe, but accepts an explicit Peano singleton.

unsafeFromList :: forall n n' a. (SingIPeano n, IsoNatPeano n n', HasCallStack) => [a] -> SizedList n a

Construct a list of given length from a regular list. Raise error if length is inconsistent.

>>> unsafeFromList @3 [1, 2, 3]
1 :< 2 :< 3 :< Nil

>>> unsafeFromList @1 [1, 2, 3]
*** Exception: Invalid list size in Morley.Util.SizedList.unsafeFromList
...

generate :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => (Natural -> a) -> SizedList' n' a

Given a type-level Nat and a generator function, make a SizedList

Indexing starts at 0

>>> generate @3 (+1)
1 :< 2 :< 3 :< Nil

generate' :: forall n a. SingNat n -> (forall m. (n > m) ~ 'True => (SingNat m, Natural) -> a) -> SizedList' n a

Same as generate, but accepts an explicit Peano singleton, and passes an explicit singleton as index to the generator function

replicate :: Natural -> a -> SomeSizedList a

Replicate a value n times. This is a version returning an existential. You probably want replicateT or replicate'.

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

As replicateT, but accepts an explicit Peano singleton.

replicateT :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => a -> SizedList n a

Replicate a value n times, where n is passed as a type-level natural. This is essentially a synonym for pure.

>>> replicateT @5 'a'
'a' :< 'a' :< 'a' :< 'a' :< 'a' :< Nil

singleton :: a -> SizedList 1 a

Construct a list of one element

Conversion

toNonEmpty :: SizedList' ('S n) a -> NonEmpty a

Convert a SizedList to NonEmpty

Zips

zipWith :: (a -> b -> c) -> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c

Zip using a binary operation.

unzipWith :: (a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c)

Unzip a sized list using a function

zip :: SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) (a, b)

Zip two lists of potentially different lengths. If one list is longer, extraneous elements will be ignored.

>>> zip (unsafeFromList @3 "abc") (unsafeFromList @4 "defg")
('a','d') :< ('b','e') :< ('c','f') :< Nil

unzip :: SizedList' n (b, c) -> (SizedList' n b, SizedList' n c)

Unzip a sized list of pairs

Index access

index' :: (m > n) ~ 'True => SingNat n -> SizedList' m a -> a

Same as index, but accepts an explicit Peano singleton

Note, that if you wish to use this with generate', indexing into some other list, for one, you may want to rethink your approach, since it's pretty inefficient. For two, you may run into arcane compiler error messages, e.g.

>>> let someList = 'a' :< 'b' :< 'c' :< Nil
>>> generate' @_ @Char (peanoSing @2) $ \(sg, _) -> index' sg someList
...
... Could not deduce (('S ('S ('S 'Z)) > m) ~ 'True)
...

To make this work, use transitivity proof:

>>> let slLen = length' someList
>>> let len = peanoSing @2
>>> generate' @_ @Char len $ \(sg, _) -> index' sg someList \\ transitivity slLen len sg
'a' :< 'b' :< Nil

index :: forall i m a. ((m > ToPeano i) ~ 'True, SingIPeano i) => SizedList' m a -> a

Index into a list using a type-level constant

>>> index @2 $ unsafeFromList @5 [1..5]
3

indexMaybe :: Natural -> SizedList' m a -> Maybe a

Use a term-level Natural to index into a list. Since the natural can be larger than the length of the list, returns a Maybe.

length' :: forall n a. SingI n => SizedList' n a -> SingNat n

Return a Peano singleton representing the list length

Sublists

take :: forall n n' m a. ((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') => SizedList' m a -> SizedList n a

Take a fixed number of elements, given by a type-level Nat. Must be smaller than the size of the list

>>> take @3 $ unsafeFromList @5 [1..5]
1 :< 2 :< 3 :< Nil

drop :: forall n n' m a. ((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') => SizedList' m a -> SizedList' (SubPeano m (ToPeano n)) a

Drop a fixed number of elements, given by a type-level Nat. Must be smaller than the size of the list

>>> drop @3 $ unsafeFromList @5 [1..5]
4 :< 5 :< Nil

splitAt :: forall n n' m a. ((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') => SizedList' m a -> (SizedList n a, SizedList' (SubPeano m n') a)

splitAt @n xs = (take @n xs, drop @n xs), but traverses the list only once

>>> splitAt @3 $ unsafeFromList @5 [1..5]
(1 :< 2 :< 3 :< Nil,4 :< 5 :< Nil)