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

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.

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.

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.

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.

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.

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.

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

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

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

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.

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

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.

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.

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.

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.

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

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

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