Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Type-level hackery.
This module is used for groups whose parameters are encoded as type-level natural numbers, for example finite cyclic groups, free groups, symmetric groups and braid groups.
- data Proxy k t :: forall k. k -> * = Proxy
- proxyUndef :: Proxy a -> a
- proxyOf :: a -> Proxy a
- proxyOf1 :: f a -> Proxy a
- proxyOf2 :: g (f a) -> Proxy a
- asProxyTypeOf :: a -> Proxy * a -> a
- asProxyTypeOf1 :: f a -> Proxy a -> f a
- typeArg :: KnownNat n => f (n :: Nat) -> Integer
- iTypeArg :: KnownNat n => f (n :: Nat) -> Int
- data Some f = KnownNat n => Some (f n)
- withSome :: Some f -> (forall n. KnownNat n => f n -> a) -> a
- withSomeM :: Monad m => Some f -> (forall n. KnownNat n => f n -> m a) -> m a
- selectSome :: Integral int => (forall n. KnownNat n => f n) -> int -> Some f
- selectSomeM :: forall m f int. (Integral int, Monad m) => (forall n. KnownNat n => m (f n)) -> int -> m (Some f)
- withSelected :: Integral int => (forall n. KnownNat n => f n -> a) -> (forall n. KnownNat n => f n) -> int -> a
- withSelectedM :: forall m f int a. (Integral int, Monad m) => (forall n. KnownNat n => f n -> a) -> (forall n. KnownNat n => m (f n)) -> int -> m a
Proxy
data Proxy k t :: forall k. k -> * #
A concrete, poly-kinded proxy type
Monad (Proxy *) | |
Functor (Proxy *) | |
Applicative (Proxy *) | |
Foldable (Proxy *) | |
Traversable (Proxy *) | |
Generic1 (Proxy *) | |
Alternative (Proxy *) | |
MonadPlus (Proxy *) | |
Bounded (Proxy k s) | |
Enum (Proxy k s) | |
Eq (Proxy k s) | |
Ord (Proxy k s) | |
Read (Proxy k s) | |
Show (Proxy k s) | |
Ix (Proxy k s) | |
Generic (Proxy k t) | |
Monoid (Proxy k s) | |
type Rep1 (Proxy *) | |
type Rep (Proxy k t) | |
proxyUndef :: Proxy a -> a Source #
asProxyTypeOf :: a -> Proxy * a -> a #
asProxyTypeOf
is a type-restricted version of const
.
It is usually used as an infix operator, and its typing forces its first
argument (which is usually overloaded) to have the same type as the tag
of the second.
asProxyTypeOf1 :: f a -> Proxy a -> f a Source #
Type-level naturals as type arguments
Hiding the type parameter
Hide the type parameter of a functor. Example: Some Braid
withSomeM :: Monad m => Some f -> (forall n. KnownNat n => f n -> m a) -> m a Source #
Monadic version of withSome
selectSome :: Integral int => (forall n. KnownNat n => f n) -> int -> Some f Source #
Given a polymorphic value, we select at run time the one specified by the second argument
selectSomeM :: forall m f int. (Integral int, Monad m) => (forall n. KnownNat n => m (f n)) -> int -> m (Some f) Source #
Monadic version of selectSome
withSelected :: Integral int => (forall n. KnownNat n => f n -> a) -> (forall n. KnownNat n => f n) -> int -> a Source #
Combination of selectSome
and withSome
: we make a temporary structure
of the given size, but we immediately consume it.
withSelectedM :: forall m f int a. (Integral int, Monad m) => (forall n. KnownNat n => f n -> a) -> (forall n. KnownNat n => m (f n)) -> int -> m a Source #
(Half-)monadic version of withSelected