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].

Methods

natsVal :: p ns -> [Integer]

natsList :: NatList ns

Instances

KnownNats ([] Nat)

(KnownNat n, KnownNats ns) => KnownNats ((:) 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)

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.

someNatsVal' :: [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.

For compatability with reifyNat, be aware that this also produces KnownNat ns where n is negative, without complaining.

sameNats :: (KnownNats ns, KnownNats ms) => 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

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' SomeNat SomeNats.

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

Like traverseNatList, but literally actually a Traversal' SomeNat SomeNats, 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 ns where

KnownSymbols ns is intended to represent that every Symbol in the type-level list ns 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 ns.

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

Methods

symbolsVal :: p ns -> [String]

symbolsList :: SymbolList ns

Instances

KnownSymbols ([] Symbol)

(KnownSymbol n, KnownSymbols ns) => KnownSymbols ((:) Symbol n ns)

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 ns => !(SymbolList ns) -> 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 n, KnownSymbols ns) => !(Proxy n) -> !(SymbolList ns) -> SymbolList (n : ns) infixr 5

Instances

Show (SymbolList ns)

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 ns. KnownSymbols ns => SymbolList 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 SomeSymbols.

sameSymbols :: (KnownSymbols ns, KnownSymbols ms) => 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

Traversals

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

Utility function for traversing over all of the Proxy ns 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' SomeSymbol SomeSymbols.

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

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

traverseSymbolList_ :: forall f ns. Applicative f => (forall n a. KnownSymbol n => Proxy n -> f a) -> SymbolList ns -> f ()

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

Maps

mapSymbolList :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol) -> SymbolList ns -> 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.