TypeLet.UserAPI

Main classes

class Let (a :: k) (b :: k)

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)

Reflexivity

A constraint Let x t, where x is an existential (skolem) type variable and t is an arbitrary type, models a type-level let x = t. There is only a single instance for Let: reflexivity (a type is equal to itself).

User code normally does not work with Let directly, but instead uses one of the introduction forms (letT and letAs) which take care to introduce Let constraints of the right shape. When Let constraints are introduced manually, the plugin will report a type error if

• The left-hand side is not a type variable

>>> let aux :: Let Int Int => () ; aux = castEqual () in aux
...
...Let with non-variable LHS...
...

>>> :{
  \(x :: a) ->
    let
      y :: Let a Int => a
      y = castEqual (1 :: Int)
    in y
:}
...
...Let with non-variable LHS...
...

• The set of let-bindings in scope are cyclic.

>>> :{
  let cycle :: (Let a b, Let b a) => (a, b) -> (a, b)
      cycle (a, b) = (castEqual b, castEqual a)
  in cycle ('a', 'b')
:}
...
...Cycle in type-level let bindings: a := b, b := a
...

Defined in TypeLet.UserAPI

class Equal (a :: k) (b :: k)

(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.

castEqual :: Equal a b => a -> b

Type-safe cast, using Equal as the notion of equality

See discussion of Equal for additional information.

Note: without additional Let constraints in scope, Equal constraints simply resolve to unification constraints:

>>> (castEqual :: Int -> Bool) 1
...
...Couldn't match...Int...Bool...
...

Introduction forms

data LetT (a :: k) where

LetT is used along with letT to introduce type-level let bindings.

See letT for more information.

Constructors

LetT :: Let b a => Proxy b -> LetT a

letT :: Proxy a -> LetT a

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

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

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 top-level:

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

data LetAs f (a :: k) where

Used together with letAs to pair a type-level let binding with a cast

See letAs for details.

Constructors

LetAs :: Let b a => f b -> LetAs f a

letAs :: f a -> LetAs f a

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.

letAs' :: forall r f a. f a -> (forall b. Let b a => f b -> r) -> r

CPS form of letAs

See also comments for letT'.

Re-exports

data Proxy (t :: 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

Foldable (Proxy :: TYPE LiftedRep -> Type)

Since: base-4.7.0.0

Defined in Data.Foldable

Methods

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

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 :: Type -> Type)

Since: base-4.7.0.0

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 :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

empty :: Proxy a

(<|>) :: Proxy a -> Proxy a -> Proxy a

some :: Proxy a -> Proxy [a]

many :: Proxy a -> Proxy [a]

Applicative (Proxy :: Type -> Type)

Since: base-4.7.0.0

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

Functor (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

fmap :: (a -> b) -> Proxy a -> Proxy b

(<$) :: a -> Proxy b -> Proxy a

Monad (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b

(>>) :: Proxy a -> Proxy b -> Proxy b

return :: a -> Proxy a

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

mzero :: Proxy a

mplus :: Proxy a -> Proxy a -> Proxy a

Monoid (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

mempty :: Proxy s

mappend :: Proxy s -> Proxy s -> Proxy s

mconcat :: [Proxy s] -> Proxy s

Semigroup (Proxy s)

Since: base-4.9.0.0

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

Bounded (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

minBound :: Proxy t

maxBound :: Proxy t

Enum (Proxy s)

Since: base-4.7.0.0

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]

Ix (Proxy s)

Since: base-4.7.0.0

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

Read (Proxy t)

Since: base-4.7.0.0

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

Defined in Data.Proxy

Methods

showsPrec :: Int -> Proxy s -> ShowS

show :: Proxy s -> String

showList :: [Proxy s] -> ShowS

Eq (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(==) :: Proxy s -> Proxy s -> Bool

(/=) :: Proxy s -> Proxy s -> Bool

Ord (Proxy s)

Since: base-4.7.0.0

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