GHC.TypeLits.List

Provides the KnownNats and KnownSymbols typeclasses in analogy to KnownNat and KnownSymbol from GHC.TypeLits. Also provides singleton-esque structures for traversing over type-level lists of Nats and Symbols. Comes with continuation-style reifiers and existential types for dependent typing usage, and as an analogy with SomeNat and SomeSymbol.

See typeclass documentations and README for more information.

KnownNats

class KnownNats ns where

KnownNats ns is intended to represent that every Nat in the type-level list ns is itself a KnownNat (meaning, you can use natVal to get its corresponding Integer).

In practice, just knowing that every item has a KnownNat instance is not enough; it's nice, but unless you're able to "iterate" over every Nat in the list, it's of limited use. That's why this class also provides a constructor for NatList ns, so that you can produce a NatList for every KnownNat ns, which you can iterate over to get Proxy ns for every n in ns along with the KnownNat n instances.

It also has an analogy to natVal, natsVal, which lets you get a list of the represented Integers for, say, Proxy [1,2,3].

Minimal complete definition

natsVal, natsList

Methods

natsVal :: p ns -> [Integer]

natsList :: NatList ns

Instances

KnownNats ([] Nat)

Methods

natsVal :: p [Nat] -> [Integer]

natsList :: NatList [Nat]

(KnownNat n, KnownNats ns) => KnownNats ((:) Nat n ns)

Methods

