Safe Haskell | Safe-Inferred |
---|---|
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.
Synopsis
- 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
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,
is a safer alternative to the
Proxy
:: Proxy
a
idiom.undefined
:: a
>>>
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
Instances
Generic1 (Proxy :: k -> Type) | |
Foldable (Proxy :: TYPE LiftedRep -> Type) | Since: base-4.7.0.0 |
Defined in Data.Foldable fold :: Monoid m => Proxy m -> m # foldMap :: Monoid m => (a -> m) -> Proxy a -> 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 # elem :: Eq a => a -> Proxy a -> Bool # maximum :: Ord a => Proxy a -> a # minimum :: Ord a => Proxy a -> a # | |
Eq1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Ord1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Read1 (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Defined in Data.Functor.Classes | |
Show1 (Proxy :: TYPE LiftedRep -> Type) | Since: base-4.9.0.0 |
Traversable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Alternative (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Applicative (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Functor (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Monad (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
MonadPlus (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Monoid (Proxy s) | Since: base-4.7.0.0 |
Semigroup (Proxy s) | Since: base-4.9.0.0 |
Bounded (Proxy t) | Since: base-4.7.0.0 |
Enum (Proxy s) | Since: base-4.7.0.0 |
Generic (Proxy t) | |
Ix (Proxy s) | Since: base-4.7.0.0 |
Defined in Data.Proxy | |
Read (Proxy t) | Since: base-4.7.0.0 |
Show (Proxy s) | Since: base-4.7.0.0 |
Eq (Proxy s) | Since: base-4.7.0.0 |
Ord (Proxy s) | Since: base-4.7.0.0 |
type Rep1 (Proxy :: k -> Type) | Since: base-4.6.0.0 |
type Rep (Proxy t) | Since: base-4.6.0.0 |
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.
>>>
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
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