Experiments, investigations and curiosities

[effectfully]

Dump here everything that fits the description of the discussion.

[effectfully]

#7278 was an attempt to ditch relying on laziness for building partial builtin applications in the CEK machine and instead just keeping the arguments directly as values without discharging them. The gist of the change:

+data PartialBuiltinApp uni fun
+    = PartialBuiltinHead fun
+    | PartialBuiltinTyInst (PartialBuiltinApp uni fun) (Type TyName uni ())
+    | PartialBuiltinApply (PartialBuiltinApp uni fun) (CkValue uni fun)

enterComputeCek = computeCek where
    applyEvaluate !ctx (VBuiltin fun app runtime) arg = do
-       let argTerm = dischargeResultToTerm $ dischargeCekValue arg
-           app' = Apply () app argTerm
+       let app' = PartialBuiltinApply app arg
        case runtime of
            BuiltinExpectArgument f ->
                evalBuiltinApp ctx fun app' $ f arg

But apparently constructing that PartialBuiltinApply is more expensive than relying on laziness like we currently do. Not by a whole lot, but introducing a performance degradation here is perhaps not worth it.

[effectfully]

#7210 made UPLC case-of-case less restrictive by allowing it to produce duplicate branches if they're small enough.

Quoting Note [Case-of-case and duplicating code]:

Case-of-case can duplicate code.

Consider this schematic example:

case (case s of { C1 a -> x; C2 b -> y; }) of
  D1 -> w
  D2 -> z

-->
 
case s of
  C1 a -> case x of { D1 -> w; D2 -> z; }
  C2 b -> case y of { D1 -> w; D2 -> z; }

We duplicate the outer case (the matcher application, importantly including
the branches) for every branch of the inner case.

Any time we duplicate code we run the risk of exponential program growth,
since we might apply case-of-case inside the duplicated parts of the
program, thus leading to multiplicative growth. In particular, since we apply
case-of-case in a bottom-up fashion, we can apply it inside a subterm (creating
duplication), and then in the main term (multiplying the duplication) in a single
pass. This is not too bad so long as case-of-known-constructor will clear
things up afterwards, but is something to be aware of.

If the inner branch bodies are conapps (see Note [Case-of-case and conapps]) then
that will reduce but not necessarily eliminate the duplication. Consider

case (case s of { C1 a -> True; C2 b -> True; C3 c -> False }) of
  True -> v
  False -> w
 
--> (case-of-case)
 
case s of
  C1 a -> case True of { True -> v; False -> w; }
  C2 b -> case True of { True -> v; False -> w; }
  C3 c -> case False of { True -> v; False -> w; }

--> (case-of-known-constructor)
 
case s of
  C1 a -> v
  C2 b -> v
  C3 c -> w

i.e. we still duplicate v! If however the conapps are all distinct constructors then
this won't happen.

We can mitigate the problem by binding the potentially-duplicated code to a variable
instead:

case (case s of { C1 a -> x; C2 b -> y; }) of
  D1 -> w
  D2 -> z
 
-->
 
let k_caseOfCase = \x -> case x of { D1 -> w; D2 -> z; }
in case s of
  C1 a -> k_caseOfCase x
  C2 b -> k_caseOfCase y

This avoids the code growth but is less good as an optimization, unless we can rely
on the inliner to see these as good inlining opportunities, which we currently can't.

So in UPLC we disallowed

case (case s of { C1 a -> True; C2 b -> True; C3 c -> False }) of
  True -> v
  False -> w

entirely because of the double occurrence of True, however if v is small enough, then it's safe to duplicate it, so #7210 implemented size-checking logic. The result was that it made absolutely no difference on any of the existing tests, so wasn't worth complicating the implementation of case-of-case.

The gist of the PR for reference:

+-- >>> annotateIsDuplicatedOn id "abacdeffdbdg"
+-- [('a',True),('b',True),('a',True),('c',False),('d',True),('e',False),('f',True),('f',True),('d',True),('b',True),('d',True),('g',False)]
+annotateIsDuplicatedOn :: (Functor f, Foldable f, Hashable b) => (a -> b) -> f a -> f (a, Bool)
+annotateIsDuplicatedOn = <...>

processTerm = \case
  original@(Case annOuter (Case annInner scrut altsInner) altsOuter) ->
    maybe
      original
      (Case annInner scrut)
      (do
-        constrs <- for altsInner $ \case
+        constrsDupl <- fmap (annotateIsDuplicatedOn fst) . for altsInner $ \case
          c@(Constr _ i _)   -> Just (Left i, c)
          c@(Constant _ val) -> Just (Right val, c)
          _                  -> Nothing
-        guard $ length (nub . toList $ fmap fst constrs) == length constrs
-        pure $ constrs <&> \(_, c) -> CaseReduce.processTerm $ Case annOuter c altsOuter)
+        for constrsDupl $ \((_, c), dupl) -> do
+            let alt = CaseReduce.processTerm $ Case annOuter c altsOuter
+            guard $ not dupl || termSize alt <= 300  -- Not duplicated or size is under a certain threshold.
+            pure alt)

