Skip to content

Commit

Permalink
[Builtins] Split 'KnownTypeIn' into two classes
Browse files Browse the repository at this point in the history
  • Loading branch information
@effectfully
effectfully committed Mar 23, 2022
1 parent dc92754 commit f891cc6
Show file tree
Hide file tree
Showing 19 changed files with 222 additions and 129 deletions.
1 change: 1 addition & 0 deletions nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions plutus-core/plutus-core.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,6 +170,7 @@ library
PlutusCore.Builtin.Meaning
PlutusCore.Builtin.Polymorphism
PlutusCore.Builtin.Runtime
PlutusCore.Builtin.TestKnown
PlutusCore.Builtin.TypeScheme
PlutusCore.Core.Instance
PlutusCore.Core.Instance.Eq
Expand Down
3 changes: 2 additions & 1 deletion plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,8 +149,9 @@ instance KnownTypeAst DefaultUni Void where
toTypeAst _ = runQuote $ do
a <- freshTyName "a"
pure $ TyForall () a (Type ()) $ TyVar () a
instance UniOf term ~ DefaultUni => KnownTypeIn DefaultUni term Void where
instance UniOf term ~ DefaultUni => MakeKnownIn DefaultUni term Void where
makeKnown _ = absurd
instance UniOf term ~ DefaultUni => ReadKnownIn DefaultUni term Void where
readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift a 'Void'" mayCause

data BuiltinErrorCall = BuiltinErrorCall
Expand Down
1 change: 1 addition & 0 deletions plutus-core/plutus-core/src/PlutusCore/Builtin.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,4 +12,5 @@ import PlutusCore.Builtin.KnownTypeAst as Export
import PlutusCore.Builtin.Meaning as Export
import PlutusCore.Builtin.Polymorphism as Export
import PlutusCore.Builtin.Runtime as Export
import PlutusCore.Builtin.TestKnown as Export
import PlutusCore.Builtin.TypeScheme as Export
166 changes: 85 additions & 81 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/KnownType.hs
View file
Original file line number Diff line number Diff line change
@@ -1,18 +1,17 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module PlutusCore.Builtin.KnownType
( MakeKnownError
Expand All @@ -22,19 +21,19 @@ module PlutusCore.Builtin.KnownType
, KnownBuiltinTypeIn
, KnownBuiltinType
, readKnownConstant
, KnownTypeIn (..)
, KnownType
, MakeKnownIn (..)
, MakeKnown
, ReadKnownIn (..)
, ReadKnown
, makeKnownRun
, makeKnownOrFail
, readKnownSelf
, TestTypesFromTheUniverseAreAllKnown
) where

import PlutusPrelude (reoption)

import PlutusCore.Builtin.Emitter
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.KnownTypeAst
import PlutusCore.Builtin.Polymorphism
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception
Expand All @@ -47,6 +46,7 @@ import Data.DList (DList)
import Data.String
import Data.Text (Text)
import GHC.Exts (inline, oneShot)
import GHC.TypeLits
import Universe

-- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\".
Expand All @@ -55,35 +55,31 @@ type KnownBuiltinTypeIn uni val a = (HasConstantIn uni val, GShow uni, GEq uni,
-- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\".
type KnownBuiltinType val a = KnownBuiltinTypeIn (UniOf val) val a

{- Note [Performance of KnownTypeIn instances]
{- Note [Performance of ReadKnownIn and MakeKnownIn instances]
It's critically important that 'readKnown' runs in the concrete 'Either' rather than a general
'MonadError'. Changing from the latter to the former gave us a speedup of up to 19%, see
https://github.com/input-output-hk/plutus/pull/4307
The same does not apply to 'makeKnown' however and so we keep 'MonadError' there, see
https://github.com/input-output-hk/plutus/pull/4308
Although there's a different kind of inlining that helps in case of 'makeKnown', see the first
commit and the first comment of https://github.com/input-output-hk/plutus/pull/4251
We don't have it merged currently though, because there's a hope for a better solution.
Replacing the @AsUnliftingError err, AsEvaluationFailure err@ constraints with the dedicated
'ReadKnownError' data type gave us a speedup of up to 4%.
Even though we don't use 'makeKnown' and 'readKnown' directly over concrete types, it's still
beneficial to inline them, because otherwise GHC compiles each of them to two definitions
(one calling the other) for some reason. So always add an @INLINE@ pragma to all definitions
of 'makeKnown' and 'readKnown' unless you have a specific reason not to.
All the same considerations apply to 'makeKnown': https://github.com/input-output-hk/plutus/pull/4421
Similarly, we inline implementations of 'toTypeAst' just to get tidier Core.
It's beneficial to inline 'readKnown' and 'makeKnown' not only because we use them directly over
concrete types once 'toBuiltinsRuntime' is inlined, but also because otherwise GHC compiles each of
them to two definitions (one calling the other) for some reason.
So always add an @INLINE@ pragma to all definitions of 'makeKnown' and 'readKnown' unless you have
a specific reason not to.
Some 'readKnown' implementations require inserting a call to 'oneShot'. E.g. if 'oneShot' is not
used in 'readKnownConstant' then 'GHC pulls @gshow uniExp@ out of the 'Nothing' branch, thus
allocating a thunk of type 'String' that is completely redundant whenever there's no error,
which is the majority of cases. And putting 'oneShot' as the outermost call results in
worse Core.
Any change to an instance of 'KnownTypeIn', even completely trivial, requires looking into the
generated Core, since compilation of these instances is extremely brittle optimization-wise.
Any change to an instance of 'ReadKnownIn' or 'MakeKnownIn', even completely trivial, requires
looking into the generated Core, since compilation of these instances is extremely brittle
optimization-wise.
Things to watch out for are unnecessary sharing (for example, a @let@ appearing outside of a @case@
allocates a thunk and if that thunk is not referenced inside of one of the branches, then it's
Expand All @@ -105,7 +101,7 @@ any different from just 'Integer' unlifting-wise.
However there's no sensible way of unlifting a value of, say, @[a]@ where @a@ in not a built-in
type. So let's say we instantiated @a@ to an @Opaque val rep@ like we do for polymorphic functions
that don't deal with polymorphic built-in types (e.g. `id`, `ifThenElse` etc). That would mean we'd
that don't deal with polymorphic built-in types (e.g. @id@, @ifThenElse@ etc). That would mean we'd
need to write a function from a @[a]@ for some arbitrary built-in @a@ to @[Opaque val a]@. Which
is really easy to do: it's just @map makeKnown@. But the problem is, unlifting is supposed to be
cheap and that @map@ is O(n), so for example 'MkCons' would become an O(n) operation making
Expand Down Expand Up @@ -154,6 +150,17 @@ Overall, asking the user to manually unlift from @SomeConstant uni [a]@ is just
faster than any kind of fancy encoding.
-}

{- Note [Alignment of ReadKnownIn and MakeKnownIn]
We keep 'ReadKnownIn' and 'MakeKnownIn' separate, because values of some types can only be lifted
and not unlifted, for example 'EvaluationResult' and 'Emitter' can't appear in argument position.
'KnownTypeAst' is not a superclass of ReadKnownIn and MakeKnownIn. This is due to the fact that
polymorphic built-in types are only liftable/unliftable when they're fully monomorphized, while
'toTypeAst' works for polymorphic built-in types that have type variables in them, and so the
constraints are completely different in the two cases and we keep the two concepts apart
(there doesn't seem to be any cons to that).
-}

-- | The type of errors that 'makeKnown' can return.
data MakeKnownError
= MakeKnownEvaluationFailure
Expand Down Expand Up @@ -214,22 +221,18 @@ readKnownConstant mayCause val = asConstant mayCause val >>= oneShot \case
throwingWithCause _UnliftingError err mayCause
{-# INLINE readKnownConstant #-}

-- See Note [Performance of KnownTypeIn instances].
-- We use @default@ for providing instances for built-in types instead of @DerivingVia@, because
-- the latter breaks on @m term@ (and for brevity).
-- | Haskell types known to exist on the PLC side.
-- Both the methods take a @Maybe cause@ argument to report the cause of a potential failure.
-- @cause@ is different to @term@ to support evaluators that distinguish between terms and values
-- (@makeKnown@ normally constructs a value, but it's convenient to report the cause of a failure
-- as a term). Note that an evaluator might require the cause to be computed lazily for best
-- performance on the happy path and @Maybe@ ensures that even if we somehow force the argument,
-- the cause stored in it is not forced due to @Maybe@ being a lazy data type.
-- Note that 'KnownTypeAst' is not a superclass of 'KnownTypeIn'. This is due to the fact that
-- polymorphic built-in types are only liftable/unliftable when they're fully monomorphized, while
-- 'toTypeAst' works for polymorphic built-in types that have type variables in them, and so the
-- constraints are completely different in the two cases and we keep the two classes apart
-- (there doesn't seem to be any cons to that).
class uni ~ UniOf val => KnownTypeIn uni val a where
{- Note [Cause of failure]
'readKnown' and 'makeKnown' each take a @Maybe cause@ argument to report the cause of a potential
failure. @cause@ is different to @val@ to support evaluators that distinguish between terms and
values (@makeKnown@ normally constructs a value, but it's convenient to report the cause of a failure
as a term). Note that an evaluator might require the cause to be computed lazily for best
performance on the happy path and @Maybe@ ensures that even if we somehow force the argument,
the cause stored in it is not forced due to @Maybe@ being a lazy data type.
-}

-- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
class uni ~ UniOf val => MakeKnownIn uni val a where
-- See Note [Cause of failure].
-- | Convert a Haskell value to the corresponding PLC val.
-- The inverse of 'readKnown'.
makeKnown :: Maybe cause -> a -> ExceptT (ErrorWithCause MakeKnownError cause) Emitter val
Expand All @@ -242,6 +245,11 @@ class uni ~ UniOf val => KnownTypeIn uni val a where
makeKnown _ x = pure . fromConstant . someValue $! x
{-# INLINE makeKnown #-}

type MakeKnown val = MakeKnownIn (UniOf val) val

-- See Note [Performance of ReadKnownIn and MakeKnownIn instances].
class uni ~ UniOf val => ReadKnownIn uni val a where
-- See Note [Cause of failure].
-- | Convert a PLC val to the corresponding Haskell value.
-- The inverse of 'makeKnown'.
readKnown :: Maybe cause -> val -> Either (ErrorWithCause ReadKnownError cause) a
Expand All @@ -252,74 +260,70 @@ class uni ~ UniOf val => KnownTypeIn uni val a where
readKnown = inline readKnownConstant
{-# INLINE readKnown #-}

-- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'.
type KnownType val a = (KnownTypeAst (UniOf val) a, KnownTypeIn (UniOf val) val a)
type ReadKnown val = ReadKnownIn (UniOf val) val

makeKnownRun
:: KnownTypeIn uni val a
:: MakeKnownIn uni val a
=> Maybe cause -> a -> (Either (ErrorWithCause MakeKnownError cause) val, DList Text)
makeKnownRun mayCause = runEmitter . runExceptT . makeKnown mayCause
{-# INLINE makeKnownRun #-}

-- | Same as 'makeKnown', but allows for neither emitting nor storing the cause of a failure.
makeKnownOrFail :: KnownTypeIn uni val a => a -> EvaluationResult val
makeKnownOrFail :: MakeKnownIn uni val a => a -> EvaluationResult val
makeKnownOrFail = reoption . fst . makeKnownRun Nothing
{-# INLINE makeKnownOrFail #-}

-- | Same as 'readKnown', but the cause of a potential failure is the provided term itself.
readKnownSelf
:: ( KnownType val a
:: ( ReadKnown val a
, AsUnliftingError err, AsEvaluationFailure err
)
=> val -> Either (ErrorWithCause err val) a
readKnownSelf val = either throwReadKnownErrorWithCause pure $ readKnown (Just val) val
{-# INLINE readKnownSelf #-}

-- | For providing a 'KnownTypeIn' instance for a built-in type it's enough for that type to satisfy
-- 'KnownBuiltinTypeIn', hence the definition.
class (forall val. KnownBuiltinTypeIn uni val a => KnownTypeIn uni val a) =>
ImplementedKnownBuiltinTypeIn uni a
instance (forall val. KnownBuiltinTypeIn uni val a => KnownTypeIn uni val a) =>
ImplementedKnownBuiltinTypeIn uni a

-- | An instance of this class not having any constraints ensures that every type
-- (according to 'Everywhere') from the universe has a 'KnownTypeIn' instance.
class uni `Everywhere` ImplementedKnownBuiltinTypeIn uni => TestTypesFromTheUniverseAreAllKnown uni

instance KnownTypeIn uni val a => KnownTypeIn uni val (EvaluationResult a) where
instance MakeKnownIn uni val a => MakeKnownIn uni val (EvaluationResult a) where
makeKnown mayCause EvaluationFailure = throwingWithCause _EvaluationFailure () mayCause
makeKnown mayCause (EvaluationSuccess x) = makeKnown mayCause x
{-# INLINE makeKnown #-}

-- Catching 'EvaluationFailure' here would allow *not* to short-circuit when 'readKnown' fails
-- to read a Haskell value of type @a@. Instead, in the denotation of the builtin function
-- the programmer would be given an explicit 'EvaluationResult' value to handle, which means
-- that when this value is 'EvaluationFailure', a PLC 'Error' was caught.
-- I.e. it would essentially allow us to catch errors and handle them in a programmable way.
-- We forbid this, because it complicates code and isn't supported by evaluation engines anyway.
-- Catching 'EvaluationFailure' here would allow *not* to short-circuit when 'readKnown' fails
-- to read a Haskell value of type @a@. Instead, in the denotation of the builtin function
-- the programmer would be given an explicit 'EvaluationResult' value to handle, which means
-- that when this value is 'EvaluationFailure', a PLC 'Error' was caught.
-- I.e. it would essentially allow us to catch errors and handle them in a programmable way.
-- We forbid this, because it complicates code and isn't supported by evaluation engines anyway.
instance
( TypeError ('Text "‘EvaluationResult’ cannot appear in the type of an argument")
, uni ~ UniOf val
) => ReadKnownIn uni val (EvaluationResult a) where
readKnown mayCause _ =
throwingWithCause _UnliftingError "Error catching is not supported" mayCause
{-# INLINE readKnown #-}
throwingWithCause _UnliftingError "Panic: 'TypeError' was bypassed" mayCause

instance KnownTypeIn uni val a => KnownTypeIn uni val (Emitter a) where
instance MakeKnownIn uni val a => MakeKnownIn uni val (Emitter a) where
makeKnown mayCause a = lift a >>= makeKnown mayCause
{-# INLINE makeKnown #-}

-- TODO: we really should tear 'KnownType' apart into two separate type classes.
readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift an 'Emitter'" mayCause
{-# INLINE readKnown #-}
instance
( TypeError ('Text "‘Emitter’ cannot appear in the type of an argument")
, uni ~ UniOf val
) => ReadKnownIn uni val (Emitter a) where
readKnown mayCause _ =
throwingWithCause _UnliftingError "Panic: 'TypeError' was bypassed" mayCause

instance HasConstantIn uni val => KnownTypeIn uni val (SomeConstant uni rep) where
instance HasConstantIn uni val => MakeKnownIn uni val (SomeConstant uni rep) where
makeKnown _ = coerceArg $ pure . fromConstant
{-# INLINE makeKnown #-}

instance HasConstantIn uni val => ReadKnownIn uni val (SomeConstant uni rep) where
readKnown = coerceVia (\asC mayCause -> fmap SomeConstant . asC mayCause) asConstant
{-# INLINE readKnown #-}

instance uni ~ UniOf val => KnownTypeIn uni val (Opaque val rep) where
instance uni ~ UniOf val => MakeKnownIn uni val (Opaque val rep) where
makeKnown _ = coerceArg pure -- A faster @pure . Opaque@.
{-# INLINE makeKnown #-}

instance uni ~ UniOf val => ReadKnownIn uni val (Opaque val rep) where
readKnown _ = coerceArg pure -- A faster @pure . Opaque@.
{-# INLINE readKnown #-}

Expand Down
9 changes: 6 additions & 3 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Meaning.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,12 +124,15 @@ class KnownMonotype val args res a | args res -> a, a -> res where
knownMonotype :: TypeScheme val args res

-- | Once we've run out of term-level arguments, we return a 'TypeSchemeResult'.
instance (res ~ res', KnownType val res) => KnownMonotype val '[] res res' where
instance (res ~ res', KnownTypeAst (UniOf val) res, MakeKnown val res) =>
KnownMonotype val '[] res res' where
knownMonotype = TypeSchemeResult

-- | Every term-level argument becomes as 'TypeSchemeArrow'.
instance (KnownType val arg, KnownMonotype val args res a) =>
KnownMonotype val (arg ': args) res (arg -> a) where
instance
( KnownTypeAst (UniOf val) arg, MakeKnown val arg, ReadKnown val arg
, KnownMonotype val args res a
) => KnownMonotype val (arg ': args) res (arg -> a) where
knownMonotype = TypeSchemeArrow knownMonotype

-- | A class that allows us to derive a polytype for a builtin.
Expand Down
5 changes: 2 additions & 3 deletions plutus-core/plutus-core/src/PlutusCore/Builtin/Runtime.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,6 @@ import PlutusPrelude
import PlutusCore.Builtin.HasConstant
import PlutusCore.Builtin.Meaning
import PlutusCore.Builtin.TypeScheme
import PlutusCore.Core
import PlutusCore.Evaluation.Machine.Exception

import Control.DeepSeq
Expand All @@ -26,10 +25,10 @@ import PlutusCore.Builtin.KnownType
-- | Same as 'TypeScheme' except this one doesn't contain any evaluation-irrelevant types stuff.
data RuntimeScheme val (args :: [GHC.Type]) res where
RuntimeSchemeResult
:: KnownTypeIn (UniOf val) val res
:: MakeKnown val res
=> RuntimeScheme val '[] res
RuntimeSchemeArrow
:: KnownTypeIn (UniOf val) val arg
:: ReadKnown val arg
=> RuntimeScheme val args res
-> RuntimeScheme val (arg ': args) res
RuntimeSchemeAll
Expand Down
Loading

0 comments on commit f891cc6

Please sign in to comment.