natsVal :: p ((Nat ': n) ns) -> [Integer]

natsList :: NatList ((Nat ': n) ns)

data SomeNats :: * where

Represents unknown type-level lists of type-level natural numbers. It's a NatList, but you don't know what the list contains at compile-time.

Constructors

SomeNats :: KnownNats ns => !(NatList ns) -> SomeNats

data NatList :: [Nat] -> * where

Singleton-esque type for "traversing" over type-level lists of Nats. Essentially contains a (value-level) list of Proxy ns, but each n has a KnownNat instance for you to use. At runtime (after type erasure), is more or less equivalent to a [Integer].

Typically generated using natsList.

Constructors

ØNL :: NatList '[]

(:<#) :: (KnownNat n, KnownNats ns) => !(Proxy n) -> !(NatList ns) -> NatList (n ': ns) infixr 5

Instances

Show (NatList ns)

Methods

showsPrec :: Int -> NatList ns -> ShowS

show :: NatList ns -> String

showList :: [NatList ns] -> ShowS

someNatsVal :: [Integer] -> Maybe SomeNats

List equivalent of someNatVal. Convert a list of integers into an unknown type-level list of naturals. Will return Nothing if any of the given Integers is negative.

someNatsValPos :: [Integer] -> SomeNats

Like someNatsVal, but will also go ahead and produce KnownNats whose integer values are negative. It won't ever error on producing them, but extra care must be taken when using the produced SomeNats.

reifyNats :: [Integer] -> (forall ns. KnownNats ns => NatList ns -> r) -> r

List equivalent of reifyNat. Given a list of integers, takes a function in an "environment" with a NatList ns corresponding to the given list, where every n in ns has a KnownNat instance.

Essentially a continuation-style version of SomeNats.

Be aware that this also produces KnownNat ns where n is negative, without complaining. To be consistent, within the library, this should be called reifyNatsPos; however, the naming choice is for consistency with reifyNat from the reflections package. Use reifyNats' for a "safe" version.

reifyNats' :: [Integer] -> r -> (forall ns. KnownNats ns => NatList ns -> r) -> r

Safe version of reifyNats, which will only run the continuation if every Integer in the list is non-negative. If not, then returns the given "default" value instead.

sameNats :: NatList ns -> NatList ms -> Maybe (ns :~: ms)

Get evidence that the two KnownNats lists are actually the "same" list of Nats (that they were instantiated with the same numbers).

Essentialy runs sameNat over the lists:

case sameNats ns ms of
  Just Refl -> -- in this branch, GHC recognizes that the two [Nat]s
                 -- are the same.
  Nothing   -> -- in this branch, they aren't

elimNatList :: forall p ns. p '[] -> (forall m ms. (KnownNat m, KnownNats ms) => Proxy m -> p ms -> p (m ': ms)) -> NatList ns -> p ns

The "eliminator" for NatList. You can think of this as a dependently typed analogy for a fold.

Since 0.2.1.0

Traversals

traverseNatList :: forall f ns. Applicative f => (forall n. KnownNat n => Proxy n -> f SomeNat) -> NatList ns -> f SomeNats

Utility function for traversing over all of the Proxy ns in a NatList, each with the corresponding KnownNat instance available. Gives the the ability to "change" the represented natural number to a new one, in a SomeNat.

Can be considered a form of a Traversal' SomeNats SomeNat.

traverseNatList' :: forall f. Applicative f => (SomeNat -> f SomeNat) -> SomeNats -> f SomeNats

Like traverseNatList, but literally actually a Traversal' SomeNats SomeNat, avoiding the Rank-2 types, so is usable with lens-library machinery.

traverseNatList_ :: forall f a ns. Applicative f => (forall n. KnownNat n => Proxy n -> f a) -> NatList ns -> f ()

Utility function for traversing over all of the Proxy ns in a NatList, each with the corresponding KnownNat instance available. Results are ignored.

Maps

mapNatList :: (forall n. KnownNat n => Proxy n -> SomeNat) -> NatList ns -> SomeNats

Utility function for "mapping" over each of the Nats in the NatList.

mapNatList' :: (SomeNat -> SomeNat) -> SomeNats -> SomeNats

Like mapNatList, but avoids the Rank-2 types, so can be used with . (function composition) and in other situations where mapNatList would cause problems.

KnownSymbols

class KnownSymbols ss where

KnownSymbols ss is intended to represent that every Symbol in the type-level list ss is itself a KnownSymbol (meaning, you can use symbolVal to get its corresponding String).

You can use symbolsVal to get the corresponding [String] from KnownSymbols ss.

For reasons discussed further in the documentation for KnownNats, this also lets you generate a SymbolList ss, in order to iterate over the type-level list of Symbols and take advantage of their KnownSymbol instances.

Minimal complete definition

symbolsVal, symbolsList

Methods

symbolsVal :: p ss -> [String]

symbolsList :: SymbolList ss

Instances

KnownSymbols ([] Symbol)

Methods

symbolsVal :: p [Symbol] -> [String]

symbolsList :: SymbolList [Symbol]

(KnownSymbol s, KnownSymbols ss) => KnownSymbols ((:) Symbol s ss)

Methods

symbolsVal :: p ((Symbol ': s) ss) -> [String]

symbolsList :: SymbolList ((Symbol ': s) ss)

data SomeSymbols :: * where

Represents unknown type-level lists of Symbols. It's a SymbolList, but you don't know what the list contains at compile-time.

Constructors

SomeSymbols :: KnownSymbols ss => !(SymbolList ss) -> SomeSymbols

data SymbolList :: [Symbol] -> * where

Singleton-esque type for "traversing" over type-level lists of Symbols. Essentially contains a (value-level) list of Proxy ns, but each n has a KnownSymbol instance for you to use. At runtime (after type erasure), is more or less equivalent to a [String].

Typically generated using symbolsList.

Constructors

ØSL :: SymbolList '[]

(:<$) :: (KnownSymbol s, KnownSymbols ss) => !(Proxy s) -> !(SymbolList ss) -> SymbolList (s ': ss) infixr 5

Instances

Show (SymbolList ns)

Methods

showsPrec :: Int -> SymbolList ns -> ShowS

show :: SymbolList ns -> String

showList :: [SymbolList ns] -> ShowS

someSymbolsVal :: [String] -> SomeSymbols

List equivalent of someNatVal. Convert a list of integers into an unknown type-level list of naturals. Will return Nothing if any of the given Integers is negative.

reifySymbols :: [String] -> (forall ss. KnownSymbols ss => SymbolList ss -> r) -> r

List equivalent of reifyNat. Given a list of integers, takes a function in an "environment" with a SymbolList ss corresponding to the given list, where every s in ss has a KnownSymbol instance.

Essentially a continuation-style version of SomeSymbols.

sameSymbols :: SymbolList ns -> SymbolList ms -> Maybe (ns :~: ms)

Get evidence that the two KnownSymbols lists are actually the "same" list of Symboless (that they were instantiated with the same strings).

Essentialy runs sameSymbol over the lists:

case sameSymbols ns ms of
  Just Refl -> -- in this branch, GHC recognizes that the
                 -- two [Symbol]s are the same
  Nothing   -> -- in this branch, they aren't

elimSymbolList :: forall p ss. p '[] -> (forall t ts. (KnownSymbol t, KnownSymbols ts) => Proxy t -> p ts -> p (t ': ts)) -> SymbolList ss -> p ss

The "eliminator" for SymbolList. You can think of this as a dependently typed analogy for a fold.

Since 0.2.1.0

Traversals

traverseSymbolList :: forall f ss. Applicative f => (forall s. KnownSymbol s => Proxy s -> f SomeSymbol) -> SymbolList ss -> f SomeSymbols

Utility function for traversing over all of the Proxy ss in a SymbolList, each with the corresponding KnownSymbol instance available. Gives the the ability to "change" the represented natural number to a new one, in a SomeSymbol.

Can be considered a form of a Traversal' SomeSymbols SomeSymbol.

traverseSymbolList' :: forall f. Applicative f => (SomeSymbol -> f SomeSymbol) -> SomeSymbols -> f SomeSymbols

Like traverseSymbolList, but literally actually a Traversal' SomeSymbols SomeSymbol, avoiding the Rank-2 types, so is usable with lens-library machinery.

traverseSymbolList_ :: forall f ss. Applicative f => (forall s a. KnownSymbol s => Proxy s -> f a) -> SymbolList ss -> f ()

Utility function for traversing over all of the Proxy ss in a SymbolList, each with the corresponding KnownSymbol instance available. Results are ignored.

Maps

mapSymbolList :: (forall s. KnownSymbol s => Proxy s -> SomeSymbol) -> SymbolList ss -> SomeSymbols

Utility function for "mapping" over each of the Symbols in the SymbolList.

mapSymbolList' :: (SomeSymbol -> SomeSymbol) -> SomeSymbols -> SomeSymbols

Like mapSymbolList, but avoids the Rank-2 types, so can be used with . (function composition) and in other situations where mapSymbolList would cause problems.