[effectfully]

#6793 was an attempt to add Fix to the AST with the expected operational semantics:

        body ~> bodyV
----------------------------- (1)
fix rec body ~> fix rec bodyV

                  <empty>
-------------------------------------------- (2)
fix rec bodyV ~> [fix rec bodyV / rec] bodyV

The implementation was made as fast as possible with some really complicated tie-the-know implementation:

1. In computeCek we save the current size of the environment in FrameFix and proceed to evaluate the body in the current environment extended with a VBlackHole. VBlackHole is a new kind of CekValue that we add to provide a value for the recursive call while we're evaluating the body of a fixpoint to a value. If while evaluating the body we reach VBlackHole, we know that this is infinite recursion and terminate the program earlier. The name is inspired by black holes in GHC, which are thunks being evaluated (and evaluation of a thunk runs into a blackhole, that is also a loop and the Haskell program terminates).
2. Once we've evaluated the body, we need to update the rec :=> VBlackHole environment entry by replacing VBlackHole with an actual value for rec, for that I added contUpdateZero (similar to contIndexZero). At that point we might have added new entries to the environment and so we need to calculate the De Bruijn index of rec in the environment by subtracting the old size of the environment from the new one.
3. We completely discharge FrameFix in returnCek without creating any new frames. We're able to achieve that because we encode recursion through a circular object: env' refers to bodyV' and vice versa -- this is an actual loop in memory. The idea here is to make the environment of bodyV' contain bodyV' itself, including its environment containing bodyV', including its environment...

The conclusion was:

Yet, even with such a performance-focused design the results are very underwhelming: nofib isn't detectably faster. The lists benchmarks are faster by up to 14.5%, which is normally a very welcome improvement, but given that we're adding an entire new AST node (with very non-trivial evaluation rules), is it worth it?

Note that we don't save much size either, this is what replacing the Z combinator with native recursion in a script amounts to:

[effectfully]

#6706 was an experiment replacing NamedDeBruijn with DeBruijn everywhere on the evaluation path to see how much names cost us.

The conclusion:

It appears that this PR somehow slows down the evaluator, while speeding up preparation, hence why we see results all over the place. How can it possibly slow down the evaluator? I have no idea, but this is likely me screwing something up, because I can't think of a way to make things slower by removing redundant code.

The experiment is over, so I'm closing this PR, but we need to make sure to investigate this weirdness in future.

We do need to come back to this at some point, if only to explain this weirdness.

[effectfully]

#4462, #4463 and #6352 were all attempts to speed up geq in PlutusCore.Default.Universe. Currently geq only inlines for non-polymorphic built-in types, e.g. Bool and Integer and notably NOT [Integer] or (Bool, ()) etc. It'd be good to inline geq for monomorphized polymorphic built-in types too, so that we don't have redundant geqRec calls, here's for example how the Core looks for ListData right now:

DefaultUniApply co6_i8od6 f4_i8od7 x12_i8od8 ->
  case geqRec $WDefaultUniProtoList f4_i8od7 of
    Nothing -> builtinRuntimeFailure <...>
    Just x9_i8odc ->
      let! { Refl co7_i8odf ~ <- x9_i8odc } in
      case geqRec $WDefaultUniData x12_i8od8 of
        Nothing -> builtinRuntimeFailure <...>
        Just x10_i8odj ->
        let! { Refl co8_i8odm ~ <- x10_i8odj } in
          <...>

Inlining those turned out to be a pretty annoying thing to do. #4462 is the most successful attempt and it's fairly simple too, it amounts to changing GEq

class GEq f where
    geq :: f a -> f b -> Maybe (a :~: b)

to a custom GEqL:

+class GEqL f a where
+    geqL :: f b -> Maybe (a :~: b)

-type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEq uni, uni `Contains` a)
+type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEqL uni (Esc a), uni `Contains` a)

(while we're here, we should probably use the strict EvaluationSuccess instead of the lazy Maybe).

It created some pretty annoying boilerplate though, e.g.

+instance GEqL DefaultUni (Esc Bool) where
+    geqL DefaultUniBool = Just Refl
+    geqL _              = Nothing

+instance (GEqL DefaultUni (Esc a), GEqL DefaultUni (Esc b)) => GEqL DefaultUni (Esc (a, b)) where
+    geqL (DefaultUniPair a b) = do
+        Refl <- geqL @DefaultUni @(Esc a) a
+        Refl <- geqL @DefaultUni @(Esc b) b
+        Just Refl
+    geqL _ = Nothing

The boilerplate is tolerable and the speedup is an okayish 1-2% for the validation benchmarks, but all of that will be irrelevant once we split the universe into two as per #4781.

I dunno, maybe we should still do the GEqL change in the meantime. Can we do it with less boilerplate?