Safe Haskell | None |
---|---|
Language | Haskell2010 |
Defines lists with length fixed on the type level
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)
- append :: SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a
- reverse :: forall n a. SingI n => SizedList' n a -> SizedList' n a
- head :: SizedList' ('S n) a -> a
- tail :: SizedList' ('S n) a -> SizedList' n a
- fromList :: forall a. [a] -> SomeSizedList a
- withNonEmpty :: forall a r. NonEmpty a -> (forall n. SingNat ('S n) -> SizedList' ('S n) a -> r) -> r
- withList :: forall a r. [a] -> (forall n. SingNat n -> SizedList' n a -> r) -> r
- fromListMaybe :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => [a] -> Maybe (SizedList n a)
- fromListMaybe' :: SingNat m -> [a] -> Maybe (SizedList' m a)
- unsafeFromList :: forall n n' a. (SingIPeano n, IsoNatPeano n n', HasCallStack) => [a] -> SizedList n a
- generate :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => (Natural -> a) -> SizedList n a
- generate' :: forall n a. SingNat n -> (forall m. (n > m) ~ 'True => (SingNat m, Natural) -> a) -> SizedList' n a
- replicate :: Natural -> a -> SomeSizedList a
- replicate' :: SingNat n -> a -> SizedList' n a
- replicateT :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => a -> SizedList n a
- singleton :: a -> SizedList 1 a
- toNonEmpty :: SizedList' ('S n) a -> NonEmpty a
- zipWith :: (a -> b -> c) -> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c
- unzipWith :: (a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c)
- zip :: SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) (a, b)
- unzip :: SizedList' n (b, c) -> (SizedList' n b, SizedList' n c)
- index' :: (m > n) ~ 'True => SingNat n -> SizedList' m a -> a
- index :: forall i m a. ((m > ToPeano i) ~ 'True, SingIPeano i) => SizedList' m a -> a
- indexMaybe :: Natural -> SizedList' m a -> Maybe a
- length' :: forall n a. SingI n => SizedList' n a -> SingNat n
- take :: forall n n' m a. ((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') => SizedList' m a -> SizedList n a
- drop :: forall n n' m a. ((m >= ToPeano n) ~ 'True, SingIPeano n, IsoNatPeano n n') => SizedList' m a -> SizedList' (SubPeano m (ToPeano n)) a
- 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)
Base types
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
Nil | |
| |
(:<) infixr 5 | |
|
pattern (::<) :: a -> SizedList' n a -> SizedList' ('S n) a infixr 5 | Sized list cons pattern. Unlike
|
pattern Nil' :: SizedList' 'Z a | Sized list Nil pattern. Unlike |
Instances
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 (SS (SS (SS (SS SZ)))) ('a' :< 'b' :< 'd' :< 'e' :< Nil)
SomeSizedList :: SingNat n -> SizedList' n a -> SomeSizedList a |
Instances
Utility type synonyms (re-exports)
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)
Basic
append :: SizedList' n a -> SizedList' m a -> SizedList' (AddPeano n m) a infixr 5 Source #
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 Source #
Reverse a SizedList
>>>
reverse $ generate @3 (+1)
3 :< 2 :< 1 :< Nil
head :: SizedList' ('S n) a -> a Source #
Get the first element of a non-empty list
tail :: SizedList' ('S n) a -> SizedList' n a Source #
Get elements after the first
Construction
fromList :: forall a. [a] -> SomeSizedList a Source #
Construct SomeSizedList
from a regular list
withNonEmpty :: forall a r. NonEmpty a -> (forall n. SingNat ('S n) -> SizedList' ('S n) a -> r) -> r Source #
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 Source #
Run some computation with a list converted to SizedList
. The same as
pattern-matching on SomeSizedList
.
fromListMaybe :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => [a] -> Maybe (SizedList n a) Source #
fromListMaybe' :: SingNat m -> [a] -> Maybe (SizedList' m a) Source #
Same as fromListMaybe
, but accepts an explicit Peano
singleton.
unsafeFromList :: forall n n' a. (SingIPeano n, IsoNatPeano n n', HasCallStack) => [a] -> SizedList n a Source #
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 Source #
generate' :: forall n a. SingNat n -> (forall m. (n > m) ~ 'True => (SingNat m, Natural) -> a) -> SizedList' n a Source #
replicate :: Natural -> a -> SomeSizedList a Source #
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 Source #
As replicateT
, but accepts an explicit Peano
singleton.
replicateT :: forall n n' a. (SingIPeano n, IsoNatPeano n n') => a -> SizedList n a Source #
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
Conversion
toNonEmpty :: SizedList' ('S n) a -> NonEmpty a Source #
Zips
zipWith :: (a -> b -> c) -> SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) c Source #
Zip using a binary operation.
unzipWith :: (a -> (b, c)) -> SizedList' n a -> (SizedList' n b, SizedList' n c) Source #
Unzip a sized list using a function
zip :: SizedList' n a -> SizedList' m b -> SizedList' (MinPeano n m) (a, b) Source #
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) Source #
Unzip a sized list of pairs
Index access
index' :: (m > n) ~ 'True => SingNat n -> SizedList' m a -> a Source #
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, _) -> transitivity slLen len sg |- index' sg someList
'a' :< 'b' :< Nil
index :: forall i m a. ((m > ToPeano i) ~ 'True, SingIPeano i) => SizedList' m a -> a Source #
Index into a list using a type-level constant
>>>
index @2 $ unsafeFromList @5 [1..5]
3
indexMaybe :: Natural -> SizedList' m a -> Maybe a Source #
length' :: forall n a. SingI n => SizedList' n a -> SingNat n Source #
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 Source #
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 Source #
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) Source #
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)