| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Math.Combinat.TypeLevel
Description
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 t :: 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 = forall n . 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 t :: k -> *
A concrete, poly-kinded proxy type
Constructors
| Proxy |
Instances
| Monad (Proxy *) | |
| Functor (Proxy *) | |
| Applicative (Proxy *) | |
| Foldable (Proxy *) | |
| Traversable (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 * t) | |
| Monoid (Proxy k s) | |
| type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1) |
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