Unlifted data types

[Edward Z. Yang]

Excerpts from Dan Doel's message of 2015-09-05 10:35:44 -0700:
> I tried with `error` first, and it worked exactly the way I described.
> 
> But I guess it's a type inference weirdness. If I annotate mv# with
> MutVar# it will work, whereas otherwise it will be inferred that mv#
> :: a where a :: *, instead of #. Whereas !x is a pattern which
> requires monomorphism of x, and so it figures out mv# :: MutVar# ....
> Kind of an odd corner case where breaking cycles causes things _not_
> to type check, due to open kinds not being first class.
> 
> I thought I remembered that at some point it was decided that `let`
> bindings of unboxed things should be required to have bangs on the
> bindings, to indicate the evaluation order. Maybe I'm thinking of
> something else (was it that it was originally required and we got rid
> of it?).

Ah yes, I added an explicit type signature, which is why I didn't see
your problem.

As for requiring bang, I think probably you are thinking of:

    commit 831a35dd00faff195cf938659c2dd736192b865f
    Author: Ian Lynagh <igloo at earth.li>
    Date:   Fri Apr 24 12:47:54 2009 +0000

        Require a bang pattern when unlifted types are where/let bound; #3182
        For now we only get a warning, rather than an error, because the alex
        and happy templates don't follow the new rules yet.

But Simon eventually made it be less chatty:

    commit 67157c5c25c8044b54419470b5e8cc677be060c3
    Author: simonpj at microsoft.com <unknown>
    Date:   Tue Nov 16 17:18:43 2010 +0000

        Warn a bit less often about unlifted bindings.

        Warn when
           (a) a pattern bindings binds unlifted values
           (b) it has no top-level bang
           (c) the RHS has a *lifted* type

        Clause (c) is new, argued for by Simon M

        Eg     x# = 4# + 4#      -- No warning
               (# a,b #) = blah  -- No warning
               I# x = blah       -- Warning

Since in our cases the RHS is not lifted, no warning occurs.

> > Nope, if you just float the error call out of MV, you will go from
> > "Okay." to an exception.  Notice that *data constructors* are what are
> > used to induce suspension.  This is why we don't have a 'suspend'
> > special form; instead, 'Box' is used directly.
> 
> I know that it's the floating that makes a difference, not the bang
> pattern. The point would be to make the syntax require the bang
> pattern to give a visual indication of when it happens, and make it
> illegal to look like you're doing a normal let that doesn't change the
> value (although having it actually be a bang pattern would be bad,
> because it'd restrict polymorphism of the definition).

I think this is a reasonable thing to ask for. I also think, with the
commit set above, this very discussion happened in 2010, and was
resolved in favor of not warning in this case for unboxed types.

Maybe the situation is different with unlifted data types; it's hard
for me to tell.

> Also, the constructor isn't exactly relevant, so much as whether the
> unlifted error occurs inside the definition of a lifted thing. For
> instance, we can go from:
> 
>     let mv = MutVar undefined
> 
> to:
> 
>     let mv = let mv# :: MutVar# RealWorld a ; mv# = undefined in MutVar mv#
> 
> and the result is the same, because it is the definition of mv that is
> lazy. Constructors in complex expressions---and all subexpressions for
> that matter---just get compiled this way. E.G.
> 
>     let f :: MutVar# RealWorld a -> MutVar a
>         f mv# = f mv#
>     in flip const (f undefined) $ putStrLn "okay"
> 
> No constructors involved, but no error.

Yes, you are right. I incorrectly surmised that a suspension function
would have to be special form, but in fact, it does not need to be.

> Okay. So, there isn't representational overhead, but there is
> overhead, where you call a function or something (which will just
> return its argument), whereas newtype constructors end up not having
> any cost whatsoever?

You might hope that it can get inlined away. But yes, a coercion would
be best.

Edward