`Unlifted` versus MILU

Learn
#1

(Creating a new thread from State monad - memory exhausted - #27 by doyougnu)

Hi @doyougnu, I wonder if you could help me with something. I have been trying to understand cases where Unlifted has benefits above and beyond Make invalid laziness unrepresentable (MILU). As I mentioned in an earlier comment, nothunks was what originally prompted me to develop the idea of MILU, and achieve a type level guarantee that a value contains no thunks. For Lifted types MILU doesn’t quite imply no thunks, because the value itself may be a thunk! It just implies that once the value is forced it no longer contains any thunks.

Of course, using Unlifted types appropriately can be part of MILU. But I still don’t understand specific cases where using Unlifted types provides more of a benefit than MILU with Lifted types. Do you have any examples?

Something I’ve been wondering about is whether GHC can take advantage of strictness of return types of functions. For example, if I have a function

strictDup !x = (x, x)

can GHC take advantage of the fact that the fields of the tuple are already evaluated after the pair constructor is evaluated? For example, can it avoid an evaluation in

let (y, z) = strictDup x in y + z

From looking at the core, or even the STG, I don’t think so. It still converts to the following:

let (y, z) = strictDup x
in case y of Int# y' ->
  case z of Int# z' ->
    Int# y' z'

and I think the pattern match on Int# requires an attempt at evaluation. In fact I don’t see any way to pattern match in Core or STG without attempting an evaluation too! As far as I can tell, the same holds even for

data StrictPair x y = StrictPair !x !y
strictPair' x = StrictPair x x

Now, if StrictPair were defined to have two Unlifted components then I think the evaluation could in principle be avoided, but again I don’t know if GHC’s intermediate representations are rich enough to express that.

Does anyone have any insight they can share?

#2

This used to be the case, but recently and a bit silently “tag inference” was implemented which goal is exactly to avoid those extra evaluations in most common cases.

Take for example this program:

{-# OPTIONS_GHC -O -ddump-stg-final -dno-typeable-binds -dsuppress-uniques #-}
module T where

{-# NOINLINE strictDup #-}
strictDup !x = (x, x)

foo :: Int -> Int
foo x =
  let (y, z) = strictDup x
  in y + z

If you compile that with a recent GHC (I’m using 9.8.1) you get this output:

==================== Final STG: ====================
T.$wstrictDup [InlPrag=NOINLINE] :: forall {b}. b -> (# b, b #)
[GblId[StrictWorker([!])], Arity=1, Str=<1L>, Unf=OtherCon []] =
    {} \r [x] case x<TagProper> of x1 { __DEFAULT -> (#,#) [x1 x1]; };

T.strictDup [InlPrag=NOINLINE[final]] :: forall {b}. b -> (b, b)
[GblId, Arity=1, Str=<1L>, Cpr=1, Unf=OtherCon []] =
    {} \r [x]
        case case x of x { __DEFAULT -> T.$wstrictDup x; } of {
        (#,#) ww [Occ=Once1] ww1 [Occ=Once1] -> (,) [ww ww1];
        };

T.foo :: GHC.Types.Int -> GHC.Types.Int
[GblId, Arity=1, Str=<1L>, Cpr=1, Unf=OtherCon []] =
    {} \r [x]
        case case x of x { __DEFAULT -> T.$wstrictDup x; } of {
        (#,#) ww [Occ=Once1!] ww1 [Occ=Once1!] ->
        case ww<TagProper> of {
        GHC.Types.I# x1 [Occ=Once1] ->
        case ww1<TagProper> of {
        GHC.Types.I# y [Occ=Once1] ->
        case +# [x1 y] of sat [Occ=Once1] {
        __DEFAULT -> GHC.Types.I# [sat];
        };
        };
        };
        };

There you can see those <TagProper> annotations. I believe those mean that it doesn’t do any evaluation.

1 Like
#3

Ah yes, I do see that appearing in 9.4. I didn’t see it before because I was using -dsuppress-all. Oops! Anyway, that’s a very important feature! If it really works the way I hope then it makes Unlifted types even less important for MILU than I was thinking. If strictness is really visible across function boundaries then forcing it to be visible by using a specific kind is less valuable.

By the way, {-# OPTIONS_GHC -O #-} doesn’t seem to do anything for me. I have to pass -O on the command line to get any optimizations. Does it actually work for you?

#4

I find that often the property that you want to enforce to avoid space leaks is that a type is deep strict.

I think an issue with both MILU and Unlifted is that they only work on the top level. A strict pair, or something that’s wrapped by Unlifted can still contain lazy types, eg, StrictPair (Maybe Int) _ or Unlifted (Maybe Int). And so even if you don’t have thunks directly in the fields of the constructor you can still have them deeper in the structure.

A type is deep strict iff for every field of every constructor, the type of the field is itself deep strict, and the field either has a bang, is a newtype, or is unlifted. Informally, we’ve put bangs on every field recursively.
This corresponds to the class of types where forcing to WHNF forces to NF, which means in terms of thunks that if the top-level term is not a thunk then it doesn’t contain any thunks.

I think stuff like MILU or Unlifted can be helpful for writing types that are deep strict, but they are only means to an end. In order to avoid thunks you want to enforce deep strictness of types.

I have a library that uses template haskell to test whether types are deep strict or not that I’m hoping to publish soon.

4 Likes
#5

Right, one can still design types badly even in the presence of primitives that allow you to design them well. Tools to help check you’ve designed them well are welcome! I look forward to seeing your library. (If the same techniques can be done using the GHC API then it could also be integrated into stan.)

1 Like
#6

Slightly tangentially: if Haskell properly supported levity polymorphism, wouldn’t it also be possible to have IntMap !() have the same representation as IntSet? That’s a lot of potential code deduplication in containers.

#7

Why is IntMap.Strict () not already sufficient for that?

#8

The question is ambiguous, so here are both sides.

Logically it’s because () has a possible state of ⊥, you can hang some evaluations onto that. !() has precisely one state, so if the container exists then it must too, therefore there’s no need to represent it in memory in those cases.

Implementation-wise I think the state right now is that you could have an IntMap (a :: BoxedRep l), but you cannot use the type without first choosing the levity. So GHC indeed could implement this optimization under the current compiler architecture. I however don’t know if there would be a strong reason to use it since it would merely allow sharing the type, all the functions would still need to be declared twice.