Copyright | (c) Justin Le 2016 |
---|---|
License | MIT |
Maintainer | justin@jle.im |
Stability | unstable |
Portability | non-portable |
Safe Haskell | Safe |
Language | Haskell2010 |
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
Nat
s and Symbol
s. 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.
- class KnownNats (ns :: [Nat]) where
- data SomeNats :: * where
- data NatList :: [Nat] -> * where
- someNatsVal :: [Integer] -> Maybe SomeNats
- someNatsValPos :: [Integer] -> SomeNats
- reifyNats :: [Integer] -> (forall ns. KnownNats ns => NatList ns -> r) -> r
- reifyNats' :: [Integer] -> r -> (forall ns. KnownNats ns => NatList ns -> r) -> r
- sameNats :: NatList ns -> NatList ms -> Maybe (ns :~: ms)
- elimNatList :: forall p ns. p '[] -> (forall m ms. (KnownNat m, KnownNats ms) => Proxy m -> p ms -> p (m ': ms)) -> NatList ns -> p ns
- traverseNatList :: forall f ns. Applicative f => (forall n. KnownNat n => Proxy n -> f SomeNat) -> NatList ns -> f SomeNats
- traverseNatList' :: forall f. Applicative f => (SomeNat -> f SomeNat) -> SomeNats -> f SomeNats
- traverseNatList_ :: forall f a ns. Applicative f => (forall n. KnownNat n => Proxy n -> f a) -> NatList ns -> f ()
- mapNatList :: (forall n. KnownNat n => Proxy n -> SomeNat) -> NatList ns -> SomeNats
- mapNatList' :: (SomeNat -> SomeNat) -> SomeNats -> SomeNats
- class KnownSymbols (ss :: [Symbol]) where
- data SomeSymbols :: * where
- SomeSymbols :: KnownSymbols ss => !(SymbolList ss) -> SomeSymbols
- data SymbolList :: [Symbol] -> * where
- ØSL :: SymbolList '[]
- (:<$) :: (KnownSymbol s, KnownSymbols ss) => !(Proxy s) -> !(SymbolList ss) -> SymbolList (s ': ss)
- someSymbolsVal :: [String] -> SomeSymbols
- reifySymbols :: [String] -> (forall ss. KnownSymbols ss => SymbolList ss -> r) -> r
- sameSymbols :: SymbolList ns -> SymbolList ms -> Maybe (ns :~: ms)
- elimSymbolList :: forall p ss. p '[] -> (forall t ts. (KnownSymbol t, KnownSymbols ts) => Proxy t -> p ts -> p (t ': ts)) -> SymbolList ss -> p ss
- traverseSymbolList :: forall f ss. Applicative f => (forall s. KnownSymbol s => Proxy s -> f SomeSymbol) -> SymbolList ss -> f SomeSymbols
- traverseSymbolList' :: forall f. Applicative f => (SomeSymbol -> f SomeSymbol) -> SomeSymbols -> f SomeSymbols
- traverseSymbolList_ :: forall f ss. Applicative f => (forall s a. KnownSymbol s => Proxy s -> f a) -> SymbolList ss -> f ()
- mapSymbolList :: (forall s. KnownSymbol s => Proxy s -> SomeSymbol) -> SymbolList ss -> SomeSymbols
- mapSymbolList' :: (SomeSymbol -> SomeSymbol) -> SomeSymbols -> SomeSymbols
KnownNats
class KnownNats (ns :: [Nat]) where Source #
is intended to represent that every KnownNats
nsNat
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
, so that you can produce
a NatList
nsNatList
for every
, which you can iterate over to get
KnownNat
ns
s for every Proxy
nn
in ns
along with the
instances.KnownNat
n
It also has an analogy to natVal
, natsVal
, which lets you get a list
of the represented Integer
s for, say,
.Proxy
[1,2,3]
Deprecated: Use SingI
from singletons instead.
data SomeNats :: * where Source #
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.
data NatList :: [Nat] -> * where Source #
Singleton-esque type for "traversing" over type-level lists of Nat
s.
Essentially contains a (value-level) list of
s, but each Proxy
nn
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.
someNatsVal :: [Integer] -> Maybe SomeNats Source #
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 Integer
s is negative.
Deprecated: Use toSing
from singletons instead.
someNatsValPos :: [Integer] -> SomeNats Source #
Like someNatsVal
, but will also go ahead and produce KnownNat
s
whose integer values are negative. It won't ever error on producing
them, but extra care must be taken when using the produced SomeNat
s.
Deprecated: Use toSing
from singletons instead.
reifyNats :: [Integer] -> (forall ns. KnownNats ns => NatList ns -> r) -> r Source #
List equivalent of reifyNat
. Given a list of integers, takes
a function in an "environment" with a
corresponding to
the given list, where every NatList
nsn
in ns
has a KnownNat
instance.
Essentially a continuation-style version of SomeNats
.
Be aware that this also produces
s where KnownNat
nn
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.
sameNats :: NatList ns -> NatList ms -> Maybe (ns :~: ms) Source #
Get evidence that the two KnownNats
lists are actually the "same"
list of Nat
s (that they were instantiated with the same numbers).
Essentialy runs sameNat
over the lists:
casesameNats
ns ms of JustRefl
-> -- 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 Source #
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 Source #
traverseNatList' :: forall f. Applicative f => (SomeNat -> f SomeNat) -> SomeNats -> f SomeNats Source #
Like traverseNatList
, but literally actually a Traversal'
, avoiding the Rank-2 types, so is usable with
lens-library machinery.SomeNats
SomeNat
traverseNatList_ :: forall f a ns. Applicative f => (forall n. KnownNat n => Proxy n -> f a) -> NatList ns -> f () Source #
Maps
mapNatList' :: (SomeNat -> SomeNat) -> SomeNats -> SomeNats Source #
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 Source #
is intended to represent that every KnownSymbols
ssSymbol
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 [
from
String
]
.KnownSymbols
ss
For reasons discussed further in the documentation for KnownNats
, this
also lets you generate a
, in order to iterate over the
type-level list of SymbolList
ssSymbol
s and take advantage of their KnownSymbol
instances.
Deprecated: Use 'SingI from singletons instead.
symbolsVal :: p ss -> [String] Source #
Deprecated: Use fromSing
from singletons instead.
symbolsList :: SymbolList ss Source #
Deprecated: Use 'sing from singletons instead.
KnownSymbols ([] Symbol) Source # | |
(KnownSymbol s, KnownSymbols ss) => KnownSymbols ((:) Symbol s ss) Source # | |
data SomeSymbols :: * where Source #
Represents unknown type-level lists of Symbol
s. It's a SymbolList
,
but you don't know what the list contains at compile-time.
Deprecated: Use SomeSing
from singletons instead.
SomeSymbols :: KnownSymbols ss => !(SymbolList ss) -> SomeSymbols |
data SymbolList :: [Symbol] -> * where Source #
Singleton-esque type for "traversing" over type-level lists of
Symbol
s. Essentially contains a (value-level) list of
s,
but each Proxy
nn
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.
ØSL :: SymbolList '[] | |
(:<$) :: (KnownSymbol s, KnownSymbols ss) => !(Proxy s) -> !(SymbolList ss) -> SymbolList (s ': ss) infixr 5 |
Show (SymbolList ns) Source # | |
someSymbolsVal :: [String] -> SomeSymbols Source #
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 Integer
s is negative.
Deprecated: Use toSing
from singletons instead.
reifySymbols :: [String] -> (forall ss. KnownSymbols ss => SymbolList ss -> r) -> r Source #
List equivalent of reifyNat
. Given a list of integers, takes
a function in an "environment" with a
corresponding to
the given list, where every SymbolList
sss
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) Source #
Get evidence that the two KnownSymbols
lists are actually the "same"
list of Symboles
s (that they were instantiated with the same strings).
Essentialy runs sameSymbol
over the lists:
casesameSymbols
ns ms of JustRefl
-> -- 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 Source #
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 Source #
Utility function for traversing over all of the
s in
a Proxy
sSymbolList
, 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 Source #
Like traverseSymbolList
, but literally actually a
Traversal'
, avoiding the Rank-2 types, so
is usable with lens-library machinery.SomeSymbols
SomeSymbol
traverseSymbolList_ :: forall f ss. Applicative f => (forall s a. KnownSymbol s => Proxy s -> f a) -> SymbolList ss -> f () Source #
Utility function for traversing over all of the
s in
a Proxy
sSymbolList
, each with the corresponding KnownSymbol
instance
available. Results are ignored.
Maps
mapSymbolList :: (forall s. KnownSymbol s => Proxy s -> SomeSymbol) -> SymbolList ss -> SomeSymbols Source #
Utility function for "mapping" over each of the Symbol
s in the
SymbolList
.
mapSymbolList' :: (SomeSymbol -> SomeSymbol) -> SomeSymbols -> SomeSymbols Source #
Like mapSymbolList
, but avoids the Rank-2 types, so can be used with
.
(function composition) and in other situations where mapSymbolList
would cause problems.