From 389e74dcd17092ad870a46a9831f5f9047eb9bf7 Mon Sep 17 00:00:00 2001 From: effectfully Date: Sun, 10 Oct 2021 20:17:29 +0300 Subject: [PATCH] [Builtins] [Refactoring] Move 'ToBinds' into 'KnownTypeAst' --- .../examples/PlutusCore/Examples/Builtins.hs | 4 +- .../src/PlutusCore/Constant/Meaning.hs | 58 +--------------- .../src/PlutusCore/Constant/Typed.hs | 69 ++++++++++++++++--- 3 files changed, 63 insertions(+), 68 deletions(-) diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs index fe44b7a667d..7c24823b8ab 100644 --- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs +++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs @@ -130,8 +130,9 @@ defBuiltinsRuntimeExt = toBuiltinsRuntime (defaultBuiltinCostModel, ()) data PlcListRep (a :: GHC.Type) instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where + type ToBinds (PlcListRep a) = ToBinds a + toTypeAst _ = TyApp () Plc.listTy . toTypeAst $ Proxy @a -type instance ToBinds (PlcListRep a) = ToBinds a instance KnownTypeAst uni Void where toTypeAst _ = runQuote $ do @@ -140,7 +141,6 @@ instance KnownTypeAst uni Void where instance KnownType term Void where makeKnown _ = absurd readKnown mayCause _ = throwingWithCause _UnliftingError "Can't unlift a 'Void'" mayCause -type instance ToBinds Void = '[] data BuiltinErrorCall = BuiltinErrorCall deriving (Show, Eq, Exception) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs index 1839ea7b9dd..6d14d842729 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs @@ -21,23 +21,18 @@ module PlutusCore.Constant.Meaning where import PlutusPrelude -import PlutusCore.Constant.Dynamic.Emit import PlutusCore.Constant.Function import PlutusCore.Constant.Typed import PlutusCore.Core -import PlutusCore.Data import PlutusCore.Evaluation.Machine.Exception -import PlutusCore.Evaluation.Result import PlutusCore.Name import Control.Lens (ix, (^?)) import Control.Monad.Except import Data.Array -import qualified Data.ByteString as BS import qualified Data.Kind as GHC import Data.Proxy import Data.Some.GADT -import Data.Text (Text) import Data.Type.Bool import Data.Type.Equality import GHC.TypeLits @@ -67,9 +62,8 @@ data BuiltinMeaning term cost = -- reasons (there isn't much point in caching a value of a type with a constraint as it becomes a -- function at runtime anyway, due to constraints being compiled as dictionaries). --- TODO: we used to have arities and it was justified to precache them before executing an --- evaluator, but now we need to reconsider that. Maybe instantiating 'BuiltinMeaning' on the fly --- is in fact faster. +-- We tried instantiating 'BuiltinMeaning' on the fly and that was sloer than precaching +-- 'BuiltinRuntime's. -- | A 'BuiltinRuntime' represents a possibly partial builtin application. -- We get an initial 'BuiltinRuntime' representing an empty builtin application (i.e. just the -- builtin with no arguments) by instantiating (via 'toBuiltinRuntime') a 'BuiltinMeaning'. @@ -195,52 +189,6 @@ instance (KnownType term arg, KnownMonotype term args res a) => KnownMonotype term (arg ': args) res (arg -> a) where knownMonotype = Proxy `TypeSchemeArrow` knownMonotype --- | Delete all @x@s from a list. -type family Delete x xs :: [a] where - Delete _ '[] = '[] - Delete x (x ': xs) = Delete x xs - Delete x (y ': xs) = y ': Delete x xs - --- | Delete all elements appearing in the first list from the second one and concatenate the lists. -type family Merge xs ys :: [a] where - Merge '[] ys = ys - Merge (x ': xs) ys = x ': Delete x (Merge xs ys) - --- | Collect all unique variables (a variable consists of a textual name, a unique and a kind) --- in an @x@. -type family ToBinds (x :: a) :: [Some TyNameRep] - -type instance ToBinds '[] = '[] -type instance ToBinds (x ': xs) = Merge (ToBinds x) (ToBinds xs) - -type instance ToBinds Integer = '[] -type instance ToBinds BS.ByteString = '[] -type instance ToBinds Text = '[] -type instance ToBinds () = '[] -type instance ToBinds Bool = '[] -type instance ToBinds Int = '[] -type instance ToBinds Data = '[] -type instance ToBinds [] = '[] -type instance ToBinds (,) = '[] -type instance ToBinds [a] = '[] -- One can't directly put a PLC type variable into lists -type instance ToBinds (a, b) = '[] -- or tuples ('SomeConstantOf' has to be used for that), - -- hence we say that polymorphic built-in types can't - -- directly contain any PLC type variables in them. - -type instance ToBinds (EvaluationResult a) = ToBinds a -type instance ToBinds (Emitter a) = ToBinds a -type instance ToBinds (Opaque _ rep) = ToBinds rep -type instance ToBinds (SomeConstant _ rep) = ToBinds rep -type instance ToBinds (SomeConstantOf _ _ reps) = ToBinds reps - -type instance ToBinds (TyVarRep var) = '[ 'Some var ] -type instance ToBinds (TyAppRep fun arg) = Merge (ToBinds fun) (ToBinds arg) -type instance ToBinds (TyForallRep var a) = Delete ('Some var) (ToBinds a) - -type instance ToBinds (TypeScheme term '[] res) = ToBinds res -type instance ToBinds (TypeScheme term (arg ': args) res) = - Merge (ToBinds arg) (ToBinds (TypeScheme term args res)) - -- | A class that allows us to derive a polytype for a builtin. class KnownPolytype (binds :: [Some TyNameRep]) term args res a | args res -> a, a -> res where knownPolytype :: Proxy binds -> TypeScheme term args res @@ -352,7 +300,7 @@ instance {-# OVERLAPPING #-} -- 2. an uninstantiated costing function makeBuiltinMeaning :: forall a term cost binds args res j. - ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ ToBinds (TypeScheme term args res) + ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ Merge (ListToBinds args) (ToBinds res) , KnownPolytype binds term args res a, EnumerateFromTo 0 j term a ) => a -> (cost -> FoldArgsEx args) -> BuiltinMeaning term cost diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 5a1d4e0aff6..c0787d18fe6 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE LambdaCase #-} -- | This module assigns types to built-ins. -- See the @plutus/plutus-core/docs/Constant application.md@ -- article for how this emerged. @@ -8,6 +7,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} @@ -35,6 +35,8 @@ module PlutusCore.Constant.Typed , HasConstant , HasConstantIn , KnownTypeAst (..) + , Merge + , ListToBinds , KnownType (..) , readKnownSelf , makeKnownOrFail @@ -61,6 +63,7 @@ import Data.Functor.Const import qualified Data.Kind as GHC (Type) import Data.Proxy import Data.SOP.Constraint +import qualified Data.Some.GADT as GADT import Data.String import qualified Data.Text as Text import GHC.TypeLits @@ -444,6 +447,14 @@ type HasConstant term = (AsConstant term, FromConstant term) type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term) class KnownTypeAst uni (a :: k) where + -- One can't directly put a PLC type variable into lists or tuples ('SomeConstantOf' has to be + -- used for that), hence we say that polymorphic built-in types can't directly contain any PLC + -- type variables in them just like monomorphic ones. + -- | Collect all unique variables (a variable consists of a textual name, a unique and a kind) + -- in an @a@. + type ToBinds (a :: k) :: [GADT.Some TyNameRep] + type ToBinds _ = '[] + -- | The type representing @a@ used on the PLC side. toTypeAst :: proxy a -> Type TyName uni () default toTypeAst :: uni `Contains` a => proxy a -> Type TyName uni () @@ -455,12 +466,30 @@ type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\". type KnownBuiltinType term a = KnownBuiltinTypeIn (UniOf term) term a -{- Note [KnownType's defaults] -We use @default@ for providing instances for built-in types instead of @DerivingVia@, because the -latter breaks on @m a@ --} - --- See Note [KnownType's defaults]. +-- | Delete all @x@s from a list. +type family Delete x xs :: [a] where + Delete _ '[] = '[] + Delete x (x ': xs) = Delete x xs + Delete x (y ': xs) = y ': Delete x xs + +-- | Delete all elements appearing in the first list from the second one and concatenate the lists. +type family Merge xs ys :: [a] where + Merge '[] ys = ys + Merge (x ': xs) ys = x ': Delete x (Merge xs ys) + +-- There's no sensible way to provide a 'KnownTypeAst' instance for a type-level list, so we +-- create a separate type family. We could have a single type family on the top level for both +-- 'ToBinds' and 'ListToBinds', but then we'd lose a very convenient default of each type from the +-- universe returning an empty list from 'ToBinds' and the user would need to do provide a +-- @type instance@ themselves (which is no big deal, but it's nicer not to ask the user to do that). +-- | Collect all unique variables (a variable consists of a textual name, a unique and a kind) +-- in a list. +type family ListToBinds (x :: [a]) :: [GADT.Some TyNameRep] +type instance ListToBinds '[] = '[] +type instance ListToBinds (x ': xs) = Merge (ToBinds x) (ListToBinds xs) + +-- We use @default@ for providing instances for built-in types instead of @DerivingVia@, because +-- the latter breaks on @m a@ -- | 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 @@ -535,6 +564,8 @@ makeKnownOrFail :: (KnownType term a, MonadError err m, AsEvaluationFailure err) makeKnownOrFail = unNoCauseT . unNoEmitterT . makeKnown Nothing instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where + type ToBinds (EvaluationResult a) = ToBinds a + toTypeAst _ = toTypeAst $ Proxy @a instance (KnownTypeAst (UniOf term) a, KnownType term a) => @@ -552,6 +583,8 @@ instance (KnownTypeAst (UniOf term) a, KnownType term a) => throwingWithCause _UnliftingError "Error catching is not supported" mayCause instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where + type ToBinds (Emitter a) = ToBinds a + toTypeAst _ = toTypeAst $ Proxy @a instance KnownType term a => KnownType term (Emitter a) where @@ -569,6 +602,8 @@ newtype SomeConstant uni rep = SomeConstant } instance (uni ~ uni', KnownTypeAst uni rep) => KnownTypeAst uni (SomeConstant uni' rep) where + type ToBinds (SomeConstant _ rep) = ToBinds rep + toTypeAst _ = toTypeAst $ Proxy @rep instance (HasConstantIn uni term, KnownTypeAst uni rep) => @@ -620,6 +655,8 @@ runSomeConstantOf (SomeConstantOfArg _ svn) = runSomeConstantOf svn instance (uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps) => KnownTypeAst uni (SomeConstantOf uni' f reps) where + type ToBinds (SomeConstantOf uni' f reps) = ListToBinds reps + toTypeAst _ = -- Convert the type-level list of arguments into a term-level one and feed it to @f@. mkIterTyApp () (mkTyBuiltin @_ @f ()) $ @@ -674,15 +711,23 @@ toTyNameAst _ = (Text.pack $ symbolVal @text Proxy) (Unique . fromIntegral $ natVal @uniq Proxy) -instance (KnownSymbol text, KnownNat uniq) => - KnownTypeAst uni (TyVarRep ('TyNameRep text uniq)) where +instance (var ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) => + KnownTypeAst uni (TyVarRep var) where + type ToBinds (TyVarRep var) = '[ 'GADT.Some var ] + toTypeAst _ = TyVar () . toTyNameAst $ Proxy @('TyNameRep text uniq) instance (KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg) where + type ToBinds (TyAppRep fun arg) = Merge (ToBinds fun) (ToBinds arg) + toTypeAst _ = TyApp () (toTypeAst $ Proxy @fun) (toTypeAst $ Proxy @arg) -instance (KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst uni a) => - KnownTypeAst uni (TyForallRep ('TyNameRep @kind text uniq) a) where +instance + ( var ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq + , KnownKind kind, KnownTypeAst uni a + ) => KnownTypeAst uni (TyForallRep var a) where + type ToBinds (TyForallRep var a) = Delete ('GADT.Some var) (ToBinds a) + toTypeAst _ = TyForall () (toTyNameAst $ Proxy @('TyNameRep text uniq)) @@ -690,6 +735,8 @@ instance (KnownSymbol text, KnownNat uniq, KnownKind kind, KnownTypeAst uni a) = (toTypeAst $ Proxy @a) instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where + type ToBinds (Opaque _ rep) = ToBinds rep + toTypeAst _ = toTypeAst $ Proxy @rep instance (term ~ term', KnownTypeAst (UniOf term) rep) => KnownType term (Opaque term' rep) where