-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Plugin to faciliate type-level let
--   
--   For a certain class of programs, type-level let is essential in order
--   to be able to write these programs in such a way that they do not
--   result in ghc core that is quadratic in size. Type-level let is not
--   explicitly supported in ghc, but we can encode it. The
--   <tt>typelet</tt> library provides a type-checker plugin that makes the
--   encoding more convenient to use as well as more effective.
@package typelet
@version 0.1.4

module TypeLet.Plugin
plugin :: Plugin

module TypeLet.UserAPI

-- | Type-level <tt>let</tt>
--   
--   A constraint <tt>Let x t</tt> where <tt>x</tt> is an (existential)
--   type variable and <tt>t</tt> is an arbitrary type represents a
--   type-level let binding <tt>let x = t</tt>.
--   
--   o Introduction form
--   
--   Type-level let bindings should be introduced using <a>letT</a> or its
--   slightly higher level cousin, <a>letAs</a>.
--   
--   o Elimination form
--   
--   To eliminate type-level let, use <a>castEqual</a>.
class Let (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
--   
--   <pre>
--   Let x1 t1
--   Let x2 t2
--   ...
--   </pre>
--   
--   Then if σ is the corresponding idempotent substitution, two types
--   <tt>a</tt> and <tt>b</tt> are considered <a>Equal</a> if <tt>σ(a)</tt>
--   and <tt>σ(b)</tt> are nominally equal.
class Equal (a :: k) (b :: k)

-- | Type-safe cast, using <a>Equal</a> as the notion of equality
--   
--   See discussion of <a>Equal</a> for additional information.
--   
--   Note: without additional <a>Let</a> constraints in scope, <a>Equal</a>
--   constraints simply resolve to unification constraints:
--   
--   <pre>
--   &gt;&gt;&gt; (castEqual :: Int -&gt; Bool) 1
--   ...
--   ...Couldn't match...Int...Bool...
--   ...
--   </pre>
castEqual :: Equal a b => a -> b

-- | <a>LetT</a> is used along with <a>letT</a> to introduce type-level let
--   bindings.
--   
--   See <a>letT</a> for more information.
data LetT (a :: k)
[LetT] :: Let b a => Proxy b -> LetT a

-- | Primitive way to introduce type-level let binding.
--   
--   Usage:
--   
--   <pre>
--   case letT (Proxy @t) of LetT (_ :: Proxy x) -&gt;
--   </pre>
--   
--   This introduces a type-level let binding <tt>x = t</tt>.
letT :: Proxy a -> LetT a

-- | CPS form of <a>letT</a>
--   
--   While this is more convenient to use, the <tt>r</tt> parameter itself
--   requires careful thought; see also <a>constructLet</a>.
letT' :: forall r a. Proxy a -> (forall b. Let b a => Proxy b -> r) -> r

-- | Dual to <a>letAs'</a>
--   
--   Where <a>letAs'</a> <i>takes</i> an existing value and then
--   <i>introduces</i> a type variable, <a>constructLet</a> is used to
--   <i>produce</i> a value and then <i>eliminate</i> a type variable.
--   
--   Consider constructing a heterogenous list <tt>[x, y, z]</tt>. Without
--   the <tt>typelet</tt> library this might look something like
--   
--   <pre>
--   hlist :: HList '[X, Y, Z]
--   hlist =
--       HCons @X @'[Y, Z] x
--     $ HCons @Y @'[   Z] y
--     $ HCons @Z @'[    ] z
--     $ HNil
--   </pre>
--   
--   The problem here is that tail list argument to <tt>HCons</tt>, and
--   causes this example to be quadratic in size. With <tt>letAs'</tt> we
--   could write this as
--   
--   <pre>
--   hlist :: HList '[X, Y, Z]
--   hlist =
--     letAs' (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) -&gt;
--     letAs' (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) -&gt;
--     letAs' (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) -&gt;
--     castEqual xs0
--   </pre>
--   
--   Here we are using <tt>letAs'</tt> 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 <tt>r</tt> to
--   <tt>letAs'</tt>; making that argument explicit, the above code is
--   really this:
--   
--   <pre>
--   hlist :: HList '[X, Y, Z]
--   hlist =
--     letAs' @(HList '[X, Y, Z]) (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) -&gt;
--     letAs' @(HList '[X, Y, Z]) (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) -&gt;
--     letAs' @(HList '[X, Y, Z]) (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) -&gt;
--     castEqual xs0
--   </pre>
--   
--   The solution is to introduce one more type variable for the whole
--   list, and use that as the top-level:
--   
--   <pre>
--   hlist :: HList '[X, Y, Z]
--   hlist = constructLet $ \(_ :: Proxy ts) -&gt;
--     letAs' @(HList ts) (HCons @Z @'[] z Nil) $ \(xs2 :: HList ts2) -&gt;
--     letAs' @(HList ts) (HCons @Y @ts2 y xs2) $ \(xs1 :: HList ts1) -&gt;
--     letAs' @(HList ts) (HCons @X @ts1 x xs1) $ (\xs0 :: HList ts0) -&gt;
--     castEqual xs0
--   </pre>
--   
--   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:
--   
--   <pre>
--   hlist :: HList '[X, Y, Z]
--   hlist = constructLet $
--     letAs' (HCons z Nil) $ \xs2 -&gt;
--     letAs' (HCons y xs2) $ \xs1 -&gt;
--     letAs' (HCons x xs1) $ (xs0 -&gt;
--     castEqual xs0
--   </pre>
constructLet :: forall f a. (forall b. Let b a => Proxy b -> f b) -> f a

-- | Used together with <a>letAs</a> to pair a type-level let binding with
--   a cast
--   
--   See <a>letAs</a> for details.
data LetAs f (a :: k)
[LetAs] :: Let b a => f b -> LetAs f a

-- | Pair a type-level let binding with a cast
--   
--   Often when we introduce a type-level let <tt>x = t</tt>, we then want
--   to cast some term <tt>e :: t</tt> to a term <tt>e :: x</tt>; function
--   <a>letAs</a> does these two things in one operation.
--   
--   If we did the above as written, however, we would have a term <tt>e ::
--   x</tt> where we know nothing about <tt>x</tt> at all (unless we cast
--   again). This is typically not useful; instead, we go from a term <tt>e
--   :: f t</tt> to a term <tt>e :: f x</tt>, let-binding the type index
--   <tt>t</tt> but not the functor <tt>f</tt>.
letAs :: f a -> LetAs f a

-- | CPS form of <a>letAs</a>
--   
--   See also comments for <a>letT'</a>.
letAs' :: forall r f a. f a -> (forall b. Let b a => f b -> r) -> r

-- | <a>Proxy</a> 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, <tt><a>Proxy</a> :: <a>Proxy</a> a</tt> is a safer
--   alternative to the <tt><a>undefined</a> :: a</tt> idiom.
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy (Void, Int -&gt; Int)
--   Proxy
--   </pre>
--   
--   Proxy can even hold types of higher kinds,
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Either
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy Functor
--   Proxy
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; Proxy :: Proxy complicatedStructure
--   Proxy
--   </pre>
data () => Proxy (t :: k)
Proxy :: Proxy (t :: k)
instance forall k (a :: k). TypeLet.UserAPI.Let a a

module TypeLet