Handle unlifted types

[conal]

By default, type variables in GHC are given kind *, i.e., the kind of types of lifted values. Consequently, the polymorphic constructors and definitions in this project are restricted to lifted (boxed) types only. How can we represent reified expressions over unlifted types?

I don't know how severely hampered we'll be in what we can tackle, nor how awkward it will be to avoid unlifted types. For circuit generation and other monomorphic back-ends, I think we'd want to strip away all but unlifted types.

[conal]

See the related discussion "Concrete syntax for open type kind?". A solution to this issue might be to change the representation of kinds as Simon describes in that thread.

[conal]

For now, I've turned back on OnlyLifted in type-encode's Encode module and lambda-ccc's Reify module, so that we won't even try handling unlifted types.

[conal]

Here's an example:

t :: Int
t = 2 * 3

After reification:

t_reified =
  appP
    (appP
       (lamvP# "ds"#
          (lamvP# "ds1"#
             (reifyEP
                (case evalEP (varP# "ds"#) of wild
                   I# x ->
                     case evalEP (varP# "ds1"#) of wild1
                       I# y -> I# ((*#) x y)))))
       (intL (I# 2)))
    (intL (I# 3))
t = evalEP t_reified

The reason reifyEP got stuck here is that it the case alternatives involved unlifted types and so cannot be represented through encoding and decoding. The problem is that encode and decode functions have types that are too restrictive, in that their domain and range must have kind *, not #.

The reason reifyEP got stuck here is that it the case alternatives involved unlifted types and so cannot be represented through encoding and decoding. The problem is that encode and decode functions have types that are too restrictive, in that their domain and range must have kind *, not #. Similarly, descending into expressions of unlifted types, we'd get ill-kinded reifyEP and evalEP applications.

We could make ill-kinded applications of encode, decode, reifyEP, and evalEP, in the hopes that they'd eventually disappear. We'd still run into a fundamental problem, however: all of the type variables in the expression GADT constructors are of kind *.

[andygill]

There are actually two candidate problems, unlifted and unboxed types.

https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/Storage/HeapObjects

[conal]

Thanks for that link. Since we're not using GHC's run-time system (including its heap layout strategies), I think it's only the issue of unlifted types that's a problem here (so far).

Of course, I'll have to think about heaps, etc for the Haskell-to-hardware project, but not just yet.

[andygill]

Both are in Core, for example unlifted tuples vs unboxed Int#s. I'm not sure if it matters, but it was an ah-ha moment when the GHC separated unlifting from unboxing. The problem, as you say, comes down to a kind problem. I'll look for a better, Core specific, link.

[andygill]

Found it. https://ghc.haskell.org/trac/ghc/wiki/IntermediateTypes

Quoted from link: GHC has a relatively complicated kind structure...

There's a little subtyping at the kind level. Here is the picture for type-kinds (kinds of sort TY).

     ?
    / \
   /   \
  ??   (#)
 /  \
*   #

  where 
    *    [LiftedTypeKind]   means boxed type
    #    [UnliftedTypeKind] means unboxed type
    (#)  [UbxTupleKind]     means unboxed tuple
    ??   [ArgTypeKind]      is the lub of *,#
    ?    [OpenTypeKind] means any type at all

In particular:

error :: forall a:?. String -> a
(->)  :: ?? -> ? -> *
(\(x::t) -> ...)    Here t::?? (i.e. not unboxed tuple)

[conal]

Simon PJ mentions this hierarchy in the discussion "Concrete syntax for open type kind?", saying "... they are a gross hack, with many messy consequences. Particularly the necessary sub-kinding, and the impact on inference. I'm not proud of it." Simon then suggests a neater formulation, which I think would neatly resolve the issue with unlifted types and reification, since the type variables in the expression GADT could all have the kind that he calls Type bv, which is equivalent to either * or # --- exactly what we're looking for here.

[conal]

Both are in Core, for example unlifted tuples vs unboxed Int#s.

And, IIUC, unboxed things are necessarily unlifted. The difficulty I'm having with Int# is that it's unlifted, not that it's unboxed in GHC's RTS.

[andygill]

Ahh - good. You seem to have a better handle on this that I have. So the problem is just the two-kind problem.