Add force and delay to typed plutus core

[phadej]

Describe the feature you'd like

force and delay are introduced to UPLC to reduce code size, an option would been to use unit abstraction and application.

I don't see a reason why same construct cannot be introduced to typed PLC for the same reason.

For example, there are expressions like (in pseudo-Haskell syntax):

(force ifThenElse)
  ((builtin equalsInteger) ...)
  (\unused -> ...)
  (\unused -> ...)
  ()

instead of

(force (force ifThenElse)
  ((builtin equalsInteger) ...)
  (delay (...))
  (delay (...)))

The difference is small, and I don't expect it (alone) to affect script size or performance, but it feels a right thing to do.

[michaelpj]

This is indeed very easy, and I thought about doing it, indeed I have a patch for it. In the end we decided that it is strictly redundant since you can use trivial type abstractions and instantiations, which erase to delay and force. Given that we've tried very hard to keep the number of terms in PLC to a minimum, I couldn't quite justify it.

[phadej]

Should the compiler then use trivial type-abstractions and instantiations rather than term-level abstractions? That indeed will have the same effect on UPLC.

[michaelpj]

It does. There's one place where it has to use term abstractions is in the handling of some recursive values.

[michaelpj]

Unless I've missed something.

[phadej]

I made a plutus-apps test suite dump uniswap.pir:

diff --git a/plutus-use-cases/test/Spec/Uniswap.hs b/plutus-use-cases/test/Spec/Uniswap.hs
index d8c55205b..0bda564a7 100644
--- a/plutus-use-cases/test/Spec/Uniswap.hs
+++ b/plutus-use-cases/test/Spec/Uniswap.hs
@@ -1,11 +1,14 @@
+{-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell   #-}
 module Spec.Uniswap(
     tests
     ) where

 import           Plutus.Contract.Test
-import qualified Plutus.Contracts.Uniswap.Trace as Uniswap
-import qualified Plutus.Trace.Emulator          as Trace
+import qualified Plutus.Contracts.Uniswap as Uniswap
+import qualified Plutus.Trace.Emulator    as Trace
+import qualified PlutusTx

 import           Test.Tasty

@@ -17,4 +20,6 @@ tests = testGroup "uniswap" [
                        "setupTokens contract should be still running"
         .&&. assertNoFailedTransactions)
         Uniswap.uniswapTrace
+
+    , goldenPir "test/Spec/uniswap.pir" $$(PlutusTx.compile [|| Uniswap.mkUniswapValidator ||])
     ]

and then there are bindings like:

(termbind
  (strict)
  (vardecl fail (fun (all a (type) a) TxOut))
  (lam
    ds
    (all a (type) a)
    [
      { error TxOut }
      [
        {
          [
            Unit_match
            [
              [
                { (builtin trace) Unit }
                (con string "expected exactly one Uniswap output")
              ]
              Unit
            ]
          ]
          (con unit)
        }
        (con unit ())
      ]
    ]
  )

and

[
  [
    [
      [
        {
          (builtin ifThenElse)
          (fun
            (con unit)
            [
              [ Tuple2 (con bytestring) ]
              (con bytestring)
            ]
          )
        }
        [
          [
            (builtin equalsInteger)
            [
              {
                {
                  (builtin fstPair)
                  (con integer)
                }
                [ (con list) (con data) ]
              }
              tup
            ]
          ]
          (con integer 0)
        ]
      ]
      (lam
        ds
        (con unit)
        [
          [
            {
              { Tuple2 (con bytestring) }
              (con bytestring)
            }
            [
              (builtin unBData)
              [
                {
                  (builtin headList) (con data)
                }
                t
              ]
            ]
          ]
          [
            (builtin unBData)
            [
              { (builtin headList) (con data) }
              [
                {
                  (builtin tailList) (con data)
                }
                t
              ]
            ]
          ]
        ]
      )
    ]
    (lam
      ds
      (con unit)
      [
        {
          error
          [
            [ Tuple2 (con bytestring) ]
            (con bytestring)
          ]
        }
        [
          {
            [
              Unit_match
              [
                [
                  { (builtin trace) Unit }
                  (con string "PT1")
                ]
                Unit
              ]
            ]
            (con unit)
          }
          (con unit ())
        ]
      ]
    )
  ]
  (con unit ())
]

[michaelpj]

Some of these may come from surface Haskell: there are some places in the source where we use unit lambdas instead of type abstractions for simplicity. I'll have a bit more of a look into this later, though.

[effectfully]

This doesn't seem to be a high priority issue, although I agree it would be great to take a deep look at it.

[effectfully]

Closing in favor of #5908.