diff --git a/.gitignore b/.gitignore
index 36f5659ea..6bd616d62 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 /result*
 /dist-newstyle
 .direnv
+bench.csv
\ No newline at end of file
diff --git a/Plutarch.hs b/Plutarch.hs
index 4d2a771c0..76d5ede57 100644
--- a/Plutarch.hs
+++ b/Plutarch.hs
@@ -22,9 +22,8 @@ module Plutarch (
   PI.punsafeConstant,
   PI.Term,
   PI.TermCont (..),
-  PL.plift,
-  PL.pconstant,
-  PL.plift',
+  PI.S,
+  PI.PType,
   PlutusType (..),
   printTerm,
   printScript,
@@ -40,13 +39,10 @@ module Plutarch (
   popaque,
   punsafeFromOpaque,
   plam,
-  -- $plam
 ) where
 
-import Data.Kind (Type)
-import Plutarch.Internal (ClosedTerm, Term, compile, papp, phoistAcyclic, plam', punsafeCoerce, (:-->))
+import Plutarch.Internal (ClosedTerm, PType, Term, compile, papp, phoistAcyclic, plam', punsafeCoerce, (:-->))
 import qualified Plutarch.Internal as PI
-import qualified Plutarch.Lift as PL
 import Plutus.V1.Ledger.Scripts (Script (Script))
 import PlutusCore.Pretty (prettyPlcReadableDebug)
 
@@ -139,7 +135,7 @@ pinl v f = f v
 
   A simple example, encoding a Sum type as an Enum via PInteger:
 
-  > data AB (s :: k) = A | B
+  > data AB (s :: S) = A | B
   >
   > instance PlutusType AB where
   >   type PInner AB _ = PInteger
@@ -161,10 +157,10 @@ pinl v f = f v
 
   Further examples can be found in examples/PlutusType.hs
 -}
-class (PCon a, PMatch a) => PlutusType (a :: k -> Type) where
+class (PCon a, PMatch a) => PlutusType (a :: PType) where
   -- `b' :: k'` causes GHC to fail type checking at various places
   -- due to not being able to expand the type family.
-  type PInner a (b' :: k -> Type) :: k -> Type
+  type PInner a (b' :: PType) :: PType
   pcon' :: forall s. a s -> forall b. Term s (PInner a b)
   pmatch' :: forall s c. (forall b. Term s (PInner a b)) -> (a s -> Term s c) -> Term s c
 
diff --git a/Plutarch/Api/V1.hs b/Plutarch/Api/V1.hs
index 59ff67574..0b2738d01 100644
--- a/Plutarch/Api/V1.hs
+++ b/Plutarch/Api/V1.hs
@@ -86,7 +86,7 @@ type PTuple = PDataList
 
 ---------- V1 Specific types, Incompatible with V2
 
-newtype PTxInfo (s :: k)
+newtype PTxInfo (s :: S)
   = PTxInfo
       ( Term
           s
@@ -126,7 +126,7 @@ instance PIsDataRepr PTxInfo where
   pmatchRepr dat f =
     (pmatchDataRepr dat) ((DRHCons (f . PTxInfo)) $ DRHNil)
 
-newtype PScriptContext (s :: k)
+newtype PScriptContext (s :: S)
   = PScriptContext (Term s (PDataList '[PTxInfo, PScriptPurpose]))
   deriving
     (PMatch, PIsData, PUnsafeLiftDecl Plutus.ScriptContext)
@@ -144,7 +144,7 @@ instance PIsDataRepr PScriptContext where
 
 -- General types, used by V1 and V2
 
-data PScriptPurpose (s :: k)
+data PScriptPurpose (s :: S)
   = PMinting (Term s (PDataList '[PCurrencySymbol]))
   | PSpending (Term s (PDataList '[PTxOutRef]))
   | PRewarding (Term s (PDataList '[PStakingCredential]))
@@ -173,60 +173,60 @@ instance PIsDataRepr PScriptPurpose where
 
 ---------- Scripts
 
-newtype PDatum (s :: k) = PDatum (Term s PData)
+newtype PDatum (s :: S) = PDatum (Term s PData)
   deriving (PIsData, PEq) via PData
 
-newtype PRedeemer (s :: k) = PRedeemer (Term s PData)
+newtype PRedeemer (s :: S) = PRedeemer (Term s PData)
   deriving (PIsData, PEq) via PData
 
-newtype PDatumHash (s :: k)
+newtype PDatumHash (s :: S)
   = PDatumHash (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
-newtype PStakeValidatorHash (s :: k)
+newtype PStakeValidatorHash (s :: S)
   = PStakeValidatorHash (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
-newtype PRedeemerHash (s :: k)
+newtype PRedeemerHash (s :: S)
   = PRedeemerHash (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
-newtype PValidatorHash (s :: k)
+newtype PValidatorHash (s :: S)
   = PValidatorHash (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
 ---------- Value
 
-newtype PTokenName (s :: k)
+newtype PTokenName (s :: S)
   = PTokenName (Term s PByteString)
   deriving (PEq, POrd, PIsData) via (PByteString)
   deriving newtype (Semigroup, Monoid)
 
-newtype PValue (s :: k)
+newtype PValue (s :: S)
   = PValue (Term s (PMap PCurrencySymbol (PMap PTokenName PInteger)))
   deriving (PIsData) via (PMap PCurrencySymbol (PMap PTokenName PInteger))
 
-newtype PCurrencySymbol (s :: k)
+newtype PCurrencySymbol (s :: S)
   = PCurrencySymbol (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
 ---------- Crypto
 
-newtype PPubKeyHash (s :: k)
+newtype PPubKeyHash (s :: S)
   = PPubKeyHash (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
-newtype PPubKey (s :: k)
+newtype PPubKey (s :: S)
   = PPubKey (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
-newtype PSignature (s :: k)
+newtype PSignature (s :: S)
   = PSignature (Term s PByteString)
   deriving (PEq, POrd, PIsData) via PByteString
 
 ---------- Time
 
-newtype PPOSIXTime (s :: k)
+newtype PPOSIXTime (s :: S)
   = PPOSIXTime (Term s PInteger)
   deriving (POrd, PEq, PIntegral, PIsData) via (PInteger)
   deriving newtype (Num)
@@ -237,7 +237,7 @@ type PPOSIXTimeRange = PInterval PPOSIXTime
 
 type PClosure = PBool
 
-newtype PInterval a (s :: k)
+newtype PInterval a (s :: S)
   = PInterval
       ( Term
           s
@@ -267,7 +267,7 @@ instance PIsDataRepr (PInterval a) where
     pmatchDataRepr dat $
       DRHCons (f . PInterval) DRHNil
 
-newtype PLowerBound a (s :: k)
+newtype PLowerBound a (s :: S)
   = PLowerBound (Term s (PDataList '[PExtended a, PClosure]))
   deriving
     ( PMatch
@@ -290,7 +290,7 @@ instance PIsDataRepr (PLowerBound a) where
     pmatchDataRepr dat $
       DRHCons (f . PLowerBound) DRHNil
 
-newtype PUpperBound a (s :: k)
+newtype PUpperBound a (s :: S)
   = PUpperBound (Term s (PDataList '[PExtended a, PClosure]))
   deriving
     ( PMatch
@@ -312,7 +312,7 @@ instance PIsDataRepr (PUpperBound a) where
     pmatchDataRepr dat $
       DRHCons (f . PUpperBound) DRHNil
 
-data PExtended a (s :: k)
+data PExtended a (s :: S)
   = PNegInf (Term s (PDataList '[]))
   | PFinite (Term s (PDataList '[a]))
   | PPosInf (Term s (PDataList '[]))
@@ -335,7 +335,7 @@ instance PIsDataRepr (PExtended a) where
 
 ---------- Tx/Address
 
-data PCredential (s :: k)
+data PCredential (s :: S)
   = PPubKeyCredential (Term s (PDataList '[PPubKeyHash]))
   | PScriptCredential (Term s (PDataList '[PValidatorHash]))
   deriving
@@ -356,7 +356,7 @@ instance PIsDataRepr PCredential where
           (f . PScriptCredential)
           DRHNil
 
-data PStakingCredential (s :: k)
+data PStakingCredential (s :: S)
   = PStakingHash (Term s (PDataList '[PCredential]))
   | PStakingPtr (Term s (PDataList '[PInteger, PInteger, PInteger]))
   deriving
@@ -377,7 +377,7 @@ instance PIsDataRepr PStakingCredential where
       DRHCons (f . PStakingHash) $
         DRHCons (f . PStakingPtr) DRHNil
 
-newtype PAddress (s :: k)
+newtype PAddress (s :: S)
   = PAddress
       ( Term
           s
@@ -405,7 +405,7 @@ instance PIsDataRepr PAddress where
 
 ---------- Tx
 
-newtype PTxId (s :: k)
+newtype PTxId (s :: S)
   = PTxId (Term s (PDataList '[PByteString]))
   deriving
     (PMatch, PIsData, PUnsafeLiftDecl Plutus.TxId)
@@ -418,7 +418,7 @@ instance PIsDataRepr PTxId where
     pmatchDataRepr dat $
       DRHCons (f . PTxId) DRHNil
 
-newtype PTxOutRef (s :: k)
+newtype PTxOutRef (s :: S)
   = PTxOutRef (Term s (PDataList '[PTxId, PInteger]))
   deriving
     (PMatch, PIsData, PUnsafeLiftDecl Plutus.TxOutRef)
@@ -431,7 +431,7 @@ instance PIsDataRepr PTxOutRef where
     pmatchDataRepr dat $
       DRHCons (f . PTxOutRef) DRHNil
 
-newtype PTxInInfo (s :: k)
+newtype PTxInInfo (s :: S)
   = PTxInInfo (Term s (PDataList '[PTxOutRef, PTxOut]))
   deriving
     (PMatch, PIsData, PUnsafeLiftDecl Plutus.TxInfo)
@@ -444,7 +444,7 @@ instance PIsDataRepr PTxInInfo where
     pmatchDataRepr dat $
       DRHCons (f . PTxInInfo) DRHNil
 
-newtype PTxOut (s :: k)
+newtype PTxOut (s :: S)
   = PTxOut
       ( Term
           s
@@ -472,7 +472,7 @@ instance PIsDataRepr PTxOut where
     pmatchDataRepr dat $
       DRHCons (f . PTxOut) DRHNil
 
-data PDCert (s :: k)
+data PDCert (s :: S)
   = PDCertDelegRegKey (Term s (PDataList '[PStakingCredential]))
   | PDCertDelegDeRegKey (Term s (PDataList '[PStakingCredential]))
   | PDCertDelegDelegate (Term s (PDataList '[PStakingCredential, PPubKeyHash]))
@@ -508,13 +508,13 @@ instance PIsDataRepr PDCert where
 
 ---------- AssocMap
 
-newtype PMap (a :: k -> Type) (b :: k -> Type) (s :: k)
+newtype PMap (a :: PType) (b :: PType) (s :: S)
   = PMap (Term s (PBuiltinMap a b))
   deriving (PIsData) via (PBuiltinMap a b)
 
 ---------- Others
 
-data PMaybe a (s :: k)
+data PMaybe a (s :: S)
   = PNothing (Term s (PDataList '[]))
   | PJust (Term s (PDataList '[a]))
   deriving
@@ -531,7 +531,7 @@ instance PIsDataRepr (PMaybe a) where
       DRHCons (f . PNothing) $
         DRHCons (f . PJust) DRHNil
 
-data PEither a b (s :: k)
+data PEither a b (s :: S)
   = PLeft (Term s (PDataList '[a]))
   | PRight (Term s (PDataList '[b]))
   deriving
diff --git a/Plutarch/Builtin.hs b/Plutarch/Builtin.hs
index 280b8ac28..b4ea0829f 100644
--- a/Plutarch/Builtin.hs
+++ b/Plutarch/Builtin.hs
@@ -33,16 +33,16 @@ import qualified PlutusCore as PLC
 import PlutusTx (Data)
 
 -- | Plutus 'BuiltinPair'
-data PBuiltinPair (a :: k -> Type) (b :: k -> Type) (s :: k)
+data PBuiltinPair (a :: PType) (b :: PType) (s :: S)
 
 -- FIXME: figure out good way of deriving this
 instance (PUnsafeLiftDecl ah a, PUnsafeLiftDecl bh b) => PUnsafeLiftDecl (ah, bh) (PBuiltinPair a b) where
   type PLiftedRepr (PBuiltinPair a b) = (PLiftedRepr a, PLiftedRepr b)
   type PLifted (PBuiltinPair a b) = (PLifted a, PLifted b)
-  pliftToRepr (x, y) = (pliftToRepr @_ @_ @a x, pliftToRepr @_ @_ @b y)
+  pliftToRepr (x, y) = (pliftToRepr @_ @a x, pliftToRepr @_ @b y)
   pliftFromRepr (x, y) = do
-    x' <- pliftFromRepr @_ @_ @a x
-    y' <- pliftFromRepr @_ @_ @b y
+    x' <- pliftFromRepr @_ @a x
+    y' <- pliftFromRepr @_ @b y
     Just (x', y')
 
 pfstBuiltin :: Term s (PBuiltinPair a b :--> a)
@@ -59,7 +59,7 @@ ppairDataBuiltin :: Term s (PAsData a :--> PAsData b :--> PBuiltinPair (PAsData
 ppairDataBuiltin = punsafeBuiltin PLC.MkPairData
 
 -- | Plutus 'BuiltinList'
-data PBuiltinList (a :: k -> Type) (s :: k)
+data PBuiltinList (a :: PType) (s :: S)
   = PCons (Term s a) (Term s (PBuiltinList a))
   | PNil
 
@@ -81,8 +81,8 @@ pconsBuiltin = phoistAcyclic $ pforce $ punsafeBuiltin PLC.MkCons
 instance PUnsafeLiftDecl ah a => PUnsafeLiftDecl [ah] (PBuiltinList a) where
   type PLifted (PBuiltinList a) = [PLifted a]
   type PLiftedRepr (PBuiltinList a) = [PLiftedRepr a]
-  pliftToRepr x = pliftToRepr @_ @_ @a <$> x
-  pliftFromRepr x = traverse (pliftFromRepr @_ @_ @a) x
+  pliftToRepr x = pliftToRepr @_ @a <$> x
+  pliftFromRepr x = traverse (pliftFromRepr @_ @a) x
 
 instance PLift a => PlutusType (PBuiltinList a) where
   type PInner (PBuiltinList a) _ = PBuiltinList a
@@ -150,7 +150,15 @@ pasByteStr = punsafeBuiltin PLC.UnBData
 pdataLiteral :: Data -> Term s PData
 pdataLiteral = pconstant
 
-data PAsData (a :: k -> Type) (s :: k)
+data PAsData (a :: PType) (s :: S)
+
+data PAsDataLifted (a :: PType)
+
+instance PUnsafeLiftDecl (PAsDataLifted a) (PAsData a) where
+  type PLifted (PAsData a) = PAsDataLifted a
+  type PLiftedRepr (PAsData a) = Data
+  pliftToRepr = \case
+  pliftFromRepr _ = Nothing
 
 pforgetData :: Term s (PAsData a) -> Term s PData
 pforgetData = punsafeCoerce
diff --git a/Plutarch/DataRepr.hs b/Plutarch/DataRepr.hs
index 8411c3e9b..8d863064d 100644
--- a/Plutarch/DataRepr.hs
+++ b/Plutarch/DataRepr.hs
@@ -28,7 +28,7 @@ import Plutarch.Prelude
 import qualified Plutus.V1.Ledger.Api as Ledger
 import qualified PlutusCore as PLC
 
-data PDataList (as :: [k -> Type]) (s :: k)
+data PDataList (as :: [PType]) (s :: S)
 
 pdhead :: Term s (PDataList (a : as) :--> PAsData a)
 pdhead = phoistAcyclic $ pforce $ punsafeBuiltin PLC.HeadList
@@ -36,8 +36,8 @@ pdhead = phoistAcyclic $ pforce $ punsafeBuiltin PLC.HeadList
 pdtail :: Term s (PDataList (a : as) :--> PDataList as)
 pdtail = phoistAcyclic $ pforce $ punsafeBuiltin PLC.TailList
 
-type PDataRepr :: [[k -> Type]] -> k -> Type
-data PDataRepr (defs :: [[k -> Type]]) (s :: k)
+type PDataRepr :: [[PType]] -> PType
+data PDataRepr (defs :: [[PType]]) (s :: S)
 
 pasData :: Term s (PDataRepr _) -> Term s PData
 pasData = punsafeCoerce
@@ -72,7 +72,7 @@ pindexDataList n =
     ind :: Term s PInteger
     ind = fromInteger $ toInteger $ natVal n
 
-data DataReprHandlers (out :: k -> Type) (def :: [[k -> Type]]) (s :: k) where
+data DataReprHandlers (out :: PType) (def :: [[PType]]) (s :: S) where
   DRHNil :: DataReprHandlers out '[] s
   DRHCons :: (Term s (PDataList def) -> Term s out) -> DataReprHandlers out defs s -> DataReprHandlers out (def : defs) s
 
@@ -122,10 +122,10 @@ pmatchDataRepr d handlers =
               handler
               $ go common (idx + 1) rest constr
 
-newtype PIsDataReprInstances (a :: k -> Type) (h :: Type) (s :: k) = PIsDataReprInstances (a s)
+newtype PIsDataReprInstances (a :: PType) (h :: Type) (s :: S) = PIsDataReprInstances (a s)
 
-class (PMatch a, PIsData a) => PIsDataRepr (a :: k -> Type) where
-  type PIsDataReprRepr a :: [[k -> Type]]
+class (PMatch a, PIsData a) => PIsDataRepr (a :: PType) where
+  type PIsDataReprRepr a :: [[PType]]
   pmatchRepr :: forall s b. Term s (PDataRepr (PIsDataReprRepr a)) -> (a s -> Term s b) -> Term s b
 
 instance PIsDataRepr a => PIsData (PIsDataReprInstances a h) where
diff --git a/Plutarch/Either.hs b/Plutarch/Either.hs
index 09b00ab1a..ae3b742ec 100644
--- a/Plutarch/Either.hs
+++ b/Plutarch/Either.hs
@@ -3,7 +3,7 @@ module Plutarch.Either (PEither (..)) where
 import Plutarch (PlutusType (PInner, pcon', pmatch'))
 import Plutarch.Prelude
 
-data PEither (a :: k -> Type) (b :: k -> Type) (s :: k) = PLeft (Term s a) | PRight (Term s b)
+data PEither (a :: PType) (b :: PType) (s :: S) = PLeft (Term s a) | PRight (Term s b)
 
 instance PlutusType (PEither a b) where
   type PInner (PEither a b) c = (a :--> c) :--> (b :--> c) :--> c
diff --git a/Plutarch/Internal.hs b/Plutarch/Internal.hs
index d6cb3587f..268ab79f6 100644
--- a/Plutarch/Internal.hs
+++ b/Plutarch/Internal.hs
@@ -24,6 +24,8 @@ module Plutarch.Internal (
   RawTerm (..),
   TermCont (..),
   TermResult (TermResult, getDeps, getTerm),
+  S,
+  PType,
 ) where
 
 import Crypto.Hash (Context, Digest, hashFinalize, hashInit, hashUpdate)
@@ -100,6 +102,13 @@ mapTerm f (TermResult t d) = TermResult (f t) d
 
 mkTermRes :: RawTerm -> TermResult
 mkTermRes r = TermResult r []
+
+-- | Type of `s`.
+data S
+
+-- | Shorthand for Plutarch types.
+type PType = S -> Type
+
 {- $term
  Source: Unembedding Domain-Specific Languages by Robert Atkey, Sam Lindley, Jeremy Yallop
  Thanks!
@@ -114,17 +123,17 @@ mkTermRes r = TermResult r []
  de-Bruijn index needed to reach its own level given the level it itself is
  instantiated with.
 -}
-newtype Term (s :: k) (a :: k -> Type) = Term {asRawTerm :: Natural -> TermResult}
+newtype Term (s :: S) (a :: PType) = Term {asRawTerm :: Natural -> TermResult}
 
 {- |
   *Closed* terms with no free variables.
 -}
-type ClosedTerm (a :: k -> Type) = forall (s :: k). Term s a
+type ClosedTerm (a :: PType) = forall (s :: S). Term s a
 
-data (:-->) (a :: k -> Type) (b :: k -> Type) (s :: k)
+data (:-->) (a :: PType) (b :: PType) (s :: S)
 infixr 0 :-->
 
-data PDelayed (a :: k -> Type) (s :: k)
+data PDelayed (a :: PType) (s :: S)
 
 {- |
   Lambda abstraction.
diff --git a/Plutarch/Lift.hs b/Plutarch/Lift.hs
index a668f2229..ed97130e8 100644
--- a/Plutarch/Lift.hs
+++ b/Plutarch/Lift.hs
@@ -9,7 +9,7 @@ import Data.Coerce
 import Data.Kind (Type)
 import GHC.Stack (HasCallStack)
 import Plutarch.Evaluate (evaluateScript)
-import Plutarch.Internal (ClosedTerm, Term, compile, punsafeConstantInternal)
+import Plutarch.Internal (ClosedTerm, PType, S, Term, compile, punsafeConstantInternal)
 import qualified Plutus.V1.Ledger.Scripts as Scripts
 import qualified PlutusCore as PLC
 import PlutusCore.Constant (readKnownConstant)
@@ -17,16 +17,16 @@ import PlutusCore.Evaluation.Machine.Exception (MachineError)
 import qualified UntypedPlutusCore as UPLC
 
 -- FIXME: `h -> p`
-class (PLifted p ~ h, PLC.DefaultUni `PLC.Includes` PLiftedRepr p) => PUnsafeLiftDecl (h :: Type) (p :: k -> Type) | p -> h where
+class (PLifted p ~ h, PLC.DefaultUni `PLC.Includes` PLiftedRepr p) => PUnsafeLiftDecl (h :: Type) (p :: PType) | p -> h where
   type PLiftedRepr p :: Type
   type PLifted p :: Type
   pliftToRepr :: h -> PLiftedRepr p
   pliftFromRepr :: PLiftedRepr p -> Maybe h
 
-class PUnsafeLiftDecl (PLifted p) p => PLift (p :: k -> Type)
-instance PUnsafeLiftDecl (PLifted p) p => PLift (p :: k -> Type)
+class PUnsafeLiftDecl (PLifted p) p => PLift (p :: PType)
+instance PUnsafeLiftDecl (PLifted p) p => PLift (p :: PType)
 
-newtype DerivePLiftViaCoercible (h :: Type) (p :: k -> Type) (r :: Type) (s :: k) = DerivePLiftViaCoercible (p s)
+newtype DerivePLiftViaCoercible (h :: Type) (p :: PType) (r :: Type) (s :: S) = DerivePLiftViaCoercible (p s)
 
 instance (Coercible h r, PLC.DefaultUni `PLC.Includes` r) => PUnsafeLiftDecl h (DerivePLiftViaCoercible h p r) where
   type PLiftedRepr (DerivePLiftViaCoercible h p r) = r
@@ -35,7 +35,7 @@ instance (Coercible h r, PLC.DefaultUni `PLC.Includes` r) => PUnsafeLiftDecl h (
   pliftFromRepr = Just . coerce
 
 pconstant :: forall p h s. PUnsafeLiftDecl h p => h -> Term s p
-pconstant x = punsafeConstantInternal $ PLC.someValue @(PLiftedRepr p) @PLC.DefaultUni $ pliftToRepr @_ @h @p x
+pconstant x = punsafeConstantInternal $ PLC.someValue @(PLiftedRepr p) @PLC.DefaultUni $ pliftToRepr @h @p x
 
 -- | Error during script evaluation.
 data LiftError = LiftError deriving stock (Eq, Show)
@@ -44,7 +44,7 @@ plift' :: forall p h. PUnsafeLiftDecl h p => ClosedTerm p -> Either LiftError h
 plift' prog = case evaluateScript (compile prog) of
   Right (_, _, Scripts.unScript -> UPLC.Program _ _ term) ->
     case readKnownConstant @_ @(PLiftedRepr p) @(MachineError PLC.DefaultFun) Nothing term of
-      Right r -> case pliftFromRepr @_ @h @p r of
+      Right r -> case pliftFromRepr @h @p r of
         Just h -> Right h
         Nothing -> Left LiftError
       Left _ -> Left LiftError
diff --git a/Plutarch/List.hs b/Plutarch/List.hs
index 9b9c26650..abab02b8f 100644
--- a/Plutarch/List.hs
+++ b/Plutarch/List.hs
@@ -2,6 +2,7 @@
 module Plutarch.List (
   PList (..),
   PListLike (..),
+  PIsListLike,
   pconvertLists,
 
   -- * Comparison
@@ -29,18 +30,25 @@ module Plutarch.List (
   precList,
   pfoldr,
   pfoldr',
+  pfoldrLazy,
+  pfoldl,
+  pfoldl',
+
+  -- * Special Folds
   pall,
+  pany,
 ) where
 
-import Plutarch
-import Plutarch.Bool (PBool (..), PEq (..), pif, (#&&))
+import Plutarch (PInner, PlutusType, pcon', pmatch')
+import Plutarch.Bool (PBool (PFalse, PTrue), PEq, pif, (#&&), (#==), (#||))
 import Plutarch.Integer (PInteger)
-import Plutarch.Pair (PPair (..))
+import Plutarch.Lift (pconstant)
+import Plutarch.Pair (PPair (PPair))
 import Plutarch.Prelude
 
 import Data.Kind
 
-data PList (a :: k -> Type) (s :: k)
+data PList (a :: PType) (s :: S)
   = PSCons (Term s a) (Term s (PList a))
   | PSNil
 
@@ -58,9 +66,12 @@ instance PEq a => PEq (PList a) where
 
 --------------------------------------------------------------------------------
 
+-- | 'PIsListLike list a' constraints 'list' be a 'PListLike' with valid element type, 'a'.
+type PIsListLike list a = (PListLike list, PElemConstraint list a)
+
 -- | Plutarch types that behave like lists.
-class PListLike (list :: (k -> Type) -> k -> Type) where
-  type PElemConstraint list (a :: k -> Type) :: Constraint
+class PListLike (list :: (PType) -> PType) where
+  type PElemConstraint list (a :: PType) :: Constraint
 
   -- | Canonical eliminator for list-likes.
   pelimList ::
@@ -77,15 +88,15 @@ class PListLike (list :: (k -> Type) -> k -> Type) where
   pnil :: PElemConstraint list a => Term s (list a)
 
   -- | Return the first element of a list. Partial, throws an error upon encountering an empty list.
-  phead :: PIsListLike list a => Term s (list a :--> a)
+  phead :: PElemConstraint list a => Term s (list a :--> a)
   phead = phoistAcyclic $ plam $ pelimList const perror
 
   -- | Take the tail of a list, meaning drop its head. Partial, throws an error upon encountering an empty list.
-  ptail :: PIsListLike list a => Term s (list a :--> list a)
+  ptail :: PElemConstraint list a => Term s (list a :--> list a)
   ptail = phoistAcyclic $ plam $ pelimList (\_ xs -> xs) perror
 
   -- | / O(1) /. Check if a list is empty
-  pnull :: PIsListLike list a => Term s (list a :--> PBool)
+  pnull :: PElemConstraint list a => Term s (list a :--> PBool)
   pnull = phoistAcyclic $ plam $ pelimList (\_ _ -> pconstant False) $ pconstant True
 
 instance PListLike PList where
@@ -93,15 +104,13 @@ instance PListLike PList where
   pelimList match_cons match_nil ls = pmatch ls $ \case
     PSCons x xs -> match_cons x xs
     PSNil -> match_nil
-  pcons = plam $ \x xs -> pcon (PSCons x xs)
+  pcons = phoistAcyclic $ plam $ \x xs -> pcon (PSCons x xs)
   pnil = pcon PSNil
 
-type PIsListLike list a = (PListLike list, PElemConstraint list a)
-
 -- | / O(n) /. Convert from any ListLike to any ListLike, provided both lists' element constraints are met.
 pconvertLists ::
   forall f g a s.
-  (PElemConstraint f a, PElemConstraint g a, PListLike f, PListLike g) =>
+  (PIsListLike f a, PIsListLike g a) =>
   Term s (f a :--> g a)
 pconvertLists = phoistAcyclic $
   pfix #$ plam $ \self ->
@@ -111,7 +120,7 @@ pconvertLists = phoistAcyclic $
 
 -- | Like 'pelimList', but with a fixpoint recursion hatch.
 precList ::
-  (PElemConstraint list a, PListLike list) =>
+  PIsListLike list a =>
   (Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r) ->
   (Term s (list a :--> r) -> Term s r) ->
   Term s (list a :--> r)
@@ -126,7 +135,7 @@ precList mcons mnil =
 
 -- | / O(1) /. Create a singleton list from an element
 psingleton :: PIsListLike list a => Term s (a :--> list a)
-psingleton = plam $ \x -> pcons # x # pnil
+psingleton = phoistAcyclic $ plam $ \x -> pcons # x # pnil
 
 --------------------------------------------------------------------------------
 -- Querying
@@ -143,14 +152,10 @@ pelem =
 -- | / O(n) /. Count the number of elements in the list
 plength :: PIsListLike list a => Term s (list a :--> PInteger)
 plength = phoistAcyclic $
-  plet
-    ( pfix #$ plam $ \self ls n ->
-        pelimList
-          (\_ xs -> self # xs # n + 1)
-          n
-          ls
-    )
-    $ \go -> plam $ \xs -> go # xs # 0
+  plam $ \xs ->
+    let go :: PIsListLike list a => Term s (list a :--> PInteger :--> PInteger)
+        go = (pfix #$ plam $ \self ls n -> pelimList (\_ xs -> self # xs # n + 1) n ls)
+     in go # xs # 0
 
 {- |
   Unsafely index a BuiltinList,
@@ -167,7 +172,26 @@ punsafeIndex = phoistAcyclic $
 
 --------------------------------------------------------------------------------
 
--- | / O(n) /. Fold on a list right-associatively
+-- | / O(n) /. Fold on a list left-associatively.
+pfoldl :: PIsListLike list a => Term s ((b :--> a :--> b) :--> b :--> list a :--> b)
+pfoldl = phoistAcyclic $
+  plam $ \f ->
+    pfix #$ plam $ \self z l ->
+      pelimList
+        (\x xs -> self # (f # z # x) # xs)
+        z
+        l
+
+-- | The same as 'pfoldl', but with Haskell-level reduction function.
+pfoldl' :: PIsListLike list a => (forall s. Term s b -> Term s a -> Term s b) -> Term s (b :--> list a :--> b)
+pfoldl' f = phoistAcyclic $
+  pfix #$ plam $ \self z l ->
+    pelimList
+      (\x xs -> self # f z x # xs)
+      z
+      l
+
+-- | / O(n) /. Fold on a list right-associatively.
 pfoldr :: PIsListLike list a => Term s ((a :--> b :--> b) :--> b :--> list a :--> b)
 pfoldr = phoistAcyclic $
   plam $ \f z ->
@@ -183,11 +207,28 @@ pfoldr' f = phoistAcyclic $
       (\self x xs -> f x (self # xs))
       (const z)
 
--- | / O(n) /. Check that predicate holds for all elements in a list
+{- | / O(n) /. Fold on a list right-associatively, with opportunity for short circuting.
+
+May short circuit when given reducer function is lazy in its second argument.
+-}
+pfoldrLazy :: PIsListLike list a => Term s ((a :--> PDelayed b :--> b) :--> b :--> list a :--> b)
+pfoldrLazy = phoistAcyclic $
+  plam $ \f z ->
+    precList
+      (\self x xs -> f # x # pdelay (self # xs))
+      (const z)
+
+-- | / O(n) /. Check that predicate holds for all elements in a list.
 pall :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> PBool)
 pall = phoistAcyclic $
   plam $ \predicate ->
-    pfoldr # plam (\x acc -> predicate # x #&& acc) # pcon PTrue
+    precList (\self x xs -> predicate # x #&& self # xs) (const $ pconstant True)
+
+-- | / O(n) /. Check that predicate holds for any element in a list.
+pany :: PIsListLike list a => Term s ((a :--> PBool) :--> list a :--> PBool)
+pany = phoistAcyclic $
+  plam $ \predicate ->
+    precList (\self x xs -> predicate # x #|| self # xs) (const $ pconstant False)
 
 -- | / O(n) /. Map a function over a list of elements
 pmap :: (PListLike list, PElemConstraint list a, PElemConstraint list b) => Term s ((a :--> b) :--> list a :--> list b)
@@ -290,12 +331,14 @@ pzip ::
   Term s (list a :--> list b :--> list (PPair a b))
 pzip = phoistAcyclic $ pzipWith' $ \x y -> pcon (PPair x y)
 
--- Horribly inefficient.
-plistEquals :: (PIsListLike list a, PElemConstraint list PBool, PEq a) => Term s (list a :--> list a :--> PBool)
+-- | / O(min(n, m)) /. Check if two lists are equal.
+plistEquals :: (PIsListLike list a, PEq a) => Term s (list a :--> list a :--> PBool)
 plistEquals =
   phoistAcyclic $
-    plam $ \xs ys ->
-      plength # xs #== plength # ys
-        #&& pfoldr' (#&&) # pcon PTrue # (pzipWith' (#==) # xs # ys)
-
---------------------------------------------------------------------------------
+    pfix #$ plam $ \self xlist ylist ->
+      pelimList
+        ( \x xs ->
+            pelimList (\y ys -> pif (x #== y) (self # xs # ys) (pconstant False)) (pconstant False) ylist
+        )
+        (pelimList (\_ _ -> pconstant False) (pconstant True) ylist)
+        xlist
diff --git a/Plutarch/Maybe.hs b/Plutarch/Maybe.hs
index a047e5279..3bafece8e 100644
--- a/Plutarch/Maybe.hs
+++ b/Plutarch/Maybe.hs
@@ -7,7 +7,7 @@ import Plutarch (PlutusType (PInner, pcon', pmatch'))
 import Plutarch.Prelude
 
 -- | Plutus Maybe type, with Scott-encoded repr
-data PMaybe (a :: k -> Type) (s :: k) = PJust (Term s a) | PNothing
+data PMaybe (a :: PType) (s :: S) = PJust (Term s a) | PNothing
 
 instance PlutusType (PMaybe a) where
   type PInner (PMaybe a) b = (a :--> b) :--> PDelayed b :--> b
diff --git a/Plutarch/Pair.hs b/Plutarch/Pair.hs
index 269f4ad99..87af724b4 100644
--- a/Plutarch/Pair.hs
+++ b/Plutarch/Pair.hs
@@ -11,7 +11,7 @@ import Plutarch.Prelude
 
   Note: This is represented differently than 'BuiltinPair'
 -}
-data PPair (a :: k -> Type) (b :: k -> Type) (s :: k) = PPair (Term s a) (Term s b)
+data PPair (a :: PType) (b :: PType) (s :: S) = PPair (Term s a) (Term s b)
 
 instance PlutusType (PPair a b) where
   type PInner (PPair a b) c = (a :--> b :--> c) :--> c
diff --git a/Plutarch/Prelude.hs b/Plutarch/Prelude.hs
index 891d97188..0fb48614f 100644
--- a/Plutarch/Prelude.hs
+++ b/Plutarch/Prelude.hs
@@ -17,6 +17,8 @@ module Plutarch.Prelude (
   pto,
   pfix,
   Type,
+  S,
+  PType,
 ) where
 
 import Prelude ()
diff --git a/Plutarch/Rational.hs b/Plutarch/Rational.hs
index 976a0b9e8..c65947f34 100644
--- a/Plutarch/Rational.hs
+++ b/Plutarch/Rational.hs
@@ -1,28 +1,251 @@
-{-# OPTIONS_GHC -Wno-orphans #-}
-
-module Plutarch.Rational (PRational) where
-
--- TODO: Make easier way of making newtypes?
-data PRational
-
-{-
-prational :: Term (PPair PInteger PInteger) -> Term PRational
-prational = punsafeCoerce
-
-punRational :: Term PRational -> Term (PPair PInteger PInteger)
-punRational = punsafeCoerce
-
-instance Num (Term PTRational) where
-  (+) = undefined
-  (-) = undefined
-  negate = undefined
-  abs = undefined
-  signum = undefined
-  fromInteger n = prational (fromInteger n) 1
-  x * y =
-    pinl (pfst (punRational x)) $ \x1 ->
-    pinl (psnd (punRational x)) $ \x2 ->
-    pinl (pfst (punRational y)) $ \y1 ->
-    pinl (psnd (punRational y)) $ \y2 ->
-    prational (x1 * y1) (x2 * y2)
-    -}
+module Plutarch.Rational (
+  PRational,
+  preduce,
+  pnumerator,
+  pdenominator,
+  pfromInteger,
+  pround,
+  ptruncate,
+  pproperFraction,
+) where
+
+import Plutarch.Prelude
+
+import Data.Ratio (denominator, numerator)
+import Plutarch (PlutusType (..), punsafeCoerce)
+import Plutarch.Bool (PEq (..), POrd (..), pif)
+import Plutarch.Builtin (
+  PAsData,
+  PBuiltinList,
+  PData,
+  PIsData (..),
+  pasInt,
+  pasList,
+  pforgetData,
+ )
+import Plutarch.Integer (PInteger, PIntegral (pdiv, pmod))
+import Plutarch.List (PListLike (pcons, phead, pnil, ptail), pmap)
+import Plutarch.Pair (PPair (..))
+
+data PRational s = PRational (Term s PInteger) (Term s PInteger)
+
+instance PIsData PRational where
+  pfromData x' = phoistAcyclic (plam $ \x -> pListToRat #$ pmap # pasInt #$ pasList # pforgetData x) # x'
+  pdata x' =
+    phoistAcyclic
+      ( plam $ \x ->
+          (punsafeCoerce :: Term _ (PAsData (PBuiltinList (PAsData PInteger))) -> Term _ (PAsData PRational)) $
+            pdata $ pRatToList # x
+      )
+      # x'
+
+pRatToList :: Term s (PRational :--> PBuiltinList (PAsData PInteger))
+pRatToList = plam $ \x -> pmatch x $ \(PRational a b) ->
+  pcons # pdata a #$ pcons # pdata b #$ punsafeCoerce (pnil :: Term s (PBuiltinList PData))
+
+pListToRat :: Term s (PBuiltinList PInteger :--> PRational)
+pListToRat = plam $ \x -> pcon $ PRational (phead # x) (phead #$ ptail # x)
+
+instance PlutusType PRational where
+  type PInner PRational c = (PInteger :--> PInteger :--> c) :--> c
+  pcon' (PRational x y) = plam $ \f -> f # x # y
+  pmatch' p f = p #$ plam $ \x y -> f (PRational x y)
+
+instance PEq PRational where
+  l' #== r' =
+    phoistAcyclic
+      ( plam $ \l r ->
+          pmatch l $ \(PRational ln ld) ->
+            pmatch r $ \(PRational rn rd) ->
+              rd * ln #== rn * ld
+      )
+      # l'
+      # r'
+
+instance POrd PRational where
+  l' #<= r' =
+    phoistAcyclic
+      ( plam $ \l r ->
+          pmatch l $ \(PRational ln ld) ->
+            pmatch r $ \(PRational rn rd) ->
+              rd * ln #<= rn * ld
+      )
+      # l'
+      # r'
+
+  l' #< r' =
+    phoistAcyclic
+      ( plam $ \l r ->
+          pmatch l $ \(PRational ln ld) ->
+            pmatch r $ \(PRational rn rd) ->
+              rd * ln #< rn * ld
+      )
+      # l'
+      # r'
+
+instance Num (Term s PRational) where
+  x' + y' =
+    phoistAcyclic
+      ( plam $ \x y ->
+          preduce #$ pmatch x $
+            \(PRational xn xd) ->
+              pmatch y $ \(PRational yn yd) ->
+                pcon $ PRational (xn * yd + yn * xd) (xd * yd)
+      )
+      # x'
+      # y'
+
+  x' - y' =
+    phoistAcyclic
+      ( plam $ \x y ->
+          preduce
+            #$ pmatch x
+            $ \(PRational xn xd) ->
+              pmatch y $ \(PRational yn yd) ->
+                pcon $ PRational (xn * yd - yn * xd) (xd * yd)
+      )
+      # x'
+      # y'
+
+  x' * y' =
+    phoistAcyclic
+      ( plam $ \x y ->
+          preduce
+            #$ pmatch x
+            $ \(PRational xn xd) ->
+              pmatch y $ \(PRational yn yd) ->
+                pcon $ PRational (xn * yn) (xd * yd)
+      )
+      # x'
+      # y'
+
+  negate x' =
+    phoistAcyclic
+      ( plam $ \x ->
+          pmatch x $ \(PRational xn xd) ->
+            pcon $ PRational (negate xn) xd
+      )
+      # x'
+
+  abs x' =
+    phoistAcyclic
+      ( plam $ \x ->
+          pmatch x $ \(PRational xn xd) ->
+            pcon $ PRational (abs xn) (abs xd)
+      )
+      # x'
+
+  signum x'' =
+    phoistAcyclic
+      ( plam $ \x' -> plet x' $ \x ->
+          pif
+            (x #== 0)
+            0
+            $ pif
+              (x #< 0)
+              (-1)
+              1
+      )
+      # x''
+
+  fromInteger n = pcon $ PRational (fromInteger n) 1
+
+instance Fractional (Term s PRational) where
+  recip x' =
+    phoistAcyclic
+      ( plam $ \x ->
+          pmatch x $ \(PRational xn xd) ->
+            pcon (PRational xd xn)
+      )
+      # x'
+
+  x' / y' =
+    phoistAcyclic
+      ( plam $ \x y ->
+          preduce
+            #$ pmatch x
+            $ \(PRational xn xd) ->
+              pmatch y $ \(PRational yn yd) ->
+                pcon (PRational (xn * yd) (xd * yn))
+      )
+      # x'
+      # y'
+
+  fromRational r =
+    pcon $ PRational (fromInteger $ numerator r) (fromInteger $ denominator r)
+
+preduce :: Term s (PRational :--> PRational)
+preduce = phoistAcyclic $
+  plam $ \x ->
+    pmatch x $ \(PRational xn xd) ->
+      plet (pgcd # xn # xd) $ \r ->
+        plet (signum xd) $ \s ->
+          pcon $ PRational (s * pdiv # xn # r) (s * pdiv # xd # r)
+
+pgcd :: Term s (PInteger :--> PInteger :--> PInteger)
+pgcd = phoistAcyclic $
+  plam $ \x' y' ->
+    plet (abs x') $ \x ->
+      plet (abs y') $ \y ->
+        plet (pmax # x # y) $ \a ->
+          plet (pmin # x # y) $ \b ->
+            pgcd' # a # b
+
+-- assumes inputs are non negative and a >= b
+pgcd' :: Term s (PInteger :--> PInteger :--> PInteger)
+pgcd' = phoistAcyclic $ pfix #$ plam $ f
+  where
+    f self a b =
+      pif
+        (b #== 0)
+        a
+        $ self # b #$ pmod # a # b
+
+pmin :: POrd a => Term s (a :--> a :--> a)
+pmin = phoistAcyclic $ plam $ \a b -> pif (a #<= b) a b
+
+pmax :: POrd a => Term s (a :--> a :--> a)
+pmax = phoistAcyclic $ plam $ \a b -> pif (a #<= b) b a
+
+pnumerator :: Term s (PRational :--> PInteger)
+pnumerator = phoistAcyclic $ plam $ \x -> pmatch x $ \(PRational n _) -> n
+
+pdenominator :: Term s (PRational :--> PInteger)
+pdenominator = phoistAcyclic $ plam $ \x -> pmatch x $ \(PRational _ d) -> d
+
+pfromInteger :: Term s (PInteger :--> PRational)
+pfromInteger = phoistAcyclic $ plam $ \n -> pcon $ PRational n 1
+
+pround :: Term s (PRational :--> PInteger)
+pround = phoistAcyclic $
+  plam $ \x ->
+    pmatch x $ \(PRational a b) ->
+      plet (pdiv # a # b) $ \base ->
+        plet (pmod # a # b) $ \rem ->
+          base
+            + pif
+              (pmod # b # 2 #== 1)
+              (pif (pdiv # b # 2 #< rem) 1 0)
+              ( pif
+                  (pdiv # b # 2 #== rem)
+                  (pmod # base # 2)
+                  (pif (rem #< pdiv # b # 2) 0 1)
+              )
+
+--(pdiv # b # 2 + pmod # b # 2 #<= pmod # a # b) 1 0
+
+ptruncate :: Term s (PRational :--> PInteger)
+ptruncate = phoistAcyclic $
+  plam $ \x ->
+    pmatch x $ \(PRational a b) ->
+      plet (pdiv # a # b) $ \q ->
+        pif
+          (0 #<= a)
+          q
+          (q + pif (pmod # a # b #== 0) 0 1)
+
+pproperFraction :: Term s (PRational :--> PPair PInteger PRational)
+pproperFraction = phoistAcyclic $
+  plam $ \x ->
+    plet (ptruncate # x) $ \q ->
+      pcon $ PPair q (x - pfromInteger # q)
diff --git a/Plutarch/Rec.hs b/Plutarch/Rec.hs
index ef3b4ec59..02594ad24 100644
--- a/Plutarch/Rec.hs
+++ b/Plutarch/Rec.hs
@@ -12,8 +12,9 @@ import Data.Functor.Compose (Compose)
 import Data.Kind (Type)
 import Data.Monoid (Dual (Dual, getDual), Endo (Endo, appEndo), Sum (Sum, getSum))
 import Numeric.Natural (Natural)
-import Plutarch (PCon, pcon, phoistAcyclic, plam, punsafeCoerce, (#), (:-->))
+import Plutarch (PlutusType (PInner, pcon', pmatch'), phoistAcyclic, plam, punsafeCoerce, (#), (:-->))
 import Plutarch.Internal (
+  PType,
   RawTerm (RApply, RLamAbs, RVar),
   Term (Term, asRawTerm),
   TermResult (TermResult, getDeps, getTerm),
@@ -23,13 +24,21 @@ import qualified Rank2
 
 newtype PRecord r s = PRecord {getRecord :: r (Term s)}
 
-type family ScottEncoded (r :: ((k -> Type) -> Type) -> Type) (a :: k -> Type) :: k -> Type
+type family ScottEncoded (r :: ((PType) -> Type) -> Type) (a :: PType) :: PType
 newtype ScottArgument r s t = ScottArgument {getScott :: Term s (ScottEncoded r t)}
 type ScottEncoding r t = ScottEncoded r t :--> t
 
-instance {-# OVERLAPS #-} Rank2.Foldable r => PCon (PRecord r) where
-  pcon :: forall s. PRecord r s -> Term s (PRecord r)
-  pcon = punsafeCoerce . rcon . getRecord
+instance (Rank2.Distributive r, Rank2.Traversable r) => PlutusType (PRecord r) where
+  type PInner (PRecord r) t = ScottEncoding r t
+  pcon' :: forall s. PRecord r s -> forall t. Term s (ScottEncoding r t)
+  pcon' (PRecord r) = rcon r
+  pmatch' :: forall s t. (forall t. Term s (ScottEncoding r t)) -> (PRecord r s -> Term s t) -> Term s t
+  pmatch' p f = p # arg
+    where
+      arg :: Term s (ScottEncoded r t)
+      arg = Term (\i -> TermResult (RLamAbs (fieldCount (initial @r) - 1) $ rawArg i) [])
+      rawArg :: Natural -> RawTerm
+      rawArg depth = getTerm $ asRawTerm (f $ PRecord variables) $ depth + fieldCount (initial @r)
 
 rcon :: forall r s t. Rank2.Foldable r => r (Term s) -> Term s (ScottEncoding r t)
 rcon r = plam (\f -> punsafeCoerce $ appEndo (getDual $ Rank2.foldMap (Dual . Endo . applyField) r) f)
@@ -49,9 +58,9 @@ letrec r = Term term
         (Dual rawTerms, deps) = Rank2.foldMap (rawResult . ($ n) . asRawTerm) (r selfReferring)
     rawResult TermResult {getTerm, getDeps} = (Dual [getTerm], getDeps)
     selfReferring = Rank2.fmap fromRecord accessors
-    fromRecord (ScottArgument (Term access)) = Term $ \depth -> mapTerm (\field -> RApply (RVar $ fieldCount + depth - 1) [field]) (access 0)
-    fieldCount :: Natural
-    fieldCount = getSum (Rank2.foldMap (const $ Sum 1) (accessors @r))
+    fromRecord :: ScottArgument r s a -> Term s a
+    fromRecord (ScottArgument (Term access)) =
+      Term $ \depth -> mapTerm (\field -> RApply (RVar $ fieldCount (initial @r) + depth - 1) [field]) (access 0)
 
 -- | Converts a Haskell field function to a Scott-encoded record field accessor.
 field ::
@@ -63,31 +72,39 @@ field f = getScott (f accessors)
 
 -- | Provides a record of function terms that access each field out of a Scott-encoded record.
 accessors :: forall r s. (Rank2.Distributive r, Rank2.Traversable r) => r (ScottArgument r s)
-accessors = Rank2.cotraverse accessor id
+accessors = abstract Rank2.<$> variables
   where
-    accessor :: (r (ScottArgument r s) -> ScottArgument r s a) -> ScottArgument r s a
-    accessor ref = ref ordered
-    ordered :: r (ScottArgument r s)
-    ordered = evalState (Rank2.traverse next initial) fieldCount
-    initial :: r (Compose Maybe (ScottArgument r s))
-    initial = Rank2.distribute Nothing
-    next :: f a -> State Natural (ScottArgument r s a)
+    abstract :: Term s a -> ScottArgument r s a
+    abstract (Term t) = ScottArgument (phoistAcyclic $ Term $ mapTerm (RLamAbs $ fieldCount (initial @r) - 1) . t)
+
+{- | A record of terms that each accesses a different variable in scope,
+ outside in following the field order.
+-}
+variables :: forall r s. (Rank2.Distributive r, Rank2.Traversable r) => r (Term s)
+variables = Rank2.cotraverse var id
+  where
+    var :: (r (Term s) -> Term s a) -> Term s a
+    var ref = ref ordered
+    ordered :: r (Term s)
+    ordered = evalState (Rank2.traverse next $ initial @r) (fieldCount $ initial @r)
+    next :: f a -> State Natural (Term s a)
     next _ = do
       i <- get
       let i' = pred i
       seq i' (put i')
-      return
-        ( ScottArgument $
-            phoistAcyclic $
-              Term $
-                const $
-                  TermResult
-                    { getTerm = RLamAbs (fieldCount - 1) $ RVar i'
-                    , getDeps = []
-                    }
-        )
-    fieldCount :: Natural
-    fieldCount = getSum (Rank2.foldMap (const $ Sum 1) initial)
+      return $
+        Term $
+          const $
+            TermResult
+              { getTerm = RVar i'
+              , getDeps = []
+              }
+
+initial :: Rank2.Distributive r => r (Compose Maybe (Term s))
+initial = Rank2.distribute Nothing
+
+fieldCount :: Rank2.Foldable r => r f -> Natural
+fieldCount = getSum . Rank2.foldMap (const $ Sum 1)
 
 -- | The raw Y-combinator term
 rfix :: RawTerm
diff --git a/Plutarch/Rec/TH.hs b/Plutarch/Rec/TH.hs
index ccb169148..b6689f3f9 100644
--- a/Plutarch/Rec/TH.hs
+++ b/Plutarch/Rec/TH.hs
@@ -1,18 +1,23 @@
 {-# LANGUAGE TemplateHaskell #-}
 
-module Plutarch.Rec.TH (deriveScottEncoded) where
+module Plutarch.Rec.TH (deriveAll, deriveScottEncoded) where
 
 import Language.Haskell.TH (Q)
 import qualified Language.Haskell.TH as TH
 import Plutarch ((:-->))
 import Plutarch.Rec (ScottEncoded)
+import qualified Rank2.TH
 
+-- | Use as a TH splice for all necessary @instance@ declarations.
+deriveAll :: TH.Name -> Q [TH.Dec]
+deriveAll name = (<>) <$> deriveScottEncoded name <*> Rank2.TH.deriveAll name
+
+-- | Use as a TH splice for @type instance ScottEncoded@ declarations.
 deriveScottEncoded :: TH.Name -> Q [TH.Dec]
 deriveScottEncoded name = do
   con <- reifyConstructor name
   a <- TH.newName "a"
   let qa = pure (TH.VarT a)
-  --   _ <- [d| type instance ScottEncoded $(pure $ TH.ConT name) $qa = $(genScottEncoded con qa) |] >>= error . show
   [d|type instance ScottEncoded $(pure $ TH.ConT name) $qa = $(genScottEncoded con qa)|]
 
 genScottEncoded :: TH.Con -> Q TH.Type -> Q TH.Type
diff --git a/README.md b/README.md
index c2ce0b30e..e81e972d0 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,13 @@
 # Plutarch
+
+[![Hercules-ci][Herc badge]][Herc link]
+[![Cachix Cache][Cachix badge]][Cachix link]
+
+[Herc badge]: https://img.shields.io/badge/ci--by--hercules-green.svg
+[Herc link]: https://hercules-ci.com/github/Plutonomicon/plutarch
+[Cachix badge]: https://img.shields.io/badge/cachix-public--plutonomicon-blue.svg
+[Cachix link]: https://public-plutonomicon.cachix.org 
+
 Plutarch is a typed eDSL in Haskell for writing efficient Plutus Core validators.
 
 # Why Plutarch?
@@ -31,5 +40,24 @@ package plutarch
 # Usage
 Read the [Plutarch guide](./docs/GUIDE.md) to get started!
 
+# Benchmarks
+
+```
+cabal bench
+```
+
+This will write the benchmark report to `bench.csv` as well as output a table view of the same.
+
+## Benchmarking a commit
+To run benchmarks on a particular commit,
+
+```
+nix run github:Plutonomicon/plutarch/<COMMIT-GOES-HERE>#benchmark
+```
+
+Note that you can also view these benchmarks on a per-commit basis by looking at Hercules CI logs. Go to the Hercules CI job run for a given commit, and navigate to the `nixCi.checks.x86_64-linux.benchmark` page in the Attributes table, and then click on the "Log" header to view its output.
+
+Eventually we will have PR integration for running benchmarks. 
+
 # Contributing
-Contributions are more than welcome! Alongside the [User guide](#usage) above, you may also find the [Developers' guide](./docs/DEVGUIDE.md) useful for understanding the codebase.
\ No newline at end of file
+Contributions are more than welcome! Alongside the [User guide](#usage) above, you may also find the [Developers' guide](./docs/DEVGUIDE.md) useful for understanding the codebase.
diff --git a/bench/Benchmark.hs b/bench/Benchmark.hs
new file mode 100644
index 000000000..b07cbc9bc
--- /dev/null
+++ b/bench/Benchmark.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE RecordWildCards #-}
+
+-- | Benchmark (exbudget and script size) for Plutus scripts
+module Benchmark (
+  -- | * Types
+  Benchmark,
+  NamedBenchmark,
+  ScriptSizeBytes,
+  -- | * Benchmark an arbitraty Plutus script
+  benchmarkScript,
+  -- | * Benchmark entrypoints
+  bench,
+  benchGroup,
+  benchMain,
+) where
+
+import qualified Codec.Serialise as Codec
+import Control.Arrow ((&&&))
+import qualified Data.ByteString.Lazy as BSL
+import qualified Text.PrettyPrint.Boxes as B
+
+import qualified Data.ByteString.Lazy as LB
+import qualified Data.ByteString.Short as SBS
+import Data.Csv (
+  DefaultOrdered,
+  ToField,
+  ToNamedRecord,
+  header,
+  namedRecord,
+  (.=),
+ )
+import qualified Data.Csv as Csv
+import Data.Int (Int64)
+import qualified Data.List as List
+import Data.Maybe (fromJust)
+import GHC.Generics (Generic)
+import GHC.Stack (HasCallStack)
+import Plutarch (ClosedTerm, compile)
+import Plutus.V1.Ledger.Api (
+  ExBudget (ExBudget),
+  ExCPU (ExCPU),
+  ExMemory (ExMemory),
+  Script,
+ )
+import qualified Plutus.V1.Ledger.Api as Plutus
+
+-- | Benchmark the given script
+benchmarkScript :: String -> Script -> NamedBenchmark
+benchmarkScript name = NamedBenchmark . (name,) . benchmarkScript'
+
+benchmarkScript' :: Script -> Benchmark
+benchmarkScript' =
+  uncurry mkBenchmark . (evalScriptCounting &&& (fromInteger . toInteger . SBS.length)) . serialiseScript
+  where
+    mkBenchmark :: ExBudget -> Int64 -> Benchmark
+    mkBenchmark (ExBudget cpu mem) = Benchmark cpu mem . ScriptSizeBytes
+
+    serialiseScript :: Script -> SBS.ShortByteString
+    serialiseScript = SBS.toShort . LB.toStrict . Codec.serialise -- Using `flat` here breaks `evalScriptCounting`
+    evalScriptCounting :: HasCallStack => Plutus.SerializedScript -> Plutus.ExBudget
+    evalScriptCounting script =
+      let costModel = fromJust Plutus.defaultCostModelParams
+          (_logout, e) = Plutus.evaluateScriptCounting Plutus.Verbose costModel script []
+       in case e of
+            Left evalErr -> error ("Eval Error: " <> show evalErr)
+            Right exbudget -> exbudget
+
+data Benchmark = Benchmark
+  { -- | CPU budget used by the script
+    exBudgetCPU :: ExCPU
+  , -- | Memory budget used by the script
+    exBudgetMemory :: ExMemory
+  , -- | Size of Plutus script in bytes
+    scriptSizeBytes :: ScriptSizeBytes
+  }
+  deriving stock (Show, Generic)
+
+newtype ScriptSizeBytes = ScriptSizeBytes Int64
+  deriving stock (Eq, Ord, Show, Generic)
+  deriving newtype (Num, ToField)
+
+{- | A `Benchmark` with a name.
+
+ Handy for writing CSV files with headers.
+-}
+newtype NamedBenchmark = NamedBenchmark (String, Benchmark)
+  deriving stock (Show, Generic)
+
+instance ToNamedRecord NamedBenchmark where
+  toNamedRecord (NamedBenchmark (name, Benchmark {..})) =
+    namedRecord ["name" .= name, "cpu" .= exBudgetCPU, "mem" .= exBudgetMemory, "size" .= scriptSizeBytes]
+
+instance DefaultOrdered NamedBenchmark where
+  headerOrder _ = header ["name", "cpu", "mem", "size"]
+
+benchGroup :: String -> [[NamedBenchmark]] -> [NamedBenchmark]
+benchGroup groupName bs =
+  [NamedBenchmark (groupName ++ ":" ++ name, benchmark) | NamedBenchmark (name, benchmark) <- concat bs]
+
+bench :: String -> ClosedTerm a -> [NamedBenchmark]
+bench name prog =
+  [benchmarkScript name $ compile prog]
+
+benchMain :: [NamedBenchmark] -> IO ()
+benchMain benchmarks = do
+  let csv = Csv.encodeDefaultOrderedByName benchmarks
+  BSL.writeFile "bench.csv" csv
+  putStrLn "Wrote to bench.csv:"
+  putStrLn $ B.render . renderBudgetTable $ benchmarks
+  where
+    -- Renders a neat tabular representation of the benchmarks
+    renderBudgetTable :: [NamedBenchmark] -> B.Box
+    renderBudgetTable bs =
+      let rows =
+            [ [ B.text name
+              , B.text $ show cpu <> "(cpu)"
+              , B.text $ show mem <> "(mem)"
+              , B.text $ show sz <> "(bytes)"
+              ]
+            | NamedBenchmark (name, Benchmark (ExCPU cpu) (ExMemory mem) (ScriptSizeBytes sz)) <- bs
+            ]
+          alignments =
+            -- Align all but the first column to the right, because they represent numeric values.
+            B.left : repeat B.right
+       in B.hsep 2 B.left . fmap (uncurry B.vcat) $ zip alignments (List.transpose rows)
diff --git a/bench/Main.hs b/bench/Main.hs
new file mode 100644
index 000000000..91406ff05
--- /dev/null
+++ b/bench/Main.hs
@@ -0,0 +1,117 @@
+module Main (main) where
+
+import Benchmark
+import Plutarch
+import Plutarch.Bool
+import Plutarch.Builtin
+import Plutarch.Integer
+import Plutarch.Lift
+import qualified Plutarch.List as List
+
+main :: IO ()
+main = do
+  benchMain benchmarks
+
+benchmarks :: [NamedBenchmark]
+benchmarks =
+  benchGroup
+    "types"
+    [ benchGroup "int" integerBench
+    , benchGroup "bool" boolBench
+    , benchGroup "builtin:intlist" intListBench
+    ]
+
+integerBench :: [[NamedBenchmark]]
+integerBench =
+  [ -- Calling add twice
+    benchGroup
+      "add(2)"
+      $ let addInlined :: Term s PInteger -> Term s PInteger -> Term s PInteger
+            addInlined x y = x + y + 1
+            addUnhoisted :: Term s (PInteger :--> PInteger :--> PInteger)
+            addUnhoisted = plam $ \x y -> x + y + 1
+            addHoisted :: Term s (PInteger :--> PInteger :--> PInteger)
+            addHoisted = phoistAcyclic $ plam $ \x y -> x + y + 1
+         in [ bench "inlined" $ addInlined 12 32 + addInlined 5 4
+            , bench "unhoist" $ addUnhoisted # 12 # 32 + addUnhoisted # 5 # 4
+            , bench "hoisted" $ addHoisted # 12 # 32 + addHoisted # 5 # 4
+            ]
+  ]
+
+boolBench :: [[NamedBenchmark]]
+boolBench =
+  let true = pconstant @PBool True
+      false = pconstant @PBool False
+      pandNoHoist = phoistAcyclic $ plam $ \x y -> pif' # x # y # (pdelay $ pcon PFalse)
+   in [ benchGroup
+          "and"
+          [ bench "strict" $ pand' # true # false
+          , bench "lazy" $ (#&&) true false
+          , -- Calling `pand` twice.
+            bench "pand(2)" $
+              let x = pand # true # pdelay false
+               in pand # true # x
+          , bench "pand(2):unhoisted" $
+              let x = pandNoHoist # true # pdelay false
+               in pandNoHoist # true # x
+          ]
+      ]
+
+intListBench :: [[NamedBenchmark]]
+intListBench =
+  let numList = pconstant @(PBuiltinList PInteger) [1 .. 5]
+   in [ bench "phead" $ List.phead # numList
+      , bench "ptail" $ List.ptail # numList
+      , -- Accessing the first two elements, and adds them.
+        benchGroup
+          "x1+x2"
+          [ -- Via HeadList and TailList only
+            bench "builtin" $
+              (List.phead #$ List.ptail # numList) + (List.phead # numList)
+          , -- Via ChooseList (twice invoked)
+            bench "pmatch" $
+              pmatch numList $ \case
+                PNil -> perror
+                PCons x xs ->
+                  pmatch xs $ \case
+                    PNil -> perror
+                    PCons y _ ->
+                      x + y
+          ]
+      , -- Various ways to uncons a list
+        benchGroup
+          "uncons"
+          [ -- ChooseList builtin, like uncons but fails on null lists
+            bench "ChooseList" $
+              pmatch numList $ \case
+                PNil -> perror
+                PCons _x xs ->
+                  xs
+          , -- Retrieving head and tail of a list
+            bench "head-and-tail" $
+              plet (List.phead # numList) $ \_x ->
+                List.ptail # numList
+          , -- Retrieve head and tail using builtins, but fail on null lists.
+            bench "head-and-tail-and-null" $
+              plet (List.pnull # numList) $ \isEmpty ->
+                pmatch isEmpty $ \case
+                  PTrue -> perror
+                  PFalse -> plet (List.phead # numList) $ \_x ->
+                    List.ptail # numList
+          ]
+      , bench
+          "plength"
+          $ List.plength # pconstant @(PBuiltinList PInteger) [1, 2, 3, 4, 5, 6, 7, 8, 9, 0]
+      , bench
+          "pelem"
+          $ List.pelem # 1 # pconstant @(PBuiltinList PInteger) [5, 2, 3, 4, 7, 5, 1, 6, 2]
+      , bench
+          "pall"
+          $ List.pall @PBuiltinList @PInteger # plam (const $ pconstant @PBool False) # pconstant [1, 2, 3, 4, 5, 6]
+      , benchGroup
+          "plistEquals"
+          [ bench "==(n=3)" $ List.plistEquals @PBuiltinList @PInteger # pconstant [1, 2, 3] # pconstant [1, 2, 3]
+          , bench "/=(n=4)" $ List.plistEquals @PBuiltinList @PInteger # pconstant [1, 2, 3, 4] # pconstant [1, 2, 3]
+          , bench "/=(empty;n=3)" $ List.plistEquals @PBuiltinList @PInteger # pconstant [] # pconstant [1, 2, 3]
+          ]
+      ]
diff --git a/cabal.project b/cabal.project
index a29ff412f..51d10030d 100644
--- a/cabal.project
+++ b/cabal.project
@@ -7,3 +7,5 @@ packages: ./.
 
 constraints:
   aeson > 2
+
+benchmarks: true
\ No newline at end of file
diff --git a/docs/DEVGUIDE.md b/docs/DEVGUIDE.md
index 79b6f4fc8..022734b91 100644
--- a/docs/DEVGUIDE.md
+++ b/docs/DEVGUIDE.md
@@ -1,7 +1,32 @@
 Looking to contribute to Plutarch? Looking for functionalities that are not currently provided by Plutarch from a safe interface? You've come to the right place!
 
+<details>
+<summary> Table of Contents </summary>
+
+- [Code Style](#code-style)
+- [Pre-commit checks](#pre-commit-checks)
+- [Concepts](#concepts)
+  - [Plutus Core constants (UNSAFE)](#plutus-core-constants-unsafe)
+  - [Plutus core builtin functions](#plutus-core-builtin-functions)
+  - [Working with BuiltinData/Data/PData](#working-with-builtindatadatapdata)
+- [Lower Level Examples](#lower-level-examples)
+  - [Extracting `txInfoInputs` from `ScriptContext` manually (UNTYPED)](#extracting-txinfoinputs-from-scriptcontext-manually-untyped)
+- [Useful Links](#useful-links)
+</details>
+
 > Note: If you spot any mistakes/have any related questions that this guide lacks the answer to, please don't hesitate to raise an issue. The goal is to have high quality documentation for Plutarch developers!
 
+# Code Style
+You should generally follow the [MLabs style guide](https://github.com/mlabs-haskell/styleguide), credit to [@Koz Ross](https://github.com/kozross).
+
+**Discouraged Extensions**
+* `ImportQualifiedPost`
+* `RecordWildCards`
+
+# Pre-commit checks
+Remember to run `./bin/format` to format your code and `cabal test` to make sure all the tests pass prior to making a PR!
+
+# Concepts
 Even if certain functionalities are absent from the public facing API - you can always implement them using functions like `punsafeConstant` and `punsafeBuiltin` - these allow you to walk the lines between Plutus core and Plutarch.
 
 A general familiarity with Plutus core is important. You can learn all of that through the following documents-
@@ -12,7 +37,7 @@ A general familiarity with Plutus core is important. You can learn all of that t
 
 Parts of the [Pluto guide](https://github.com/Plutonomicon/pluto/blob/main/GUIDE.md) may also prove useful.
 
-# Plutus Core constants (UNSAFE)
+## Plutus Core constants (UNSAFE)
 
 > **NOTE**: The following information is almost never necessary with the existence of `pconstant`. Refer to [constant building](./GUIDE.md#constants) and [`PLift`](./GUIDE.md#plift) section of the Plutarch user guide.
 
@@ -71,7 +96,7 @@ foo = punsafeConstant . PLC.Some . PLC.ValueOf PLC.DefaultUniBool
 
 Of course, we represent Plutus core booleans as `Term s PBool` in Plutarch - so that's its type!
 
-# Plutus core builtin functions
+## Plutus core builtin functions
 
 This is what you will be wrangling with the most. Builtin functions are going to be the foundation of _everything_ you do. And the documentation on them is….. sparse.
 
@@ -112,7 +137,7 @@ pchooseList = pforce $ pforce $ punsafeBuiltin PLC.ChooseList
 
 We have a [Plutus Core builtin functions reference](https://github.com/Plutonomicon/plutonomicon/blob/main/builtin-functions.md) for everything you need to know about them. Including types, usage, and forcing.
 
-# Working with BuiltinData/Data/PData
+## Working with BuiltinData/Data/PData
 
 Most of the time, you'll be working with `BuiltinData`/`Data` - this is the type of the arguments that will be passed onto your script from the outside. This is the type of the datum, the redeemer and the script context. This is also the type of arguments you will be able to pass to a `Script`.
 
@@ -120,7 +145,8 @@ Plutarch aims to hide these low level details from the user. Ideally, you will b
 
 If you want to work with `BuiltinData` directly however, which you may have to do during developing Plutarch, you can find all that you need to know at [Plutonomicon](https://github.com/Plutonomicon/plutonomicon/blob/main/builtin-data.md).
 
-# Extracting `txInfoInputs` from `ScriptContext` manually (UNTYPED)
+# Lower Level Examples
+## Extracting `txInfoInputs` from `ScriptContext` manually (UNTYPED)
 Here's a quick refresher on what `ScriptContext` looks like-
 
 ```haskell
diff --git a/docs/GUIDE.md b/docs/GUIDE.md
index 87ab43073..a3a289272 100644
--- a/docs/GUIDE.md
+++ b/docs/GUIDE.md
@@ -17,6 +17,7 @@
     - [Recursion](#recursion)
   - [Concepts](#concepts)
     - [Hoisting, metaprogramming,  and fundamentals](#hoisting-metaprogramming--and-fundamentals)
+      - [Hoisting Operators](#hoisting-operators)
     - [What is the `s`?](#what-is-the-s)
     - [eDSL Types in Plutarch](#edsl-types-in-plutarch)
     - [`plet` to avoid work duplication](#plet-to-avoid-work-duplication)
@@ -321,6 +322,42 @@ To solve this problem, Plutarch supports _hoisting_. Hoisting only works for _cl
 
 Hoisted terms are essentially moved to a top-level `plet`, i.e. it's essentially common subexpression elimination. Do note that because of this, your hoisted term is **also strictly evaluated, meaning that you shouldn't hoist non-lazy complex computations (use e.g.** `pdelay` **to avoid this).**
 
+#### Hoisting Operators
+For the sake of convenience, you often would want to use operators - which must be Haskell level functions. This is the case for `+`, `-`, `#==` and many more.
+
+Choosing convenience over efficiency is difficult, but if you notice that your operator uses complex logic and may end up creating big terms - you can trivially factor out the logic into a Plutarch level function, hoist it, and simply apply that function within the operator.
+
+Consider boolean or-
+```hs
+(#||) :: Term s PBool -> Term s PBool -> Term s PBool
+x #|| y = pif x (pcon PTrue) $ pif y (pcon PTrue) $ pcon PFalse
+```
+You can factor out most of the logic to a Plutarch level function, and apply that in the operator definition-
+
+```hs
+(#||) :: Term s PBool -> Term s PBool -> Term s PBool
+x #|| y = por # x # pdelay y
+
+por :: Term s (PBool :--> PDelayed PBool :--> PBool)
+por = phoistAcyclic $ plam $ \x y -> pif' # x # pcon PTrue # pforce y
+```
+
+In general the pattern goes like this-
+```hs
+(<//>) :: Term s x -> Term s y -> Term s z
+x <//> y = f # x # y
+
+f :: Term s (x :--> y :--> z)
+f = phoistAcyclic $ plam $ \x y -> <complex computation>
+```
+(OR, simply inlined)
+```hs
+(<//>) :: Term s x -> Term s y -> Term s z
+x <//> y = (\f -> f # x # y) $ phoistAcyclic $ plam $ \x y -> <complex computation>
+```
+
+> Note: You don't even need to export the Plutarch level function or anything! You can simply have that complex logic factored out into a *hoisted, internal Plutarch function* and everything will work just fine!
+
 ### What is the `s`?
 
 The `s` essentially represents the context, and is like the `s` of `ST`.
@@ -1080,28 +1117,7 @@ Of course, what you _really_ should do , is prefer Plutarch level functions when
 
 Plutarch level functions have a lot of advantages - they can be hoisted; they are strict so you can [use their arguments however many times you like without duplicating work](#dont-duplicate-work); they are required for Plutarch level higher order functions etc. Unless you _really_ need laziness, like `pif` does, try to use Plutarch level functions.
 
-What about convenient Haskell operators? Well, these must be Haskell level functions working on Plutarch terms. This is the case for `+`, `-`, `#==` and many more.
-
-Choosing convenience over efficiency is difficult, but if you notice that your operator uses complex logic and may end up creating big terms, like in this case-
-
-```haskell
-(#||) :: Term s PBool -> Term s PBool -> Term s PBool
-x #|| y = pif x (pcon PTrue) $ pif y (pcon PTrue) $ pcon PFalse
-```
-
-You can factor out most of the logic to a Plutarch level function, and apply that in the operator definition-
-
-```haskell
-(#||) :: Term s PBool -> Term s PBool -> Term s PBool
-x #|| y = por # pdelay x # pdelay y
-
-por :: Term s (PDelayed PBool :--> PDelayed PBool :--> PBool)
-por = phoistAcyclic $
-  plam $
-    \x y -> pif' # pforce x # pcon PTrue #$ pif' # pforce y # pcon PTrue # pcon PFalse
-```
-
-The necessity of workarounds like these will be significantly reduced once we figure out [eta reductions (#32)](https://github.com/Plutonomicon/plutarch/issues/32) though!
+Also see: [Hoisting](#hoisting-metaprogramming--and-fundamentals).
 
 ## When to use Haskell level functions?
 Although you should generally [prefer Plutarch level functions](#prefer-plutarch-level-functions), there are times when a Haskell level function is actually much better. However, figuring out *when* that is the case is a delicate art.
diff --git a/examples/Examples/Api.hs b/examples/Examples/Api.hs
index 8d1d04e3e..a010d3637 100644
--- a/examples/Examples/Api.hs
+++ b/examples/Examples/Api.hs
@@ -10,6 +10,7 @@ import Plutarch.Api.V1 (
  )
 import Plutarch.Builtin (PAsData, PBuiltinList)
 import Plutarch.DataRepr (pindexDataList)
+import Plutarch.Lift (pconstant)
 
 import Plutus.V1.Ledger.Api (
   Address (..),
diff --git a/examples/Examples/LetRec.hs b/examples/Examples/LetRec.hs
index 1a979b34e..890e825fc 100644
--- a/examples/Examples/LetRec.hs
+++ b/examples/Examples/LetRec.hs
@@ -2,17 +2,15 @@
 
 module Examples.LetRec (tests) where
 
-import Test.Tasty (TestTree, testGroup)
-
-{-
-import Plutarch (printTerm, punsafeCoerce)
+import Plutarch (pcon', pmatch', printTerm)
 import Plutarch.Bool (PBool (PFalse, PTrue), pif, (#==))
 import Plutarch.Integer (PInteger)
 import Plutarch.Prelude
 import Plutarch.Rec (PRecord (PRecord), ScottEncoded, ScottEncoding, field, letrec)
-import Plutarch.Rec.TH (deriveScottEncoded)
+import Plutarch.Rec.TH (deriveAll)
 import Plutarch.String (PString)
 import qualified Rank2.TH
+import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.HUnit (testCase, (@?=))
 import Utils
 import Prelude hiding (even, odd)
@@ -23,16 +21,27 @@ data SampleRecord f = SampleRecord
   , sampleString :: f PString
   }
 
-sampleRecord :: PRecord SampleRecord s
+data EvenOdd f = EvenOdd
+  { even :: f (PInteger :--> PBool)
+  , odd :: f (PInteger :--> PBool)
+  }
+
+type instance ScottEncoded EvenOdd a = (PInteger :--> PBool) :--> (PInteger :--> PBool) :--> a
+
+$(Rank2.TH.deriveAll ''EvenOdd)
+$(deriveAll ''SampleRecord) -- also autoderives the @type instance ScottEncoded@
+
+sampleRecord :: Term (s :: S) (ScottEncoding SampleRecord (t :: PType))
 sampleRecord =
-  PRecord
-    SampleRecord
-      { sampleBool = pcon PFalse
-      , sampleInt = 6
-      , sampleString = "Salut, Monde!"
-      }
+  pcon' $
+    PRecord
+      SampleRecord
+        { sampleBool = pcon PFalse
+        , sampleInt = 6
+        , sampleString = "Salut, Monde!"
+        }
 
-sampleRecur :: Term (s :: k) (ScottEncoding SampleRecord (t :: k -> Type))
+sampleRecur :: Term (s :: S) (ScottEncoding SampleRecord (t :: PType))
 sampleRecur =
   letrec $
     const
@@ -42,14 +51,7 @@ sampleRecur =
         , sampleString = "Hello, World!"
         }
 
-data EvenOdd f = EvenOdd
-  { even :: f (PInteger :--> PBool)
-  , odd :: f (PInteger :--> PBool)
-  }
-
-type instance ScottEncoded EvenOdd a = (PInteger :--> PBool) :--> (PInteger :--> PBool) :--> a
-
-evenOdd :: Term (s :: k) (ScottEncoding EvenOdd (t :: k -> Type))
+evenOdd :: Term (s :: S) (ScottEncoding EvenOdd (t :: PType))
 evenOdd = letrec evenOddRecursion
   where
     evenOddRecursion :: EvenOdd (Term s) -> EvenOdd (Term s)
@@ -65,9 +67,13 @@ tests =
     "Records"
     [ testGroup
         "Simple"
-        [ testCase "precord" $
-            printTerm (punsafeCoerce (pcon sampleRecord) # field sampleInt)
+        [ testCase "record construction" $
+            printTerm (sampleRecord # field sampleInt)
               @?= "(program 1.0.0 ((\\i0 -> i1 False 6 \"Salut, Monde!\") (\\i0 -> \\i0 -> \\i0 -> i2)))"
+        , testCase "record field" $
+            equal' (sampleRecord # field sampleInt) "(program 1.0.0 6)"
+        , testCase "record match" $
+            equal' (pmatch' sampleRecord $ \(PRecord r) -> sampleString r) "(program 1.0.0 \"Salut, Monde!\")"
         ]
     , testGroup
         "Letrec"
@@ -78,11 +84,3 @@ tests =
         , testCase "even 5" $ equal' (evenOdd # field even # (5 :: Term s PInteger)) "(program 1.0.0 False)"
         ]
     ]
-
-$(Rank2.TH.deriveAll ''EvenOdd)
-$(Rank2.TH.deriveAll ''SampleRecord)
-$(deriveScottEncoded ''SampleRecord)
--}
-
-tests :: TestTree
-tests = testGroup "FIXME letrec" []
diff --git a/examples/Examples/List.hs b/examples/Examples/List.hs
index 1bdfa0b23..3baccd7a8 100644
--- a/examples/Examples/List.hs
+++ b/examples/Examples/List.hs
@@ -9,6 +9,7 @@ import Plutarch
 import Plutarch.Bool (pnot, (#<), (#==))
 import Plutarch.Builtin (PBuiltinList (..))
 import Plutarch.Integer
+import Plutarch.Lift
 import Plutarch.List
 
 --------------------------------------------------------------------------------
@@ -50,4 +51,17 @@ tests = do
         expect $
           (pzipWith' (+) # integerList [1 .. 10] # integerList [1 .. 10])
             #== integerList (fmap (* 2) [1 .. 10])
+    , testCase "pfoldl" $ do
+        expect $
+          (pfoldl # plam (-) # 0 # integerList [1 .. 10])
+            #== pconstant (foldl (-) 0 [1 .. 10])
+        expect $
+          (pfoldl' (-) # 0 # integerList [1 .. 10])
+            #== pconstant (foldl (-) 0 [1 .. 10])
+        expect $
+          (pfoldl # plam (-) # 0 # integerList [])
+            #== pconstant 0
+        expect $
+          (pfoldl' (-) # 0 # integerList [])
+            #== pconstant 0
     ]
diff --git a/examples/Examples/PlutusType.hs b/examples/Examples/PlutusType.hs
index 92c3bc511..ac13e605b 100644
--- a/examples/Examples/PlutusType.hs
+++ b/examples/Examples/PlutusType.hs
@@ -12,7 +12,7 @@ import Utils
 {- |
   A Sum type, which can be encoded as an Enum
 -}
-data AB (s :: k) = A | B
+data AB (s :: S) = A | B
 
 {- |
   AB is encoded as an Enum, using values of PInteger
diff --git a/examples/Examples/Rationals.hs b/examples/Examples/Rationals.hs
new file mode 100644
index 000000000..79b811223
--- /dev/null
+++ b/examples/Examples/Rationals.hs
@@ -0,0 +1,101 @@
+module Examples.Rationals (tests) where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Utils
+
+import Plutarch
+import Plutarch.Bool
+import Plutarch.Builtin
+import Plutarch.Pair
+import Plutarch.Rational
+
+--import Data.Ratio ((%))
+
+tests :: HasTester => TestTree
+tests = do
+  testGroup
+    "rational tests"
+    [ testCase "1/2 + 1/2 = 1" $
+        expect $ 1 / 2 + 1 / 2 #== (1 :: Term s PRational)
+    , testCase "(1 - 3/2) * (2 - 5/2) == 1/4" $
+        expect $ (1 - 3 / 2) * (2 - 5 / 2) #== (1 / 4 :: Term s PRational)
+    , testCase "1/2 - 1/3 = 1/6" $
+        expect $ 1 / 2 - 1 / 3 #== (1 / 6 :: Term s PRational)
+    , testCase "2/9 < 3/10" $
+        expect $ 2 / 9 #< (3 / 10 :: Term s PRational)
+    , testCase "harmonic sum" $
+        expect $ 1 / 2 + 1 / 3 + 1 / 4 + 1 / 5 #== (77 / 60 :: Term s PRational)
+    , testCase "product" $
+        expect $ 1 / 2 * 2 / 3 * 3 / 4 * 4 / 5 * 5 / 6 #== (1 / 6 :: Term s PRational)
+    , testCase "round 5/3" $
+        expect $ pround # (5 / 3) #== 2
+    , testCase "round 4/3" $
+        expect $ pround # (4 / 3) #== 1
+    , testCase "round 5/2" $
+        expect $ pround # (5 / 2) #== 2
+    , testCase "round 7/2" $
+        expect $ pround # (7 / 2) #== 4
+    , testCase "round 9/2" $
+        expect $ pround # (9 / 2) #== 4
+    , testCase "round 11/2" $
+        expect $ pround # (11 / 2) #== 6
+    , testCase "round 9/4" $
+        expect $ pround # (9 / 4) #== 2
+    , testCase "round 11/4" $
+        expect $ pround # (11 / 4) #== 3
+    , testCase "round -1/3" $
+        expect $ pround # (-1 / 3) #== 0
+    , testCase "round -1/2" $
+        expect $ pround # (-1 / 2) #== 0
+    , testCase "round -2/3" $
+        expect $ pround # (-2 / 3) #== -1
+    , testCase "round -3/2" $
+        expect $ pround # (-3 / 2) #== -2
+    , testCase "round -5/2" $
+        expect $ pround # (-5 / 2) #== -2
+    , testCase "truncate 5/4" $
+        expect $ ptruncate # (5 / 4) #== 1
+    , testCase "truncate 3/2" $
+        expect $ ptruncate # (3 / 2) #== 1
+    , testCase "truncate 7/4" $
+        expect $ ptruncate # (7 / 4) #== 1
+    , testCase "truncate 1/4" $
+        expect $ ptruncate # (1 / 4) #== 0
+    , testCase "truncate -1/4" $
+        expect $ ptruncate # (-1 / 4) #== 0
+    , testCase "truncate -7/4" $
+        expect $ ptruncate # (-7 / 4) #== -1
+    , testCase "properFraction 11/7" $
+        expect $
+          pmatch (pproperFraction # (11 / 7)) $ \(PPair x y) ->
+            x #== 1 #&& y #== (4 / 7)
+    , testCase "properFraction 13/7" $
+        expect $
+          pmatch (pproperFraction # (13 / 7)) $ \(PPair x y) ->
+            x #== 1 #&& y #== (6 / 7)
+    , testCase "properFraction -1/2" $
+        expect $
+          pmatch (pproperFraction # (-1 / 2)) $ \(PPair x y) ->
+            x #== 0 #&& y #== (-1 / 2)
+    , testCase "properFraction -3/2" $
+        expect $
+          pmatch (pproperFraction # (-3 / 2)) $ \(PPair x y) ->
+            x #== -1 #&& y #== (-1 / 2)
+    , testCase "properFraction -4/3" $
+        expect $
+          pmatch (pproperFraction # (-4 / 3)) $ \(PPair x y) ->
+            x #== -1 #&& y #== (-1 / 3)
+    , testCase "0.5 literal" $
+        printTerm (0.5 :: Term s PRational) @?= "(program 1.0.0 (\\i0 -> i1 1 2))"
+    , -- most print tests are impractical to read
+      -- and varify by hand because reduce is fairly
+      -- complicated and used in even fairly short tests
+      testCase "pfromData . pdata = id" $ do
+        expect $ (0.5 :: Term s PRational) #== pfromData (pdata 0.5)
+        expect $ (2 :: Term s PRational) #== pfromData (pdata 2)
+        expect $ (3 :: Term s PRational) #== pfromData (pdata 3)
+        expect $ ((1 / 3) :: Term s PRational) #== pfromData (pdata (1 / 3))
+        expect $ ((11 / 7) :: Term s PRational) #== pfromData (pdata (11 / 7))
+    ]
diff --git a/examples/Main.hs b/examples/Main.hs
index f35da51c2..f94750b52 100644
--- a/examples/Main.hs
+++ b/examples/Main.hs
@@ -11,7 +11,7 @@ import qualified Data.ByteString as BS
 import Data.Maybe (fromJust)
 import qualified Examples.List as List
 import Examples.Tracing (traceTests)
-import Plutarch (POpaque, pconstant, plift', popaque, printTerm, punsafeBuiltin)
+import Plutarch (POpaque, popaque, printTerm, punsafeBuiltin)
 import Plutarch.Api.V1 (PScriptPurpose (PMinting))
 import Plutarch.Bool (PBool (PFalse, PTrue), pand, pif, pnot, por, (#&&), (#<), (#<=), (#==), (#||))
 import Plutarch.Builtin (PBuiltinList (..), PBuiltinPair, PData, PIsData (..), pdata)
@@ -19,6 +19,7 @@ import Plutarch.ByteString (PByteString, pconsBS, phexByteStr, pindexBS, plength
 import Plutarch.Either (PEither (PLeft, PRight))
 import Plutarch.Integer (PInteger)
 import Plutarch.Internal (punsafeConstantInternal)
+import Plutarch.Lift (pconstant, plift')
 import Plutarch.Prelude
 import Plutarch.String (PString)
 import Plutarch.Unit (PUnit (..))
@@ -30,6 +31,7 @@ import qualified PlutusTx
 import qualified Examples.Api as Api
 import qualified Examples.LetRec as LetRec
 import qualified Examples.PlutusType as PlutusType
+import qualified Examples.Rationals as Rationals
 import qualified Examples.Recursion as Recursion
 import Utils
 
@@ -86,6 +88,7 @@ tests =
     , Recursion.tests
     , Api.tests
     , List.tests
+    , Rationals.tests
     , LetRec.tests
     ]
 
diff --git a/examples/Utils.hs b/examples/Utils.hs
index c5c1e0356..6c6eb0853 100644
--- a/examples/Utils.hs
+++ b/examples/Utils.hs
@@ -4,11 +4,11 @@
 module Utils (HasTester, standardTester, eval, equal, equalBudgeted, equal', fails, expect, throws, traces) where
 
 import Control.Exception (SomeException, try)
-import Data.Kind (Type)
 import Data.Text (Text)
-import Plutarch (ClosedTerm, PCon (pcon), Term, compile, printScript)
+import Plutarch (ClosedTerm, compile, printScript)
 import Plutarch.Bool (PBool (PTrue))
 import Plutarch.Evaluate (evaluateBudgetedScript, evaluateScript)
+import Plutarch.Prelude
 import qualified Plutus.V1.Ledger.Scripts as Scripts
 import PlutusCore.Evaluation.Machine.ExBudget (ExBudget (ExBudget))
 import qualified PlutusCore.Evaluation.Machine.ExMemory as ExMemory
@@ -16,13 +16,13 @@ import qualified PlutusCore.Evaluation.Machine.ExMemory as ExMemory
 --import Shrink (shrinkScript)
 import Test.Tasty.HUnit
 
-newtype EvalImpl = EvalImpl {runEvalImpl :: forall k (a :: k -> Type). HasCallStack => ClosedTerm a -> IO Scripts.Script}
-newtype EqualImpl = EqualImpl {runEqualImpl :: forall k (a :: k -> Type) (b :: k -> Type). HasCallStack => ClosedTerm a -> ClosedTerm b -> Assertion}
-newtype Equal'Impl = Equal'Impl {runEqual'Impl :: forall k (a :: k -> Type). HasCallStack => ClosedTerm a -> String -> Assertion}
-newtype FailsImpl = FailsImpl {runFailsImpl :: forall k (a :: k -> Type). HasCallStack => ClosedTerm a -> Assertion}
-newtype ExpectImpl = ExpectImpl {runExpectImpl :: forall (k :: Type). HasCallStack => ClosedTerm @k PBool -> Assertion}
-newtype ThrowsImpl = ThrowsImpl {runThrowsImpl :: forall k (a :: k -> Type). ClosedTerm a -> Assertion}
-newtype TracesImpl = TracesImpl {runTracesImpl :: forall k (a :: k -> Type). ClosedTerm a -> [Text] -> Assertion}
+newtype EvalImpl = EvalImpl {runEvalImpl :: forall (a :: PType). HasCallStack => ClosedTerm a -> IO Scripts.Script}
+newtype EqualImpl = EqualImpl {runEqualImpl :: forall (a :: PType) (b :: PType). HasCallStack => ClosedTerm a -> ClosedTerm b -> Assertion}
+newtype Equal'Impl = Equal'Impl {runEqual'Impl :: forall (a :: PType). HasCallStack => ClosedTerm a -> String -> Assertion}
+newtype FailsImpl = FailsImpl {runFailsImpl :: forall (a :: PType). HasCallStack => ClosedTerm a -> Assertion}
+newtype ExpectImpl = ExpectImpl {runExpectImpl :: HasCallStack => ClosedTerm PBool -> Assertion}
+newtype ThrowsImpl = ThrowsImpl {runThrowsImpl :: forall (a :: PType). ClosedTerm a -> Assertion}
+newtype TracesImpl = TracesImpl {runTracesImpl :: forall (a :: PType). ClosedTerm a -> [Text] -> Assertion}
 
 data Tester = Tester
   { evalImpl :: EvalImpl
@@ -143,7 +143,7 @@ shrinkTester =
 
 eval :: (HasCallStack, HasTester) => ClosedTerm a -> IO Scripts.Script
 eval = runEvalImpl (evalImpl ?tester)
-equal :: forall k (a :: k -> Type) (b :: k -> Type). (HasCallStack, HasTester) => ClosedTerm @k a -> ClosedTerm @k b -> Assertion
+equal :: forall (a :: PType) (b :: PType). (HasCallStack, HasTester) => ClosedTerm a -> ClosedTerm b -> Assertion
 equal x y = runEqualImpl (equalImpl ?tester) x y
 equal' :: (HasCallStack, HasTester) => ClosedTerm a -> String -> Assertion
 equal' = runEqual'Impl (equal'Impl ?tester)
diff --git a/flake.nix b/flake.nix
index 294cbdb82..a95b7d5b5 100644
--- a/flake.nix
+++ b/flake.nix
@@ -43,6 +43,81 @@
 
   outputs = inputs@{ self, nixpkgs, haskell-nix, plutus, flake-compat-ci, ... }:
     let
+      extraSources = [
+        {
+          src = inputs.protolude;
+          subdirs = [ "." ];
+        }
+        {
+          src = inputs.foundation;
+          subdirs = [
+            "foundation"
+            "basement"
+          ];
+        }
+        {
+          src = inputs.cardano-prelude;
+          subdirs = [
+            "cardano-prelude"
+            # "cardano-prelude-test"
+          ];
+        }
+        {
+          src = inputs.hs-memory;
+          subdirs = [ "." ];
+        }
+        {
+          src = inputs.cardano-crypto;
+          subdirs = [ "." ];
+        }
+        {
+          src = inputs.cryptonite;
+          subdirs = [ "." ];
+        }
+        {
+          src = inputs.flat;
+          subdirs = [ "." ];
+        }
+        {
+          src = inputs.cardano-base;
+          subdirs = [
+           # "base-deriving-via"
+            "binary"
+           # "binary/test"
+           "cardano-crypto-class"
+           # "cardano-crypto-praos"
+           # "cardano-crypto-tests"
+           # "measures"
+           # "orphans-deriving-via"
+           # "slotting"
+           # "strict-containers"
+          ];
+        }
+        {
+          src = inputs.sized-functors;
+          subdirs = [ "." ];
+        }
+        {
+          src = inputs.th-extras;
+          subdirs = [ "." ];
+        }
+        {
+          src = inputs.plutus;
+          subdirs = [
+            #"plutus-benchmark"
+            "plutus-core"
+            #"plutus-errors"
+            "plutus-ledger-api"
+            #"plutus-metatheory"
+            "plutus-tx"
+            #"plutus-tx-plugin"
+            "prettyprinter-configurable"
+            "word-array"
+            #"stubs/plutus-ghc-stub"
+          ];
+        }
+      ];
+
       supportedSystems = with nixpkgs.lib.systems.supported; tier1 ++ tier2 ++ tier3;
 
       perSystem = nixpkgs.lib.genAttrs supportedSystems;
@@ -57,92 +132,7 @@
           src = ./.;
           compiler-nix-name = "ghc921";
           cabalProjectFileName = "cabal.project";
-          extraSources = [
-            {
-              src = inputs.protolude;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.foundation;
-              subdirs = [
-                "foundation"
-                "basement"
-              ];
-            }
-            {
-              src = inputs.cardano-prelude;
-              subdirs = [
-                "cardano-prelude"
-                # "cardano-prelude-test"
-              ];
-            }
-            {
-              src = inputs.hs-memory;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.cardano-crypto;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.cryptonite;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.flat;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.cardano-base;
-              subdirs = [
-               # "base-deriving-via"
-                "binary"
-               # "binary/test"
-               "cardano-crypto-class"
-               # "cardano-crypto-praos"
-               # "cardano-crypto-tests"
-               # "measures"
-               # "orphans-deriving-via"
-               # "slotting"
-               # "strict-containers"
-              ];
-            }
-            {
-              src = inputs.sized-functors;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.th-extras;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.plutus;
-              subdirs = [
-                #"plutus-benchmark"
-                "plutus-core"
-                #"plutus-errors"
-                "plutus-ledger-api"
-                #"plutus-metatheory"
-                "plutus-tx"
-                #"plutus-tx-plugin"
-                "prettyprinter-configurable"
-                "word-array"
-                #"stubs/plutus-ghc-stub"
-              ];
-            }
-          ];
-          /*
-          extraSources = [
-            {
-              src = inputs.Win32-network;
-              subdirs = [ "." ];
-            }
-            {
-              src = inputs.Shrinker;
-              subdirs = [ "." "testing" ];
-            }
-          ];
-          */
+          inherit extraSources;
           modules = [{
             packages = {
               basement.src = "${inputs.foundation}/basement";
@@ -202,8 +192,6 @@
 
             additional = ps: [
               ps.plutus-ledger-api
-              #ps.plutus-tx
-              #ps.plutus-ledger-api
               #ps.shrinker
               #ps.shrinker-testing
             ];
@@ -227,6 +215,8 @@
           ;
     in
     {
+      inherit extraSources;
+
       project = perSystem projectFor;
       flake = perSystem (system: (projectFor system).flake {});
 
@@ -236,6 +226,7 @@
         self.flake.${system}.checks
         // {
           formatCheck = formatCheckFor system;
+          benchmark = (nixpkgsFor system).runCommand "benchmark" { } "${self.apps.${system}.benchmark.program} | tee $out";
         }
       );
       check = perSystem (system:
@@ -243,7 +234,15 @@
           nativeBuildInputs = builtins.attrValues self.checks.${system};
         } "touch $out"
       );
-      apps = perSystem (system: self.flake.${system}.apps);
+      apps = perSystem (system: 
+        self.flake.${system}.apps
+        // {
+            benchmark = {
+            type = "app";
+            program = "${self.flake.${system}.packages."plutarch:bench:perf"}/bin/perf";
+          };
+        }
+      );
       devShell = perSystem (system: self.flake.${system}.devShell);
 
       nixCi = flake-compat-ci.lib.recurseIntoFlakeWith {
diff --git a/plutarch.cabal b/plutarch.cabal
index 8441ef88b..91cff974c 100644
--- a/plutarch.cabal
+++ b/plutarch.cabal
@@ -129,6 +129,7 @@ test-suite examples
     Examples.List
     Examples.PlutusType
     Examples.Recursion
+    Examples.Rationals
     Examples.Tracing
     Utils
 
@@ -148,3 +149,25 @@ test-suite examples
 
   if flag(development)
     cpp-options: -DDevelopment
+
+benchmark perf
+  import:         c 
+  type:           exitcode-stdio-1.0
+  hs-source-dirs: bench
+  main-is:        Main.hs 
+  other-modules: Benchmark
+  build-depends:
+    , base
+    , boxes
+    , bytestring
+    , cassava
+    , foldl
+    , mtl
+    , plutarch
+    , serialise
+    , plutus-core
+    , plutus-ledger-api
+    , text
+    , flat
+    , data-default
+