Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
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 Char
SomeSizedList (SS (SS (SS (SS SZ)))) ('a' :< 'b' :< 'd' :< 'e' :< Nil)
SomeSizedList :: SingNat n -> SizedList' n a -> SomeSizedList a |