GHC.TypeLits.List

Deprecated: Use singletons package instead

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 :: [Nat]) 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].

Deprecated: Use SingI from singletons instead.

Minimal complete definition

natsVal, natsList

Methods

natsVal :: p ns -> [Integer]

Deprecated: Use fromSing from singletons instead.

natsList :: NatList ns

Deprecated: Use sing from singletons instead.

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.

Deprecated: Use SomeSing from singletons instead.

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.

Deprecated: Use Sing from singletons instead.

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.

Deprecated: Use toSing from singletons instead.

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.

Deprecated: Use toSing from singletons instead.

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.

Deprecated: Use withSomeSing from singletons instead.

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.

Deprecated: Use withSomeSing from singletons 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

Deprecated: Use %~ from singletons instead.

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 :: [Symbol]) 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.

Deprecated: Use 'SingI from singletons instead.

Minimal complete definition

symbolsVal, symbolsList

Methods

symbolsVal :: p ss -> [String]

Deprecated: Use fromSing from singletons instead.

symbolsList :: SymbolList ss

Deprecated: Use 'sing from singletons instead.

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.

Deprecated: Use SomeSing from singletons instead.

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.

Deprecated: Use Sing from singletons instead.

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.

Deprecated: Use toSing from singletons instead.

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.

Deprecated: Use withSomeSing from singletons instead.

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

Deprecated: Use %~ from singletons instead.

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.