Safe Haskell	Safe
Language	Haskell2010

Math.Combinat.TypeLevel

Contents

Proxy
Type-level naturals as type arguments
Hiding the type parameter

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.

Synopsis

data Proxy (t :: k) :: 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 (t :: k) :: forall k. k -> * #

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the 'undefined :: a' idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy

Instances

Generic1 (Proxy :: k -> *)
Instance details Defined in GHC.Generics Associated Types type Rep1 Proxy :: k -> * # Methods from1 :: Proxy a -> Rep1 Proxy a # to1 :: Rep1 Proxy a -> Proxy a #
Monad (Proxy :: * -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b # (>>) :: Proxy a -> Proxy b -> Proxy b # return :: a -> Proxy a # fail :: String -> Proxy a #
Functor (Proxy :: * -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods fmap :: (a -> b) -> Proxy a -> Proxy b # (<$) :: a -> Proxy b -> Proxy a #
Applicative (Proxy :: * -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods pure :: a -> Proxy a # (<>) :: Proxy (a -> b) -> Proxy a -> Proxy b # liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c # (>) :: Proxy a -> Proxy b -> Proxy b # (<*) :: Proxy a -> Proxy b -> Proxy a #
Foldable (Proxy :: * -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Foldable Methods fold :: Monoid m => Proxy m -> m # foldMap :: Monoid m => (a -> m) -> Proxy a -> m # foldr :: (a -> b -> b) -> b -> Proxy a -> b # foldr' :: (a -> b -> b) -> b -> Proxy a -> b # foldl :: (b -> a -> b) -> b -> Proxy a -> b # foldl' :: (b -> a -> b) -> b -> Proxy a -> b # foldr1 :: (a -> a -> a) -> Proxy a -> a # foldl1 :: (a -> a -> a) -> Proxy a -> a # toList :: Proxy a -> [a] # null :: Proxy a -> Bool # length :: Proxy a -> Int # elem :: Eq a => a -> Proxy a -> Bool # maximum :: Ord a => Proxy a -> a # minimum :: Ord a => Proxy a -> a # sum :: Num a => Proxy a -> a # product :: Num a => Proxy a -> a #
Traversable (Proxy :: * -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Traversable Methods traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b) # sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a) # mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b) # sequence :: Monad m => Proxy (m a) -> m (Proxy a) #
Alternative (Proxy :: * -> *)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods empty :: Proxy a # (<\|>) :: Proxy a -> Proxy a -> Proxy a # some :: Proxy a -> Proxy [a] # many :: Proxy a -> Proxy [a] #
MonadPlus (Proxy :: * -> *)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods mzero :: Proxy a # mplus :: Proxy a -> Proxy a -> Proxy a #
Bounded (Proxy t)
Instance details Defined in Data.Proxy Methods minBound :: Proxy t # maxBound :: Proxy t #
Enum (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods succ :: Proxy s -> Proxy s # pred :: Proxy s -> Proxy s # toEnum :: Int -> Proxy s # fromEnum :: Proxy s -> Int # enumFrom :: Proxy s -> [Proxy s] # enumFromThen :: Proxy s -> Proxy s -> [Proxy s] # enumFromTo :: Proxy s -> Proxy s -> [Proxy s] # enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s] #
Eq (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods (==) :: Proxy s -> Proxy s -> Bool # (/=) :: Proxy s -> Proxy s -> Bool #
Ord (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods compare :: Proxy s -> Proxy s -> Ordering # (<) :: Proxy s -> Proxy s -> Bool # (<=) :: Proxy s -> Proxy s -> Bool # (>) :: Proxy s -> Proxy s -> Bool # (>=) :: Proxy s -> Proxy s -> Bool # max :: Proxy s -> Proxy s -> Proxy s # min :: Proxy s -> Proxy s -> Proxy s #
Read (Proxy t)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods readsPrec :: Int -> ReadS (Proxy t) # readList :: ReadS [Proxy t] # readPrec :: ReadPrec (Proxy t) # readListPrec :: ReadPrec [Proxy t] #
Show (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods showsPrec :: Int -> Proxy s -> ShowS # show :: Proxy s -> String # showList :: [Proxy s] -> ShowS #
Ix (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods range :: (Proxy s, Proxy s) -> [Proxy s] # index :: (Proxy s, Proxy s) -> Proxy s -> Int # unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool # rangeSize :: (Proxy s, Proxy s) -> Int # unsafeRangeSize :: (Proxy s, Proxy s) -> Int
Generic (Proxy t)
Instance details Defined in GHC.Generics Associated Types type Rep (Proxy t) :: * -> * # Methods from :: Proxy t -> Rep (Proxy t) x # to :: Rep (Proxy t) x -> Proxy t #
Semigroup (Proxy s)	Since: base-4.9.0.0
Instance details Defined in Data.Proxy Methods (<>) :: Proxy s -> Proxy s -> Proxy s # sconcat :: NonEmpty (Proxy s) -> Proxy s # stimes :: Integral b => b -> Proxy s -> Proxy s #
Monoid (Proxy s)	Since: base-4.7.0.0
Instance details Defined in Data.Proxy Methods mempty :: Proxy s # mappend :: Proxy s -> Proxy s -> Proxy s # mconcat :: [Proxy s] -> Proxy s #
type Rep1 (Proxy :: k -> *)
Instance details Defined in GHC.Generics type Rep1 (Proxy :: k -> ) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: k -> ))
type Rep (Proxy t)
Instance details Defined in GHC.Generics type Rep (Proxy t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: * -> *))

proxyUndef :: Proxy a -> a Source #

proxyOf :: a -> Proxy a Source #

proxyOf1 :: f a -> Proxy a Source #

proxyOf2 :: g (f a) -> Proxy 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.

>>> import Data.Word
>>> :type asProxyTypeOf 123 (Proxy :: Proxy Word8)
asProxyTypeOf 123 (Proxy :: Proxy Word8) :: Word8

Note the lower-case proxy in the definition. This allows any type constructor with just one argument to be passed to the function, for example we could also write

>>> import Data.Word
>>> :type asProxyTypeOf 123 (Just (undefined :: Word8))
asProxyTypeOf 123 (Just (undefined :: Word8)) :: Word8

asProxyTypeOf1 :: f a -> Proxy a -> f a Source #

Type-level naturals as type arguments

typeArg :: KnownNat n => f (n :: Nat) -> Integer Source #

iTypeArg :: KnownNat n => f (n :: Nat) -> Int Source #

Hiding the type parameter

data Some f Source #

Hide the type parameter of a functor. Example: Some Braid

Constructors

KnownNat n => Some (f n)

withSome :: Some f -> (forall n. KnownNat n => f n -> a) -> a Source #

Uses the value inside a Some

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