Safe Haskell  SafeInferred 

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
 constructLet :: forall f a. (forall b. Let b a => Proxy b > f b) > f a
 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 #
Typelevel let
A constraint Let x t
where x
is an (existential) type variable and t
is an arbitrary type represents a typelevel let binding let x = t
.
o Introduction form
Typelevel let bindings should be introduced using letT
or its slightly
higher level cousin, letAs
.
o Elimination form
To eliminate typelevel 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 typelevel let
This is a class without any definitions; 'Equal a b' is instead proved by the plugin. Suppose we have a bunch of typelevel 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 typelevel let binding.
Usage:
case letT (Proxy @t) of LetT (_ :: Proxy x) >
This introduces a typelevel 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; see also constructLet
.
constructLet :: forall f a. (forall b. Let b a => Proxy b > f b) > f a Source #
Dual to letAs'
Where letAs'
takes an existing value and then introduces a type
variable, constructLet
is used to produce a value and then eliminate a
type variable.
Consider constructing a heterogenous list [x, y, z]
. Without the typelet
library this might look something like
hlist :: HList '[X, Y, Z] hlist = HCons @X @'[Y, Z] x $ HCons @Y @'[ Z] y $ HCons @Z @'[ ] z $ HNil
The problem here is that tail list argument to HCons
, and causes this
example to be quadratic in size. With letAs'
we could write this as
hlist :: HList '[X, Y, Z] hlist = letAs' (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) > letAs' (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) > letAs' (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) > castEqual xs0
Here we are using letAs'
to introduce a type variable for each partial
list, thereby avoiding the repeated lists in the type arguments. However,
if we write it like this, there is an additional repeated list in the
implicit continuation type argument r
to letAs'
; making that argument
explicit, the above code is really this:
hlist :: HList '[X, Y, Z] hlist = letAs' @(HList '[X, Y, Z]) (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) > letAs' @(HList '[X, Y, Z]) (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) > letAs' @(HList '[X, Y, Z]) (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) > castEqual xs0
The solution is to introduce one more type variable for the whole list, and use that as the toplevel:
hlist :: HList '[X, Y, Z] hlist = constructLet $ \(_ :: Proxy ts) > letAs' @(HList ts) (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) > letAs' @(HList ts) (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) > letAs' @(HList ts) (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) > castEqual xs0
Note that none of these type arguments are necessary; we merely showed them to illustrate what is going on. The final example can be written as shown below, and will be linear in size:
hlist :: HList '[X, Y, Z] hlist = constructLet $ letAs' (HCons z Nil) $ \xs2 > letAs' (HCons y xs2) $ \xs1 > letAs' (HCons x xs1) $ (xs0 > castEqual xs0
letAs :: f a > LetAs f a Source #
Pair a typelevel let binding with a cast
Often when we introduce a typelevel 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
,
letbinding the type index t
but not the functor f
.
Reexports
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
Foldable (Proxy :: TYPE LiftedRep > Type)  Since: base4.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: base4.7.0.0 
Alternative (Proxy :: Type > Type)  Since: base4.9.0.0 
Applicative (Proxy :: Type > Type)  Since: base4.7.0.0 
Functor (Proxy :: Type > Type)  Since: base4.7.0.0 
Monad (Proxy :: Type > Type)  Since: base4.7.0.0 
MonadPlus (Proxy :: Type > Type)  Since: base4.9.0.0 
Monoid (Proxy s)  Since: base4.7.0.0 
Semigroup (Proxy s)  Since: base4.9.0.0 
Bounded (Proxy t)  Since: base4.7.0.0 
Enum (Proxy s)  Since: base4.7.0.0 
Ix (Proxy s)  Since: base4.7.0.0 
Defined in Data.Proxy  
Read (Proxy t)  Since: base4.7.0.0 
Show (Proxy s)  Since: base4.7.0.0 
Eq (Proxy s)  Since: base4.7.0.0 
Ord (Proxy s)  Since: base4.7.0.0 