Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- class Let (a :: k) (b :: k)
- class Equal (a :: k) (b :: k)
- castEqual :: Equal a b => a -> b
- data LetT (a :: k) where
- letT :: Proxy a -> LetT a
- letT' :: forall r a. Proxy a -> (forall b. Let b a => Proxy b -> r) -> r
- data LetAs f (a :: k) where
- letAs :: f a -> LetAs f a
- letAs' :: forall r f a. f a -> (forall b. Let b a => f b -> r) -> r
- data Proxy (t :: k) = Proxy
Main classes
class Let (a :: k) (b :: k) Source #
Type-level let
A constraint Let x t
where x
is an (existential) type variable and t
is an arbitrary type represents a type-level let binding let x = t
.
o Introduction form
Type-level let bindings should be introduced using letT
or its slightly
higher level cousin, letAs
.
o Elimination form
To eliminate type-level let, use castEqual
.
Instances
Let (a :: k) (a :: k) Source # | Reflexivity A constraint User code normally does not work with
|
Defined in TypeLet.UserAPI |
class Equal (a :: k) (b :: k) Source #
(Nominal) type equality, up to type-level let
This is a class without any definitions; 'Equal a b' is instead proved by the plugin. Suppose we have a bunch of type-level let constraints in scope
Let x1 t1 Let x2 t2 ...
Then if σ is the corresponding idempotent substitution, two types a
and b
are considered Equal
if σ(a)
and σ(b)
are nominally equal.
Introduction forms
letT :: Proxy a -> LetT a Source #
Primitive way to introduce type-level let binding.
Usage:
case letT (Proxy @t) of LetT (_ :: Proxy x) ->
This introduces a type-level let binding x = t
.
letT' :: forall r a. Proxy a -> (forall b. Let b a => Proxy b -> r) -> r Source #
CPS form of letT
While this is more convenient to use, the r
parameter itself requires
careful thought.
letAs :: f a -> LetAs f a Source #
Pair a type-level let binding with a cast
Often when we introduce a type-level let x = t
, we then want to cast some
term e :: t
to a term e :: x
; function letAs
does these two things in
one operation.
If we did the above as written, however, we would have a term e :: x
where
we know nothing about x
at all (unless we cast again). This is typically
not useful; instead, we go from a term e :: f t
to a term e :: f x
,
let-binding the type index t
but not the functor f
.
Re-exports
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
Monad (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Functor (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Applicative (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Foldable (Proxy :: Type -> 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 # | |
Traversable (Proxy :: Type -> Type) | Since: base-4.7.0.0 |
Alternative (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
MonadPlus (Proxy :: Type -> Type) | Since: base-4.9.0.0 |
Bounded (Proxy t) | Since: base-4.7.0.0 |
Enum (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 |
Read (Proxy t) | Since: base-4.7.0.0 |
Show (Proxy s) | Since: base-4.7.0.0 |
Ix (Proxy s) | Since: base-4.7.0.0 |
Defined in Data.Proxy | |
Semigroup (Proxy s) | Since: base-4.9.0.0 |
Monoid (Proxy s) | Since: base-4.7.0.0 |