From c1beb8a0bb27d471d4e0ea51f9cb9f7f0c055609 Mon Sep 17 00:00:00 2001 From: effectfully Date: Wed, 5 Jan 2022 03:24:05 +0300 Subject: [PATCH 01/13] [Builtins] Disentangle 'KnownTypeAst' from 'KnownTypeIn' --- .../src/PlutusCore/Constant/Typed.hs | 38 ++++++++++--------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 49164e6529a..9b3179d1987 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -514,13 +514,17 @@ type family ListToBinds (x :: [a]) :: [GADT.Some TyNameRep] type instance ListToBinds '[] = '[] type instance ListToBinds (x ': xs) = Merge (ToBinds x) (ListToBinds xs) --- We need to be able to partially apply that in the definition of 'ImplementedKnownBuiltinTypeIn', --- hence defining it as a class synonym. +-- -- We need to be able to partially apply that in the definition of 'ImplementedKnownBuiltinTypeIn', +-- -- hence defining it as a class synonym. +-- -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\". +-- class (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => +-- KnownBuiltinTypeIn uni term a +-- instance (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => +-- KnownBuiltinTypeIn uni term a + -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\". -class (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => - KnownBuiltinTypeIn uni term a -instance (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => - KnownBuiltinTypeIn uni term a + +type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\". type KnownBuiltinType term a = KnownBuiltinTypeIn (UniOf term) term a @@ -591,7 +595,7 @@ readKnownConstant mayCause term = asConstant mayCause term >>= oneShot \case -- 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. -class (uni ~ UniOf term, KnownTypeAst uni a) => KnownTypeIn uni term a where +class uni ~ UniOf term => KnownTypeIn uni term a where -- | Convert a Haskell value to the corresponding PLC term. -- The inverse of 'readKnown'. makeKnown @@ -624,8 +628,12 @@ class (uni ~ UniOf term, KnownTypeAst uni a) => KnownTypeIn uni term a where readKnown = inline readKnownConstant {-# INLINE readKnown #-} +-- -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'. +-- class (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a +-- instance (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a + -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'. -type KnownType term = KnownTypeIn (UniOf term) term +type KnownType term a = (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself. readKnownSelf @@ -669,8 +677,7 @@ instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where toTypeAst _ = toTypeAst $ Proxy @a {-# INLINE toTypeAst #-} -instance (KnownTypeAst uni a, KnownTypeIn uni term a) => - KnownTypeIn uni term (EvaluationResult a) where +instance KnownTypeIn uni term a => KnownTypeIn uni term (EvaluationResult a) where makeKnown _ mayCause EvaluationFailure = throwingWithCause _EvaluationFailure () mayCause makeKnown emit mayCause (EvaluationSuccess x) = makeKnown emit mayCause x {-# INLINE makeKnown #-} @@ -714,8 +721,7 @@ instance (uni ~ uni', KnownTypeAst uni rep) => KnownTypeAst uni (SomeConstant un toTypeAst _ = toTypeAst $ Proxy @rep {-# INLINE toTypeAst #-} -instance (HasConstantIn uni term, KnownTypeAst uni rep) => - KnownTypeIn uni term (SomeConstant uni rep) where +instance (uni ~ uni', HasConstantIn uni term) => KnownTypeIn uni term (SomeConstant uni' rep) where makeKnown _ _ = coerceArg $ pure . fromConstant {-# INLINE makeKnown #-} @@ -743,9 +749,8 @@ instance (uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps) => [] {-# INLINE toTypeAst #-} -instance ( uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps - , HasConstantIn uni term - ) => KnownTypeIn uni term (SomeConstantPoly uni f reps) where +instance (uni ~ uni', HasConstantIn uni term) => + KnownTypeIn uni term (SomeConstantPoly uni' f reps) where makeKnown _ _ = coerceArg $ pure . fromConstant {-# INLINE makeKnown #-} @@ -792,8 +797,7 @@ instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where toTypeAst _ = toTypeAst $ Proxy @rep {-# INLINE toTypeAst #-} -instance (term ~ term', uni ~ UniOf term, KnownTypeAst uni rep) => - KnownTypeIn uni term (Opaque term' rep) where +instance (term ~ term', uni ~ UniOf term) => KnownTypeIn uni term (Opaque term' rep) where makeKnown _ _ = coerceArg pure -- A faster @pure . Opaque@. {-# INLINE makeKnown #-} From 20fd9d80e547a0d0fa24d5701420d719d3f35522 Mon Sep 17 00:00:00 2001 From: effectfully Date: Wed, 5 Jan 2022 16:14:06 +0300 Subject: [PATCH 02/13] Use class synonyms --- .../src/PlutusCore/Constant/Typed.hs | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 9b3179d1987..ae0ace663c9 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -514,17 +514,17 @@ type family ListToBinds (x :: [a]) :: [GADT.Some TyNameRep] type instance ListToBinds '[] = '[] type instance ListToBinds (x ': xs) = Merge (ToBinds x) (ListToBinds xs) --- -- We need to be able to partially apply that in the definition of 'ImplementedKnownBuiltinTypeIn', --- -- hence defining it as a class synonym. --- -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\". --- class (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => --- KnownBuiltinTypeIn uni term a --- instance (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => --- KnownBuiltinTypeIn uni term a +-- We need to be able to partially apply that in the definition of 'ImplementedKnownBuiltinTypeIn', +-- hence defining it as a class synonym. +-- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\". +class (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => + KnownBuiltinTypeIn uni term a +instance (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => + KnownBuiltinTypeIn uni term a -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\". -type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) +-- type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\". type KnownBuiltinType term a = KnownBuiltinTypeIn (UniOf term) term a @@ -628,12 +628,12 @@ class uni ~ UniOf term => KnownTypeIn uni term a where readKnown = inline readKnownConstant {-# INLINE readKnown #-} --- -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'. --- class (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a --- instance (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a - -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'. -type KnownType term a = (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) +class (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a +instance (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a + +-- -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'. +-- type KnownType term a = (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself. readKnownSelf From 4693b29bf512816066920ce03432be38f99bd062 Mon Sep 17 00:00:00 2001 From: effectfully Date: Wed, 5 Jan 2022 19:39:57 +0300 Subject: [PATCH 03/13] Drop some '~' --- .../plutus-core/src/PlutusCore/Constant/Typed.hs | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index ae0ace663c9..95a00d8bbbf 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -715,13 +715,13 @@ newtype SomeConstant uni rep = SomeConstant { unSomeConstant :: Some (ValueOf uni) } -instance (uni ~ uni', KnownTypeAst uni rep) => KnownTypeAst uni (SomeConstant uni' rep) where +instance KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep) where type ToBinds (SomeConstant _ rep) = ToBinds rep toTypeAst _ = toTypeAst $ Proxy @rep {-# INLINE toTypeAst #-} -instance (uni ~ uni', HasConstantIn uni term) => KnownTypeIn uni term (SomeConstant uni' rep) where +instance HasConstantIn uni term => KnownTypeIn uni term (SomeConstant uni rep) where makeKnown _ _ = coerceArg $ pure . fromConstant {-# INLINE makeKnown #-} @@ -736,9 +736,9 @@ newtype SomeConstantPoly uni f reps = SomeConstantPoly { unSomeConstantPoly :: Some (ValueOf uni) } -instance (uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps) => - KnownTypeAst uni (SomeConstantPoly uni' f reps) where - type ToBinds (SomeConstantPoly uni' f reps) = ListToBinds reps +instance (uni `Contains` f, All (KnownTypeAst uni) reps) => + KnownTypeAst uni (SomeConstantPoly uni f reps) where + type ToBinds (SomeConstantPoly uni f reps) = ListToBinds reps toTypeAst _ = -- Convert the type-level list of arguments into a term-level one and feed it to @f@. @@ -749,8 +749,7 @@ instance (uni `Contains` f, uni ~ uni', All (KnownTypeAst uni) reps) => [] {-# INLINE toTypeAst #-} -instance (uni ~ uni', HasConstantIn uni term) => - KnownTypeIn uni term (SomeConstantPoly uni' f reps) where +instance HasConstantIn uni term => KnownTypeIn uni term (SomeConstantPoly uni f reps) where makeKnown _ _ = coerceArg $ pure . fromConstant {-# INLINE makeKnown #-} @@ -797,7 +796,7 @@ instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where toTypeAst _ = toTypeAst $ Proxy @rep {-# INLINE toTypeAst #-} -instance (term ~ term', uni ~ UniOf term) => KnownTypeIn uni term (Opaque term' rep) where +instance uni ~ UniOf term => KnownTypeIn uni term (Opaque term rep) where makeKnown _ _ = coerceArg pure -- A faster @pure . Opaque@. {-# INLINE makeKnown #-} From c42a9f2523c119bac5cb55d5d8274d0486a2590e Mon Sep 17 00:00:00 2001 From: effectfully Date: Wed, 5 Jan 2022 21:45:46 +0300 Subject: [PATCH 04/13] Back to type synonyms --- .../src/PlutusCore/Constant/Typed.hs | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 95a00d8bbbf..d83d7ccbcb1 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -514,17 +514,8 @@ type family ListToBinds (x :: [a]) :: [GADT.Some TyNameRep] type instance ListToBinds '[] = '[] type instance ListToBinds (x ': xs) = Merge (ToBinds x) (ListToBinds xs) --- We need to be able to partially apply that in the definition of 'ImplementedKnownBuiltinTypeIn', --- hence defining it as a class synonym. -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\". -class (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => - KnownBuiltinTypeIn uni term a -instance (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) => - KnownBuiltinTypeIn uni term a - --- | A constraint for \"@a@ is a 'KnownType' by means of being included in @uni@\". - --- type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) +type KnownBuiltinTypeIn uni term a = (HasConstantIn uni term, GShow uni, GEq uni, uni `Contains` a) -- | A constraint for \"@a@ is a 'KnownType' by means of being included in @UniOf term@\". type KnownBuiltinType term a = KnownBuiltinTypeIn (UniOf term) term a @@ -629,11 +620,7 @@ class uni ~ UniOf term => KnownTypeIn uni term a where {-# INLINE readKnown #-} -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'. -class (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a -instance (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) => KnownType term a - --- -- | Haskell types known to exist on the PLC side. See 'KnownTypeIn'. --- type KnownType term a = (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) +type KnownType term a = (KnownTypeAst (UniOf term) a, KnownTypeIn (UniOf term) term a) -- | Same as 'readKnown', but the cause of a potential failure is the provided term itself. readKnownSelf From 00740cde46fb37929ef9cc5c45a349eeb409722a Mon Sep 17 00:00:00 2001 From: effectfully Date: Thu, 6 Jan 2022 16:03:25 +0300 Subject: [PATCH 05/13] Much better 'TypeScheme' inference machinery --- .../examples/PlutusCore/Examples/Builtins.hs | 51 +++---- .../src/PlutusCore/Constant/Meaning.hs | 71 +++++++-- .../src/PlutusCore/Constant/Typed.hs | 138 +++++++++--------- .../src/PlutusCore/Default/Builtins.hs | 32 ++-- .../Golden/ConstrData.plc.golden | 2 +- .../TypeSynthesis/Golden/IdRank2.plc.golden | 2 +- .../TypeSynthesis/Golden/ListData.plc.golden | 2 +- .../TypeSynthesis/Golden/MapData.plc.golden | 2 +- .../TypeSynthesis/Golden/MkNilData.plc.golden | 2 +- .../Golden/MkNilPairData.plc.golden | 2 +- .../Golden/MkPairData.plc.golden | 2 +- .../Golden/UnConstrData.plc.golden | 2 +- .../Golden/UnListData.plc.golden | 2 +- .../TypeSynthesis/Golden/UnMapData.plc.golden | 2 +- .../Golden/UnsafeCoerce.plc.golden | 1 + 15 files changed, 177 insertions(+), 136 deletions(-) create mode 100644 plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerce.plc.golden diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs index 58a05af936f..436c82846cb 100644 --- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs +++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs @@ -102,6 +102,7 @@ data ExtensionFun | ExpensiveSucc | FailingPlus | ExpensivePlus + | UnsafeCoerce | Undefined | Absurd | ErrorPrime -- Like 'Error', but a builtin. What do we even need 'Error' for at this point? @@ -132,6 +133,7 @@ defBuiltinsRuntimeExt = toBuiltinsRuntime (defaultBuiltinCostModel, ()) data PlcListRep (a :: GHC.Type) instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where + type ToHoles (PlcListRep a) = '[ RepInfer a ] type ToBinds (PlcListRep a) = ToBinds a toTypeAst _ = TyApp () Plc.listTy . toTypeAst $ Proxy @a @@ -147,6 +149,8 @@ instance UniOf term ~ DefaultUni => KnownTypeIn DefaultUni term Void where data BuiltinErrorCall = BuiltinErrorCall deriving (Show, Eq, Exception) +-- TODO: JoinOpaque + -- See Note [Representable built-in functions over polymorphic built-in types]. -- We have lists in the universe and so we can define a function like @\x -> [x, x]@ that duplicates -- the constant that it receives. Should memory consumption of that function be linear in the number @@ -179,25 +183,18 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where toBuiltinMeaning IdFInteger = makeBuiltinMeaning - (Prelude.id - :: a ~ Opaque term (TyAppRep (TyVarRep ('TyNameRep "f" 0)) Integer) - => a -> a) + (Prelude.id :: fi ~ Opaque term (TyAppRep f Integer) => fi -> fi) (\_ _ -> ExBudget 1 0) toBuiltinMeaning IdList = makeBuiltinMeaning - (Prelude.id - :: a ~ Opaque term (PlcListRep (TyVarRep ('TyNameRep "a" 0))) - => a -> a) + (Prelude.id :: la ~ Opaque term (PlcListRep a) => la -> la) (\_ _ -> ExBudget 1 0) toBuiltinMeaning IdRank2 = makeBuiltinMeaning (Prelude.id - :: ( f ~ 'TyNameRep "f" 0 - , a ~ 'TyNameRep @GHC.Type "a" 1 - , afa ~ Opaque term (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a))) - ) + :: afa ~ Opaque term (TyForallRep a (TyAppRep (TyVarRep f) (TyVarRep a))) => afa -> afa) (\_ _ -> ExBudget 1 0) @@ -225,6 +222,11 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where (\_ _ -> throw BuiltinErrorCall) (\_ _ _ -> unExRestrictingBudget enormousBudget) + toBuiltinMeaning UnsafeCoerce = + makeBuiltinMeaning + (Opaque . unOpaque) + (\_ _ -> ExBudget 1 0) + toBuiltinMeaning Undefined = makeBuiltinMeaning undefined @@ -244,40 +246,39 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where commaPlc :: SomeConstant uni a -> SomeConstant uni b - -> SomeConstantPoly uni (,) '[a, b] + -> SomeConstant uni (a, b) commaPlc (SomeConstant (Some (ValueOf uniA x))) (SomeConstant (Some (ValueOf uniB y))) = - SomeConstantPoly $ someValueOf (DefaultUniPair uniA uniB) (x, y) + SomeConstant $ someValueOf (DefaultUniPair uniA uniB) (x, y) toBuiltinMeaning BiconstPair = makeBuiltinMeaning biconstPairPlc mempty where biconstPairPlc :: SomeConstant uni a -> SomeConstant uni b - -> SomeConstantPoly uni (,) '[a, b] - -> EvaluationResult (SomeConstantPoly uni (,) '[a, b]) + -> SomeConstant uni (a, b) + -> EvaluationResult (SomeConstant uni (a, b)) biconstPairPlc (SomeConstant (Some (ValueOf uniA x))) (SomeConstant (Some (ValueOf uniB y))) - (SomeConstantPoly (Some (ValueOf uniPairAB _))) = do + (SomeConstant (Some (ValueOf uniPairAB _))) = do DefaultUniPair uniA' uniB' <- pure uniPairAB Just Refl <- pure $ uniA `geq` uniA' Just Refl <- pure $ uniB `geq` uniB' - pure . SomeConstantPoly $ someValueOf uniPairAB (x, y) + pure . SomeConstant $ someValueOf uniPairAB (x, y) toBuiltinMeaning Swap = makeBuiltinMeaning swapPlc mempty where swapPlc - :: SomeConstantPoly uni (,) '[a, b] - -> EvaluationResult (SomeConstantPoly uni (,) '[b, a]) - swapPlc (SomeConstantPoly (Some (ValueOf uniPairAB p))) = do + :: SomeConstant uni (a, b) + -> EvaluationResult (SomeConstant uni (b, a)) + swapPlc (SomeConstant (Some (ValueOf uniPairAB p))) = do DefaultUniPair uniA uniB <- pure uniPairAB - pure . SomeConstantPoly $ someValueOf (DefaultUniPair uniB uniA) (snd p, fst p) + pure . SomeConstant $ someValueOf (DefaultUniPair uniB uniA) (snd p, fst p) toBuiltinMeaning SwapEls = makeBuiltinMeaning swapElsPlc mempty where -- The type reads as @[(a, Bool)] -> [(Bool, a)]@. swapElsPlc - :: a ~ Opaque term (TyVarRep ('TyNameRep "a" 0)) - => SomeConstantPoly uni [] '[SomeConstantPoly uni (,) '[a, Bool]] - -> EvaluationResult (SomeConstantPoly uni [] '[SomeConstantPoly uni (,) '[Bool, a]]) - swapElsPlc (SomeConstantPoly (Some (ValueOf uniList xs))) = do + :: SomeConstant uni [SomeConstant uni (a, Bool)] + -> EvaluationResult (SomeConstant uni [SomeConstant uni (Bool, a)]) + swapElsPlc (SomeConstant (Some (ValueOf uniList xs))) = do DefaultUniList (DefaultUniPair uniA DefaultUniBool) <- pure uniList let uniList' = DefaultUniList $ DefaultUniPair DefaultUniBool uniA - pure . SomeConstantPoly . someValueOf uniList' $ map swap xs + pure . SomeConstant . someValueOf uniList' $ map swap xs diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs index 5ee65ae353b..3e86ac947f9 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs @@ -20,13 +20,11 @@ module PlutusCore.Constant.Meaning where import PlutusPrelude -import PlutusCore.Constant.Dynamic.Emit import PlutusCore.Constant.Function import PlutusCore.Constant.Kinded import PlutusCore.Constant.Typed import PlutusCore.Core import PlutusCore.Evaluation.Machine.Exception -import PlutusCore.Evaluation.Result import PlutusCore.Name import Control.Lens (ix, (^?)) @@ -232,28 +230,78 @@ type x ~?~ y = TryUnify (x === y) x y -- | Get the element at an @i@th position in a list. type Lookup :: forall a. Nat -> [a] -> a type family Lookup n xs where + Lookup _ '[] = TypeError ('Text "Not enough elements") Lookup 0 (x ': xs) = x Lookup n (_ ': xs) = Lookup (n - 1) xs -- | Get the name at the @i@th position in the list of default names. We could use @a_0@, @a_1@, -- @a_2@ etc instead, but @a@, @b@, @c@ etc are nicer. -type GetName i = Lookup i '["a", "b", "c", "d", "e", "f", "g", "h"] +type GetName :: GHC.Type -> Nat -> Symbol +type family GetName k i where + GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"] + GetName _ i = Lookup i '["f", "g", "h", "m", "n"] -- | Try to specialize @a@ as a type representing a PLC type variable. -- @i@ is a fresh id and @j@ is a final one (either @i + 1@ or @i@ depending on whether -- specialization attempt is successful or not). -type TrySpecializeAsVar :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint -class TrySpecializeAsVar i j term a | i term a -> j +type TrySpecializeAsVar :: forall k. Nat -> Nat -> (k -> k) -> k -> GHC.Constraint +class TrySpecializeAsVar i j f a | i f a -> j instance - ( var ~ Opaque term (TyVarRep ('TyNameRep (GetName i) i)) + ( var ~ f (TyVarRep @k ('TyNameRep (GetName k i) i)) -- Try to unify @a@ with a freshly created @var@. , a ~?~ var -- If @a@ is equal to @var@ then unification was successful and we just used the fresh id and -- so we need to bump it up. Otherwise @var@ was discarded and so the fresh id is still fresh. -- Replacing @(===)@ with @(==)@ causes errors at use site, for whatever reason. , j ~ If (a === var) (i + 1) i - ) => TrySpecializeAsVar i j term a + ) => TrySpecializeAsVar i j f (a :: k) +type Id :: forall a. a -> a +data family Id x + +type HandleHole :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint +class HandleHole i j term hole | i term hole -> j +instance + ( TrySpecializeAsVar i j Id (Id x) + , HandleHoles j k term x + ) => HandleHole i k term (RepInfer x) +instance + ( TrySpecializeAsVar i j (Opaque term) a + , HandleHoles j k term a + ) => HandleHole i k term (TypeInfer a) + +type HandleHolesGo :: Nat -> Nat -> GHC.Type -> [GHC.Type] -> GHC.Constraint +class HandleHolesGo i j term holes | i term holes -> j +instance i ~ j => HandleHolesGo i j term '[] +instance + ( HandleHole i j term hole + , HandleHolesGo j k term holes + ) => HandleHolesGo i k term (hole ': holes) + +type HandleHoles :: forall a. Nat -> Nat -> GHC.Type -> a -> GHC.Constraint +type HandleHoles i j term x = HandleHolesGo i j term (ToHoles x) + +type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint +type EnumerateFromTo i j term a = HandleHole i j term (TypeInfer a) + +-- type EnumerateFromToRec :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint +-- class EnumerateFromToRec i j term a | i term a -> j +-- instance {-# OVERLAPPABLE #-} HandleHoles i j term a => EnumerateFromToRec i j term a +-- -- | TODO: First try to instantiate @a@ as a PLC type variable, then handle all the special cases. +-- instance {-# OVERLAPPING #-} +-- ( TrySpecializeAsVar i j (Opaque term) a +-- , HandleHoles j k term a +-- , EnumerateFromTo k l term b +-- ) => EnumerateFromToRec i l term (a -> b) + +-- type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint +-- class EnumerateFromTo i j term a | i term a -> j +-- instance +-- ( TrySpecializeAsVar i j (Opaque term) a +-- , HandleHoles j k term a +-- ) => EnumerateFromTo i k term a + +{- -- | For looking under special-case types, for example the type of a constant or the type arguments -- of a polymorphic built-in type get specialized as types representing PLC type variables, -- and for 'Emitter' and 'EvaluationResult' we simply recurse into the type that they receive. @@ -275,10 +323,10 @@ instance {-# OVERLAPPING #-} EnumerateFromToOne i j term a => HandleSpecialCases i j term (Emitter a) -- Note that we don't explicitly handle the no-more-arguments case as it's handled by the -- @OVERLAPPABLE@ instance above. -instance {-# OVERLAPPING #-} - ( TrySpecializeAsVar i j term (Opaque term rep) - , HandleSpecialCases j k term (SomeConstantPoly uni f reps) - ) => HandleSpecialCases i k term (SomeConstantPoly uni f (rep ': reps)) +-- instance {-# OVERLAPPING #-} +-- ( TrySpecializeAsVar i j term (Opaque term rep) +-- , HandleSpecialCases j k term (SomeConstantPoly uni f reps) +-- ) => HandleSpecialCases i k term (SomeConstantPoly uni f (rep ': reps)) -- | Instantiate an argument or result type. type EnumerateFromToOne :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint @@ -320,6 +368,7 @@ instance ( EnumerateFromToOne i j term a , EnumerateFromToRec j k term a ) => EnumerateFromTo i k term a +-} -- See Note [Automatic derivation of type schemes] -- | Construct the meaning for a built-in function by automatically deriving its diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index d83d7ccbcb1..058c4653f17 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -37,6 +37,8 @@ module PlutusCore.Constant.Typed , FromConstant (..) , HasConstant , HasConstantIn + , RepInfer + , TypeInfer , KnownBuiltinTypeAst , KnownTypeAst (..) , Merge @@ -50,7 +52,6 @@ module PlutusCore.Constant.Typed , readKnownSelf , makeKnownOrFail , SomeConstant (..) - , SomeConstantPoly (..) ) where import PlutusPrelude @@ -66,10 +67,8 @@ import PlutusCore.MkPlc hiding (error) import PlutusCore.Name import Control.Monad.Except -import Data.Functor.Const import Data.Kind qualified as GHC (Type) import Data.Proxy -import Data.SOP.Constraint import Data.Some.GADT qualified as GADT import Data.String import Data.Text (Text) @@ -457,41 +456,74 @@ type HasConstant term = (AsConstant term, FromConstant term) -- and connects @term@ and its @uni@. type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term) --- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\". --- We add such a trivial type synonym to make instances of 'KnownTypeAst' for built-in types look --- better. For example, the \"abstract\" 'KnownBuiltinTypeAst' looks sensible here: --- --- > instance KnownBuiltinTypeAst DefaultUni Integer => KnownTypeAst DefaultUni Integer --- --- while inlining the definition would give us --- --- > instance DefaultUni `Contains` Integer => KnownTypeAst DefaultUni Integer --- --- which is nonsense, because the @DefaultUni `Contains` Integer@ constraint is redundant --- (by means of being trivially satisfied). --- --- We could omit the constraint in both the cases due to `Integer` being monomorphic, but for --- polymorphic built-in types we do need it and so we keep things uniform by introducing this --- type synonym. Which also allows us to replicate the same pattern as with 'KnownTypeIn': --- --- > instance KnownBuiltinTypeIn DefaultUni term Integer => KnownTypeIn DefaultUni term Integer -type KnownBuiltinTypeAst = Contains +-- -- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\". +-- -- We add such a trivial type synonym to make instances of 'KnownTypeAst' for built-in types look +-- -- better. For example, the \"abstract\" 'KnownBuiltinTypeAst' looks sensible here: +-- -- +-- -- > instance KnownBuiltinTypeAst DefaultUni Integer => KnownTypeAst DefaultUni Integer +-- -- +-- -- while inlining the definition would give us +-- -- +-- -- > instance DefaultUni `Contains` Integer => KnownTypeAst DefaultUni Integer +-- -- +-- -- which is nonsense, because the @DefaultUni `Contains` Integer@ constraint is redundant +-- -- (by means of being trivially satisfied). +-- -- +-- -- We could omit the constraint in both the cases due to `Integer` being monomorphic, but for +-- -- polymorphic built-in types we do need it and so we keep things uniform by introducing this +-- -- type synonym. Which also allows us to replicate the same pattern as with 'KnownTypeIn': +-- -- +-- -- > instance KnownBuiltinTypeIn DefaultUni term Integer => KnownTypeIn DefaultUni term Integer +-- type KnownBuiltinTypeAst = Contains + +data RepInfer (x :: a) +data TypeInfer (a :: GHC.Type) + +-- type BuiltinToHoles :: forall k. k -> [GHC.Type] +-- type family BuiltinToHoles b where +-- BuiltinToHoles (f a) = TypeInfer a ': BuiltinToHoles f +-- BuiltinToHoles _ = '[] + +type BuiltinHead :: forall k. k -> k +data family BuiltinHead f + +type ElaborateBuiltin :: forall k. k -> k +type family ElaborateBuiltin a where + ElaborateBuiltin (f x) = ElaborateBuiltin f `TyAppRep` x + ElaborateBuiltin f = BuiltinHead f + +type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a) class KnownTypeAst uni (a :: k) where + type ToHoles a :: [GHC.Type] + type ToHoles a = ToHoles (ElaborateBuiltin a) + -- One can't directly put a PLC type variable into lists or tuples ('SomeConstantPoly' 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 _ = '[] + type ToBinds a :: [GADT.Some TyNameRep] + type ToBinds a = ToBinds (ElaborateBuiltin a) -- | The type representing @a@ used on the PLC side. toTypeAst :: proxy a -> Type TyName uni () default toTypeAst :: KnownBuiltinTypeAst uni a => proxy a -> Type TyName uni () - toTypeAst _ = mkTyBuiltin @_ @a () + toTypeAst _ = toTypeAst $ Proxy @(ElaborateBuiltin a) {-# INLINE toTypeAst #-} +instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) where + type ToHoles (a -> b) = '[TypeInfer a, TypeInfer b] + type ToBinds (a -> b) = Merge (ToBinds a) (ToBinds b) + + toTypeAst _ = TyFun () (toTypeAst $ Proxy @a) (toTypeAst $ Proxy @b) + +instance uni `Contains` f => KnownTypeAst uni (BuiltinHead f) where + type ToHoles (BuiltinHead f) = '[] + type ToBinds (BuiltinHead f) = '[] + + toTypeAst _ = mkTyBuiltin @_ @f () + -- | Delete all @x@s from a list. type family Delete x xs :: [a] where Delete _ '[] = '[] @@ -659,6 +691,7 @@ makeKnownOrFail :: (KnownType term a, MonadError err m, AsEvaluationFailure err) makeKnownOrFail = unNoCauseT . makeKnown (\_ -> pure ()) Nothing instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where + type ToHoles (EvaluationResult a) = '[ TypeInfer a ] type ToBinds (EvaluationResult a) = ToBinds a toTypeAst _ = toTypeAst $ Proxy @a @@ -680,6 +713,7 @@ instance KnownTypeIn uni term a => KnownTypeIn uni term (EvaluationResult a) whe {-# INLINE readKnown #-} instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where + type ToHoles (Emitter a) = '[ TypeInfer a ] type ToBinds (Emitter a) = ToBinds a toTypeAst _ = toTypeAst $ Proxy @a @@ -698,11 +732,12 @@ instance KnownTypeIn uni term a => KnownTypeIn uni term (Emitter a) where -- -- The @rep@ parameter specifies how the type looks on the PLC side (i.e. just like with -- @Opaque term rep@). -newtype SomeConstant uni rep = SomeConstant +newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant { unSomeConstant :: Some (ValueOf uni) } instance KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep) where + type ToHoles (SomeConstant _ rep) = '[ RepInfer rep ] type ToBinds (SomeConstant _ rep) = ToBinds rep toTypeAst _ = toTypeAst $ Proxy @rep @@ -715,34 +750,6 @@ instance HasConstantIn uni term => KnownTypeIn uni term (SomeConstant uni rep) w readKnown = coerceVia (\asC mayCause -> fmap SomeConstant . asC mayCause) asConstant {-# INLINE readKnown #-} --- | For unlifting from the 'Constant' constructor when the stored value is of a polymorphic --- built-in type. --- --- The @f@ is the built-in type and @reps@ are its arguments representing PLC types. -newtype SomeConstantPoly uni f reps = SomeConstantPoly - { unSomeConstantPoly :: Some (ValueOf uni) - } - -instance (uni `Contains` f, All (KnownTypeAst uni) reps) => - KnownTypeAst uni (SomeConstantPoly uni f reps) where - type ToBinds (SomeConstantPoly 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 ()) $ - cfoldr_SList - (Proxy @(All (KnownTypeAst uni) reps)) - (\(_ :: Proxy (rep ': _reps')) rs -> toTypeAst (Proxy @rep) : rs) - [] - {-# INLINE toTypeAst #-} - -instance HasConstantIn uni term => KnownTypeIn uni term (SomeConstantPoly uni f reps) where - makeKnown _ _ = coerceArg $ pure . fromConstant - {-# INLINE makeKnown #-} - - readKnown = coerceVia (\asC mayCause -> fmap SomeConstantPoly . asC mayCause) asConstant - {-# INLINE readKnown #-} - toTyNameAst :: forall text uniq. (KnownSymbol text, KnownNat uniq) => Proxy ('TyNameRep text uniq) -> TyName @@ -753,12 +760,14 @@ toTyNameAst _ = instance (var ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) => KnownTypeAst uni (TyVarRep var) where + type ToHoles (TyVarRep var) = '[] type ToBinds (TyVarRep var) = '[ 'GADT.Some var ] toTypeAst _ = TyVar () . toTyNameAst $ Proxy @('TyNameRep text uniq) {-# INLINE toTypeAst #-} instance (KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg) where + type ToHoles (TyAppRep fun arg) = '[ RepInfer fun, RepInfer arg ] type ToBinds (TyAppRep fun arg) = Merge (ToBinds fun) (ToBinds arg) toTypeAst _ = TyApp () (toTypeAst $ Proxy @fun) (toTypeAst $ Proxy @arg) @@ -768,6 +777,7 @@ instance ( var ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq , KnownKind kind, KnownTypeAst uni a ) => KnownTypeAst uni (TyForallRep var a) where + type ToHoles (TyForallRep var a) = '[ RepInfer a ] type ToBinds (TyForallRep var a) = Delete ('GADT.Some var) (ToBinds a) toTypeAst _ = @@ -778,6 +788,7 @@ instance {-# INLINE toTypeAst #-} instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where + type ToHoles (Opaque _ rep) = '[ RepInfer rep ] type ToBinds (Opaque _ rep) = ToBinds rep toTypeAst _ = toTypeAst $ Proxy @rep @@ -865,22 +876,3 @@ coerceVia _ = coerce coerceArg :: Coercible a b => (a -> r) -> b -> r coerceArg = coerce {-# INLINE coerceArg #-} - --- | Like 'cpara_SList' but the folding function takes a 'Proxy' argument for the convenience of --- the caller. -cparaP_SList - :: forall k c (xs :: [k]) proxy r. All c xs - => proxy c - -> r '[] - -> (forall y ys. (c y, All c ys) => Proxy (y ': ys) -> r ys -> r (y ': ys)) - -> r xs -cparaP_SList p z f = cpara_SList p z $ f Proxy - --- | A right fold over reflected lists. Like 'cparaP_SList' except not indexed. -cfoldr_SList - :: forall c xs r proxy. All c xs - => proxy (All c xs) - -> (forall y ys. (c y, All c ys) => Proxy (y ': ys) -> r -> r) - -> r - -> r -cfoldr_SList _ f z = getConst $ cparaP_SList @_ @c @xs Proxy (coerce z) (coerce . f) diff --git a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs index fb7ca5f6453..043e8157637 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Default/Builtins.hs @@ -267,8 +267,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where fstPlc (runCostingFunOneArgument . paramFstPair) where - fstPlc :: SomeConstantPoly uni (,) '[a, b] -> EvaluationResult (Opaque term a) - fstPlc (SomeConstantPoly (Some (ValueOf uniPairAB xy))) = do + fstPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque term a) + fstPlc (SomeConstant (Some (ValueOf uniPairAB xy))) = do DefaultUniPair uniA _ <- pure uniPairAB pure . fromConstant . someValueOf uniA $ fst xy {-# INLINE fstPlc #-} @@ -277,8 +277,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where sndPlc (runCostingFunOneArgument . paramSndPair) where - sndPlc :: SomeConstantPoly uni (,) '[a, b] -> EvaluationResult (Opaque term b) - sndPlc (SomeConstantPoly (Some (ValueOf uniPairAB xy))) = do + sndPlc :: SomeConstant uni (a, b) -> EvaluationResult (Opaque term b) + sndPlc (SomeConstant (Some (ValueOf uniPairAB xy))) = do DefaultUniPair _ uniB <- pure uniPairAB pure . fromConstant . someValueOf uniB $ snd xy {-# INLINE sndPlc #-} @@ -288,8 +288,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where choosePlc (runCostingFunThreeArguments . paramChooseList) where - choosePlc :: SomeConstantPoly uni [] '[a] -> b -> b -> EvaluationResult b - choosePlc (SomeConstantPoly (Some (ValueOf uniListA xs))) a b = do + choosePlc :: SomeConstant uni [a] -> b -> b -> EvaluationResult b + choosePlc (SomeConstant (Some (ValueOf uniListA xs))) a b = do DefaultUniList _ <- pure uniListA pure $ case xs of [] -> a @@ -302,11 +302,11 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where where consPlc :: SomeConstant uni a - -> SomeConstantPoly uni [] '[a] - -> EvaluationResult (Opaque term (SomeConstantPoly uni [] '[a])) + -> SomeConstant uni [a] + -> EvaluationResult (Opaque term [a]) consPlc (SomeConstant (Some (ValueOf uniA x))) - (SomeConstantPoly (Some (ValueOf uniListA xs))) = do + (SomeConstant (Some (ValueOf uniListA xs))) = do DefaultUniList uniA' <- pure uniListA -- Checking that the type of the constant is the same as the type of the elements -- of the unlifted list. Note that there's no way we could enforce this statically @@ -322,8 +322,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where headPlc (runCostingFunOneArgument . paramHeadList) where - headPlc :: SomeConstantPoly uni [] '[a] -> EvaluationResult (Opaque term a) - headPlc (SomeConstantPoly (Some (ValueOf uniListA xs))) = do + headPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque term a) + headPlc (SomeConstant (Some (ValueOf uniListA xs))) = do DefaultUniList uniA <- pure uniListA x : _ <- pure xs pure . fromConstant $ someValueOf uniA x @@ -333,10 +333,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where tailPlc (runCostingFunOneArgument . paramTailList) where - tailPlc - :: listA ~ SomeConstantPoly uni [] '[a] - => listA -> EvaluationResult (Opaque term listA) - tailPlc (SomeConstantPoly (Some (ValueOf uniListA xs))) = do + tailPlc :: SomeConstant uni [a] -> EvaluationResult (Opaque term [a]) + tailPlc (SomeConstant (Some (ValueOf uniListA xs))) = do DefaultUniList _ <- pure uniListA _ : xs' <- pure xs pure . fromConstant $ someValueOf uniListA xs' @@ -346,8 +344,8 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where nullPlc (runCostingFunOneArgument . paramNullList) where - nullPlc :: SomeConstantPoly uni [] '[a] -> EvaluationResult Bool - nullPlc (SomeConstantPoly (Some (ValueOf uniListA xs))) = do + nullPlc :: SomeConstant uni [a] -> EvaluationResult Bool + nullPlc (SomeConstant (Some (ValueOf uniListA xs))) = do DefaultUniList _ <- pure uniListA pure $ null xs {-# INLINE nullPlc #-} diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden index fe32ff4613e..5fa1482c828 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ConstrData.plc.golden @@ -1 +1 @@ -(fun (con integer) (fun (con list (data)) (con data))) \ No newline at end of file +(fun (con integer) (fun [ (con list) (con data) ] (con data))) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden index 9bf820ba54f..5b55553b890 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/IdRank2.plc.golden @@ -1 +1 @@ -(all f (fun (type) (type)) (fun (all a (type) [ f a ]) (all a (type) [ f a ]))) \ No newline at end of file +(all f (fun (type) (type)) (fun (all b (type) [ f b ]) (all b (type) [ f b ]))) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden index db1c0d46832..650a37e4f13 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/ListData.plc.golden @@ -1 +1 @@ -(fun (con list (data)) (con data)) \ No newline at end of file +(fun [ (con list) (con data) ] (con data)) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden index 4528e44fc2d..c05e012e32d 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MapData.plc.golden @@ -1 +1 @@ -(fun (con list (pair (data) (data))) (con data)) \ No newline at end of file +(fun [ (con list) [ [ (con pair) (con data) ] (con data) ] ] (con data)) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden index 5aa049e4e5d..5cdcb2c0c12 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilData.plc.golden @@ -1 +1 @@ -(fun (con unit) (con list (data))) \ No newline at end of file +(fun (con unit) [ (con list) (con data) ]) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden index 03cfed066e4..754dae6673f 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkNilPairData.plc.golden @@ -1 +1 @@ -(fun (con unit) (con list (pair (data) (data)))) \ No newline at end of file +(fun (con unit) [ (con list) [ [ (con pair) (con data) ] (con data) ] ]) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden index 95b239b007d..2c3fb473d97 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/MkPairData.plc.golden @@ -1 +1 @@ -(fun (con data) (fun (con data) (con pair (data) (data)))) \ No newline at end of file +(fun (con data) (fun (con data) [ [ (con pair) (con data) ] (con data) ])) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden index 4bc2e6fad6d..5c617498086 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnConstrData.plc.golden @@ -1 +1 @@ -(fun (con data) (con pair (integer) (list (data)))) \ No newline at end of file +(fun (con data) [ [ (con pair) (con integer) ] [ (con list) (con data) ] ]) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden index 47c39980724..5ef033d37fe 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnListData.plc.golden @@ -1 +1 @@ -(fun (con data) (con list (data))) \ No newline at end of file +(fun (con data) [ (con list) (con data) ]) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden index 9865ed48054..4a2082f4f8f 100644 --- a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnMapData.plc.golden @@ -1 +1 @@ -(fun (con data) (con list (pair (data) (data)))) \ No newline at end of file +(fun (con data) [ (con list) [ [ (con pair) (con data) ] (con data) ] ]) \ No newline at end of file diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerce.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerce.plc.golden new file mode 100644 index 00000000000..6126ad090f6 --- /dev/null +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerce.plc.golden @@ -0,0 +1 @@ +(all a (type) (all b (type) (fun a b))) \ No newline at end of file From 8fcee47b8b2dc5fd142bf505a0edcc1f5fdc0055 Mon Sep 17 00:00:00 2001 From: effectfully Date: Thu, 6 Jan 2022 16:10:55 +0300 Subject: [PATCH 06/13] Remove a now redundant dependency --- plutus-core/plutus-core.cabal | 1 - 1 file changed, 1 deletion(-) diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal index 1ed9b6e6c3c..1b2872d92a9 100644 --- a/plutus-core/plutus-core.cabal +++ b/plutus-core/plutus-core.cabal @@ -304,7 +304,6 @@ library serialise -any, size-based -any, some < 1.0.3, - sop-core -any, tasty -any, tasty-golden -any, tasty-hedgehog -any, From 7d3c855f4d2d07824f34a04cdaee8124f6ed4a83 Mon Sep 17 00:00:00 2001 From: effectfully Date: Thu, 6 Jan 2022 16:26:31 +0300 Subject: [PATCH 07/13] fix 'nix' --- nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix | 1 - nix/pkgs/haskell/materialized-darwin/default.nix | 2 -- nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix | 1 - nix/pkgs/haskell/materialized-linux/default.nix | 2 -- nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix | 1 - nix/pkgs/haskell/materialized-windows/default.nix | 2 -- 6 files changed, 9 deletions(-) diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix index 9fd9f29796e..0a709c884b3 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-core.nix @@ -86,7 +86,6 @@ (hsPkgs."serialise" or (errorHandler.buildDepError "serialise")) (hsPkgs."size-based" or (errorHandler.buildDepError "size-based")) (hsPkgs."some" or (errorHandler.buildDepError "some")) - (hsPkgs."sop-core" or (errorHandler.buildDepError "sop-core")) (hsPkgs."tasty" or (errorHandler.buildDepError "tasty")) (hsPkgs."tasty-golden" or (errorHandler.buildDepError "tasty-golden")) (hsPkgs."tasty-hedgehog" or (errorHandler.buildDepError "tasty-hedgehog")) diff --git a/nix/pkgs/haskell/materialized-darwin/default.nix b/nix/pkgs/haskell/materialized-darwin/default.nix index 0f5e07a9b6c..4306eb4ff51 100644 --- a/nix/pkgs/haskell/materialized-darwin/default.nix +++ b/nix/pkgs/haskell/materialized-darwin/default.nix @@ -184,7 +184,6 @@ "charset".revision = (((hackage."charset")."0.3.9").revisions).default; "unix".revision = (((hackage."unix")."2.7.2.2").revisions).default; "dependent-sum-template".revision = (((hackage."dependent-sum-template")."0.1.0.3").revisions).default; - "sop-core".revision = (((hackage."sop-core")."0.5.0.1").revisions).default; "data-fix".revision = (((hackage."data-fix")."0.3.2").revisions).default; "dense-linear-algebra".revision = (((hackage."dense-linear-algebra")."0.1.0.0").revisions).default; "contravariant".revision = (((hackage."contravariant")."1.5.5").revisions).default; @@ -774,7 +773,6 @@ "case-insensitive".components.library.planned = lib.mkOverride 900 true; "data-fix".components.library.planned = lib.mkOverride 900 true; "dependent-sum-template".components.library.planned = lib.mkOverride 900 true; - "sop-core".components.library.planned = lib.mkOverride 900 true; "text-short".components.library.planned = lib.mkOverride 900 true; "plutus-tx".components.library.planned = lib.mkOverride 900 true; "wcwidth".components.library.planned = lib.mkOverride 900 true; diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix index 9fd9f29796e..0a709c884b3 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-core.nix @@ -86,7 +86,6 @@ (hsPkgs."serialise" or (errorHandler.buildDepError "serialise")) (hsPkgs."size-based" or (errorHandler.buildDepError "size-based")) (hsPkgs."some" or (errorHandler.buildDepError "some")) - (hsPkgs."sop-core" or (errorHandler.buildDepError "sop-core")) (hsPkgs."tasty" or (errorHandler.buildDepError "tasty")) (hsPkgs."tasty-golden" or (errorHandler.buildDepError "tasty-golden")) (hsPkgs."tasty-hedgehog" or (errorHandler.buildDepError "tasty-hedgehog")) diff --git a/nix/pkgs/haskell/materialized-linux/default.nix b/nix/pkgs/haskell/materialized-linux/default.nix index 0f5e07a9b6c..4306eb4ff51 100644 --- a/nix/pkgs/haskell/materialized-linux/default.nix +++ b/nix/pkgs/haskell/materialized-linux/default.nix @@ -184,7 +184,6 @@ "charset".revision = (((hackage."charset")."0.3.9").revisions).default; "unix".revision = (((hackage."unix")."2.7.2.2").revisions).default; "dependent-sum-template".revision = (((hackage."dependent-sum-template")."0.1.0.3").revisions).default; - "sop-core".revision = (((hackage."sop-core")."0.5.0.1").revisions).default; "data-fix".revision = (((hackage."data-fix")."0.3.2").revisions).default; "dense-linear-algebra".revision = (((hackage."dense-linear-algebra")."0.1.0.0").revisions).default; "contravariant".revision = (((hackage."contravariant")."1.5.5").revisions).default; @@ -774,7 +773,6 @@ "case-insensitive".components.library.planned = lib.mkOverride 900 true; "data-fix".components.library.planned = lib.mkOverride 900 true; "dependent-sum-template".components.library.planned = lib.mkOverride 900 true; - "sop-core".components.library.planned = lib.mkOverride 900 true; "text-short".components.library.planned = lib.mkOverride 900 true; "plutus-tx".components.library.planned = lib.mkOverride 900 true; "wcwidth".components.library.planned = lib.mkOverride 900 true; diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix index 9fd9f29796e..0a709c884b3 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-core.nix @@ -86,7 +86,6 @@ (hsPkgs."serialise" or (errorHandler.buildDepError "serialise")) (hsPkgs."size-based" or (errorHandler.buildDepError "size-based")) (hsPkgs."some" or (errorHandler.buildDepError "some")) - (hsPkgs."sop-core" or (errorHandler.buildDepError "sop-core")) (hsPkgs."tasty" or (errorHandler.buildDepError "tasty")) (hsPkgs."tasty-golden" or (errorHandler.buildDepError "tasty-golden")) (hsPkgs."tasty-hedgehog" or (errorHandler.buildDepError "tasty-hedgehog")) diff --git a/nix/pkgs/haskell/materialized-windows/default.nix b/nix/pkgs/haskell/materialized-windows/default.nix index 7ae285ff310..9227d896e8a 100644 --- a/nix/pkgs/haskell/materialized-windows/default.nix +++ b/nix/pkgs/haskell/materialized-windows/default.nix @@ -181,7 +181,6 @@ "ieee754".revision = (((hackage."ieee754")."0.8.0").revisions).default; "charset".revision = (((hackage."charset")."0.3.9").revisions).default; "dependent-sum-template".revision = (((hackage."dependent-sum-template")."0.1.0.3").revisions).default; - "sop-core".revision = (((hackage."sop-core")."0.5.0.1").revisions).default; "data-fix".revision = (((hackage."data-fix")."0.3.2").revisions).default; "dense-linear-algebra".revision = (((hackage."dense-linear-algebra")."0.1.0.0").revisions).default; "contravariant".revision = (((hackage."contravariant")."1.5.5").revisions).default; @@ -751,7 +750,6 @@ "case-insensitive".components.library.planned = lib.mkOverride 900 true; "data-fix".components.library.planned = lib.mkOverride 900 true; "dependent-sum-template".components.library.planned = lib.mkOverride 900 true; - "sop-core".components.library.planned = lib.mkOverride 900 true; "text-short".components.library.planned = lib.mkOverride 900 true; "plutus-tx".components.library.planned = lib.mkOverride 900 true; "fail".components.library.planned = lib.mkOverride 900 true; From d0f9195bbcaf75e791483fd068ba9a1e1dfabebc Mon Sep 17 00:00:00 2001 From: effectfully Date: Thu, 6 Jan 2022 22:03:37 +0300 Subject: [PATCH 08/13] Cleaning up --- .../examples/PlutusCore/Examples/Builtins.hs | 4 +- .../src/PlutusCore/Constant/Meaning.hs | 91 +++---------------- .../src/PlutusCore/Constant/Typed.hs | 66 +++++--------- 3 files changed, 33 insertions(+), 128 deletions(-) diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs index 436c82846cb..31ac6f23970 100644 --- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs +++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs @@ -133,7 +133,7 @@ defBuiltinsRuntimeExt = toBuiltinsRuntime (defaultBuiltinCostModel, ()) data PlcListRep (a :: GHC.Type) instance KnownTypeAst uni a => KnownTypeAst uni (PlcListRep a) where - type ToHoles (PlcListRep a) = '[ RepInfer a ] + type ToHoles (PlcListRep a) = '[RepHole a] type ToBinds (PlcListRep a) = ToBinds a toTypeAst _ = TyApp () Plc.listTy . toTypeAst $ Proxy @a @@ -149,8 +149,6 @@ instance UniOf term ~ DefaultUni => KnownTypeIn DefaultUni term Void where data BuiltinErrorCall = BuiltinErrorCall deriving (Show, Eq, Exception) --- TODO: JoinOpaque - -- See Note [Representable built-in functions over polymorphic built-in types]. -- We have lists in the universe and so we can define a function like @\x -> [x, x]@ that duplicates -- the constant that it receives. Should memory consumption of that function be linear in the number diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs index 3e86ac947f9..826bc0ee9c5 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs @@ -259,16 +259,24 @@ instance type Id :: forall a. a -> a data family Id x +-- The 'Opaque' wrapper is due to 'TrySpecializeAsVar' trying to unify its last argument with +-- an 'Opaque' thing, but here we only want to instantiate the type representations. +-- | For looking under special-case types, for example the type of a constant or the type arguments +-- of a polymorphic built-in type get specialized as types representing PLC type variables, +-- and for 'Emitter' and 'EvaluationResult' we simply recurse into the type that they receive. +-- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since +-- 'HandleSpecialCases' can specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ +-- (including @0@). type HandleHole :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint class HandleHole i j term hole | i term hole -> j instance ( TrySpecializeAsVar i j Id (Id x) , HandleHoles j k term x - ) => HandleHole i k term (RepInfer x) + ) => HandleHole i k term (RepHole x) instance ( TrySpecializeAsVar i j (Opaque term) a , HandleHoles j k term a - ) => HandleHole i k term (TypeInfer a) + ) => HandleHole i k term (TypeHole a) type HandleHolesGo :: Nat -> Nat -> GHC.Type -> [GHC.Type] -> GHC.Constraint class HandleHolesGo i j term holes | i term holes -> j @@ -281,78 +289,6 @@ instance type HandleHoles :: forall a. Nat -> Nat -> GHC.Type -> a -> GHC.Constraint type HandleHoles i j term x = HandleHolesGo i j term (ToHoles x) -type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint -type EnumerateFromTo i j term a = HandleHole i j term (TypeInfer a) - --- type EnumerateFromToRec :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint --- class EnumerateFromToRec i j term a | i term a -> j --- instance {-# OVERLAPPABLE #-} HandleHoles i j term a => EnumerateFromToRec i j term a --- -- | TODO: First try to instantiate @a@ as a PLC type variable, then handle all the special cases. --- instance {-# OVERLAPPING #-} --- ( TrySpecializeAsVar i j (Opaque term) a --- , HandleHoles j k term a --- , EnumerateFromTo k l term b --- ) => EnumerateFromToRec i l term (a -> b) - --- type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint --- class EnumerateFromTo i j term a | i term a -> j --- instance --- ( TrySpecializeAsVar i j (Opaque term) a --- , HandleHoles j k term a --- ) => EnumerateFromTo i k term a - -{- --- | For looking under special-case types, for example the type of a constant or the type arguments --- of a polymorphic built-in type get specialized as types representing PLC type variables, --- and for 'Emitter' and 'EvaluationResult' we simply recurse into the type that they receive. --- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since --- 'HandleSpecialCases' can specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ --- (including @0@). -type HandleSpecialCases :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint -class HandleSpecialCases i j term a | i term a -> j -instance {-# OVERLAPPABLE #-} i ~ j => HandleSpecialCases i j term a --- The 'Opaque' wrapper is due to 'TrySpecializeAsVar' trying to unify its last argument with --- an 'Opaque' thing, but here we only want to instantiate the type representations. --- | Take an argument of a polymorphic built-in type and try to specialize it as a type representing --- a PLC type variable. -instance {-# OVERLAPPING #-} TrySpecializeAsVar i j term (Opaque term rep) => - HandleSpecialCases i j term (SomeConstant uni rep) -instance {-# OVERLAPPING #-} EnumerateFromToOne i j term a => - HandleSpecialCases i j term (EvaluationResult a) -instance {-# OVERLAPPING #-} EnumerateFromToOne i j term a => - HandleSpecialCases i j term (Emitter a) --- Note that we don't explicitly handle the no-more-arguments case as it's handled by the --- @OVERLAPPABLE@ instance above. --- instance {-# OVERLAPPING #-} --- ( TrySpecializeAsVar i j term (Opaque term rep) --- , HandleSpecialCases j k term (SomeConstantPoly uni f reps) --- ) => HandleSpecialCases i k term (SomeConstantPoly uni f (rep ': reps)) - --- | Instantiate an argument or result type. -type EnumerateFromToOne :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint -class EnumerateFromToOne i j term a | i term a -> j --- | First try to instantiate @a@ as a PLC type variable, then handle all the special cases. -instance - ( TrySpecializeAsVar i j term a - , HandleSpecialCases j k term a - ) => EnumerateFromToOne i k term a - --- See https://github.com/effectfully/sketches/tree/master/poly-type-of-saga/part2-enumerate-type-vars --- for a detailed elaboration on how this works. --- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable by --- deconstructing @a@ into an applied @(->)@ (we don't recurse to the left of @(->)@, only to the --- right) and trying to specialize every argument and result type as a PLC type variable --- (via 'TrySpecializeAsVar') until no deconstruction is possible, at which point we've got a result --- which we don't try to specialize, because it's already monomorphic due to 'EnumerateFromTo' --- trying to specialize its argument before recursing on it using this class. -type EnumerateFromToRec :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint -class EnumerateFromToRec i j term a | i term a -> j -instance {-# OVERLAPPABLE #-} i ~ j => EnumerateFromToRec i j term a -instance {-# OVERLAPPING #-} - ( EnumerateFromToOne i j term a - , EnumerateFromTo j k term b - ) => EnumerateFromToRec i k term (a -> b) - -- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable by -- first trying to specialize the whole type using 'EnumerateFromToOne' and then recursing on the -- result of that using 'EnumerateFromToRec'. The initial attempt to specialize the type allows us @@ -363,12 +299,7 @@ instance {-# OVERLAPPING #-} -- of the type and so forth until we get to the result, which is attempted to be specialized just -- like in the @undefined@ case where there are no argument types in the first place. type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint -class EnumerateFromTo i j term a | i term a -> j -instance - ( EnumerateFromToOne i j term a - , EnumerateFromToRec j k term a - ) => EnumerateFromTo i k term a --} +type EnumerateFromTo i j term a = HandleHole i j term (TypeHole a) -- See Note [Automatic derivation of type schemes] -- | Construct the meaning for a built-in function by automatically deriving its diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 058c4653f17..f02776fcd4e 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -37,8 +37,8 @@ module PlutusCore.Constant.Typed , FromConstant (..) , HasConstant , HasConstantIn - , RepInfer - , TypeInfer + , RepHole + , TypeHole , KnownBuiltinTypeAst , KnownTypeAst (..) , Merge @@ -398,13 +398,13 @@ for built-in types. data TyNameRep (kind :: GHC.Type) = TyNameRep Symbol Nat -- | Representation of an intrinsically-kinded type variable: a name. -data family TyVarRep (var :: TyNameRep kind) :: kind +data family TyVarRep (name :: TyNameRep kind) :: kind -- | Representation of an intrinsically-kinded type application: a function and an argument. data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod -- | Representation of of an intrinsically-kinded universal quantifier: a bound name and a body. -data family TyForallRep (var :: TyNameRep kind) (a :: GHC.Type) :: GHC.Type +data family TyForallRep (name :: TyNameRep kind) (a :: GHC.Type) :: GHC.Type -- | Throw an 'UnliftingError' saying that the received argument is not a constant. throwNotAConstant @@ -456,33 +456,8 @@ type HasConstant term = (AsConstant term, FromConstant term) -- and connects @term@ and its @uni@. type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term) --- -- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\". --- -- We add such a trivial type synonym to make instances of 'KnownTypeAst' for built-in types look --- -- better. For example, the \"abstract\" 'KnownBuiltinTypeAst' looks sensible here: --- -- --- -- > instance KnownBuiltinTypeAst DefaultUni Integer => KnownTypeAst DefaultUni Integer --- -- --- -- while inlining the definition would give us --- -- --- -- > instance DefaultUni `Contains` Integer => KnownTypeAst DefaultUni Integer --- -- --- -- which is nonsense, because the @DefaultUni `Contains` Integer@ constraint is redundant --- -- (by means of being trivially satisfied). --- -- --- -- We could omit the constraint in both the cases due to `Integer` being monomorphic, but for --- -- polymorphic built-in types we do need it and so we keep things uniform by introducing this --- -- type synonym. Which also allows us to replicate the same pattern as with 'KnownTypeIn': --- -- --- -- > instance KnownBuiltinTypeIn DefaultUni term Integer => KnownTypeIn DefaultUni term Integer --- type KnownBuiltinTypeAst = Contains - -data RepInfer (x :: a) -data TypeInfer (a :: GHC.Type) - --- type BuiltinToHoles :: forall k. k -> [GHC.Type] --- type family BuiltinToHoles b where --- BuiltinToHoles (f a) = TypeInfer a ': BuiltinToHoles f --- BuiltinToHoles _ = '[] +data RepHole (x :: a) +data TypeHole (a :: GHC.Type) type BuiltinHead :: forall k. k -> k data family BuiltinHead f @@ -492,6 +467,7 @@ type family ElaborateBuiltin a where ElaborateBuiltin (f x) = ElaborateBuiltin f `TyAppRep` x ElaborateBuiltin f = BuiltinHead f +-- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\". type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a) class KnownTypeAst uni (a :: k) where @@ -513,7 +489,7 @@ class KnownTypeAst uni (a :: k) where {-# INLINE toTypeAst #-} instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) where - type ToHoles (a -> b) = '[TypeInfer a, TypeInfer b] + type ToHoles (a -> b) = '[TypeHole a, TypeHole b] type ToBinds (a -> b) = Merge (ToBinds a) (ToBinds b) toTypeAst _ = TyFun () (toTypeAst $ Proxy @a) (toTypeAst $ Proxy @b) @@ -691,7 +667,7 @@ makeKnownOrFail :: (KnownType term a, MonadError err m, AsEvaluationFailure err) makeKnownOrFail = unNoCauseT . makeKnown (\_ -> pure ()) Nothing instance KnownTypeAst uni a => KnownTypeAst uni (EvaluationResult a) where - type ToHoles (EvaluationResult a) = '[ TypeInfer a ] + type ToHoles (EvaluationResult a) = '[TypeHole a] type ToBinds (EvaluationResult a) = ToBinds a toTypeAst _ = toTypeAst $ Proxy @a @@ -713,7 +689,7 @@ instance KnownTypeIn uni term a => KnownTypeIn uni term (EvaluationResult a) whe {-# INLINE readKnown #-} instance KnownTypeAst uni a => KnownTypeAst uni (Emitter a) where - type ToHoles (Emitter a) = '[ TypeInfer a ] + type ToHoles (Emitter a) = '[TypeHole a] type ToBinds (Emitter a) = ToBinds a toTypeAst _ = toTypeAst $ Proxy @a @@ -737,7 +713,7 @@ newtype SomeConstant uni (rep :: GHC.Type) = SomeConstant } instance KnownTypeAst uni rep => KnownTypeAst uni (SomeConstant uni rep) where - type ToHoles (SomeConstant _ rep) = '[ RepInfer rep ] + type ToHoles (SomeConstant _ rep) = '[RepHole rep] type ToBinds (SomeConstant _ rep) = ToBinds rep toTypeAst _ = toTypeAst $ Proxy @rep @@ -758,27 +734,27 @@ toTyNameAst _ = (Text.pack $ symbolVal @text Proxy) (Unique . fromIntegral $ natVal @uniq Proxy) -instance (var ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) => - KnownTypeAst uni (TyVarRep var) where - type ToHoles (TyVarRep var) = '[] - type ToBinds (TyVarRep var) = '[ 'GADT.Some var ] +instance (name ~ 'TyNameRep text uniq, KnownSymbol text, KnownNat uniq) => + KnownTypeAst uni (TyVarRep name) where + type ToHoles (TyVarRep name) = '[] + type ToBinds (TyVarRep name) = '[ 'GADT.Some name ] toTypeAst _ = TyVar () . toTyNameAst $ Proxy @('TyNameRep text uniq) {-# INLINE toTypeAst #-} instance (KnownTypeAst uni fun, KnownTypeAst uni arg) => KnownTypeAst uni (TyAppRep fun arg) where - type ToHoles (TyAppRep fun arg) = '[ RepInfer fun, RepInfer arg ] + type ToHoles (TyAppRep fun arg) = '[RepHole fun, RepHole arg] type ToBinds (TyAppRep fun arg) = Merge (ToBinds fun) (ToBinds arg) toTypeAst _ = TyApp () (toTypeAst $ Proxy @fun) (toTypeAst $ Proxy @arg) {-# INLINE toTypeAst #-} instance - ( var ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq + ( name ~ 'TyNameRep @kind text uniq, KnownSymbol text, KnownNat uniq , KnownKind kind, KnownTypeAst uni a - ) => KnownTypeAst uni (TyForallRep var a) where - type ToHoles (TyForallRep var a) = '[ RepInfer a ] - type ToBinds (TyForallRep var a) = Delete ('GADT.Some var) (ToBinds a) + ) => KnownTypeAst uni (TyForallRep name a) where + type ToHoles (TyForallRep name a) = '[RepHole a] + type ToBinds (TyForallRep name a) = Delete ('GADT.Some name) (ToBinds a) toTypeAst _ = TyForall () @@ -788,7 +764,7 @@ instance {-# INLINE toTypeAst #-} instance KnownTypeAst uni rep => KnownTypeAst uni (Opaque term rep) where - type ToHoles (Opaque _ rep) = '[ RepInfer rep ] + type ToHoles (Opaque _ rep) = '[RepHole rep] type ToBinds (Opaque _ rep) = ToBinds rep toTypeAst _ = toTypeAst $ Proxy @rep From 4ba7a721f79dfa36c459e7209ac14fc16427efb0 Mon Sep 17 00:00:00 2001 From: effectfully Date: Fri, 7 Jan 2022 20:32:02 +0300 Subject: [PATCH 09/13] Add some docs --- .../examples/PlutusCore/Examples/Builtins.hs | 13 ++ .../src/PlutusCore/Constant/Meaning.hs | 4 +- .../src/PlutusCore/Constant/Typed.hs | 128 ++++++++++++++++-- 3 files changed, 134 insertions(+), 11 deletions(-) diff --git a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs index 31ac6f23970..89e2d592942 100644 --- a/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs +++ b/plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs @@ -103,6 +103,7 @@ data ExtensionFun | FailingPlus | ExpensivePlus | UnsafeCoerce + | UnsafeCoerceEl | Undefined | Absurd | ErrorPrime -- Like 'Error', but a builtin. What do we even need 'Error' for at this point? @@ -225,6 +226,18 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni ExtensionFun where (Opaque . unOpaque) (\_ _ -> ExBudget 1 0) + toBuiltinMeaning UnsafeCoerceEl = + makeBuiltinMeaning + unsafeCoerceElPlc + (\_ _ -> ExBudget 1 0) + where + unsafeCoerceElPlc + :: SomeConstant DefaultUni [a] + -> EvaluationResult (SomeConstant DefaultUni [b]) + unsafeCoerceElPlc (SomeConstant (Some (ValueOf uniList xs))) = do + DefaultUniList _ <- pure uniList + pure . SomeConstant $ someValueOf uniList xs + toBuiltinMeaning Undefined = makeBuiltinMeaning undefined diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs index 826bc0ee9c5..c674e47898c 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs @@ -267,7 +267,7 @@ data family Id x -- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since -- 'HandleSpecialCases' can specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ -- (including @0@). -type HandleHole :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint +type HandleHole :: Nat -> Nat -> GHC.Type -> Hole -> GHC.Constraint class HandleHole i j term hole | i term hole -> j instance ( TrySpecializeAsVar i j Id (Id x) @@ -278,7 +278,7 @@ instance , HandleHoles j k term a ) => HandleHole i k term (TypeHole a) -type HandleHolesGo :: Nat -> Nat -> GHC.Type -> [GHC.Type] -> GHC.Constraint +type HandleHolesGo :: Nat -> Nat -> GHC.Type -> [Hole] -> GHC.Constraint class HandleHolesGo i j term holes | i term holes -> j instance i ~ j => HandleHolesGo i j term '[] instance diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index f02776fcd4e..c03d3a6daa5 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -37,6 +37,7 @@ module PlutusCore.Constant.Typed , FromConstant (..) , HasConstant , HasConstantIn + , Hole , RepHole , TypeHole , KnownBuiltinTypeAst @@ -67,7 +68,7 @@ import PlutusCore.MkPlc hiding (error) import PlutusCore.Name import Control.Monad.Except -import Data.Kind qualified as GHC (Type) +import Data.Kind qualified as GHC (Constraint, Type) import Data.Proxy import Data.Some.GADT qualified as GADT import Data.String @@ -456,12 +457,117 @@ type HasConstant term = (AsConstant term, FromConstant term) -- and connects @term@ and its @uni@. type HasConstantIn uni term = (UniOf term ~ uni, HasConstant term) -data RepHole (x :: a) -data TypeHole (a :: GHC.Type) +{- Note [Rep vs Type context] +Say you define an @Id@ built-in function and specify its Haskell type signature: + id :: forall a. a -> a + +This gets picked up by the 'TypeScheme' inference machinery, which detects @a@ and instantiates it +to @Opaque term Var0@ where @Var0@ is some concrete type (the exact details don't matter here) +representing a Plutus type variable of kind @*@ with the @0@ unique, so @id@ elaborates to + + id :: Opaque term Var0 -> Opaque term Var0 + +But consider also the case where you want to define @id@ only over lists. The signature of the +built-in function then is + + idList :: forall a. Opaque term [a] -> Opaque term [a] + +Now the 'Opaque' is explicit and the 'TypeScheme' inference machinery needs to go under it in order +to instantiate @a@. Which now does not get instantiated to an 'Opaque' as before, since we're +already inside an 'Opaque' and can just use @Var0@ directly. So @idList@ elaborates to + + idList :: Opaque term [Var0] -> Opaque term [Var0] + +Now let's make up some syntax for annotating contexts so that it's clear what's going on: + + idList @Type | + :: (@Type | Opaque term (@Rep | [Var0])) + -> (@Type | Opaque term (@Rep | [Var0])) + +'@ann |' annotates everything to the right of it. The whole thing then reads as + +1. a builtin is always defined in the Type context +2. @->@ preserves the Type context, i.e. it accepts it and passes it down to the domain and codomain +3. @Opaque term@ switches the context from Type to Rep, i.e. it accepts the Type context, but +creates the Rep context for its argument that represents a Plutus type + +So why the distinction? + +The difference between the Rep and the Type contexts that we've seen so far is that in the Rep +context we don't need any @Opaque@, but this is a very superficial reason to keep the distinction +between contexts, since everything that is legal in the Type context is legal in the Rep context +as well. For example we could've elaborated @idList@ into a bit more verbose + + idList :: Opaque term [Opaque term Var0] -> Opaque term [Opaque term Var0] + +and the world wouldn't end because of that, everything would work correctly. + +The opposite however is not true: certain types that are legal in the Rep context are not legal in +the Type one and this is the reason why the distinction exists. The simplest example is + + id :: Var0 -> Var0 + +@Var0@ represents a Plutus type variable and it's a data family with no inhabitants, so it does not +make sense to try to unlift a value of that type. + +Now let's say we added a @term@ argument to @Var0@ and said that when @Var0 term@ is a @GHC.Type@, +it has a @term@ inside, just like 'Opaque'. Then we would be able to unlift it, but we also have +things like @TyAppRep@, @TyForallRep@ and that set is open, any Plutus type can be represented +using such combinators and we can even name particular types, e.g. we could have @PlcListRep@, +so we'd have to special-case @GHC.Type@ for each of them and it would be a huge mess. + +So instead of mixing up types whose values are actually unliftable with types that are only used +for type checking, we keep the distinction explicit. + +The barrier between Haskell and Plutus is the barrier between the Type and the Rep contexts and +that barrier must always be some explicit type constructor that switches the context from Type to +Rep. We've only considered 'Opaque' as an example of such type constructor, but we also have +'SomeConstant' as another example. + +Some type constructors turn any context into the Type one, for example 'EvaluationResult' and +'Emitter', although they are useless inside the Rep context, given that it's only for type checking +Plutus and they don't exist in the type language of Plutus. + +These @*Rep@ data families like 'TyVarRep', 'TyAppRep' etc all require the Rep context and preserve +it, since they're only for representing Plutus types for type checking purposes. + +We call a thing in a Rep or 'Type' context a 'RepHole' or 'TypeHole' respectively. The reason for +the name is that the inference machinery looks at the thing and tries to instantiate it, like fill +a hole. + +For the user defining a builtin this all is pretty much invisible. +-} + +-- See Note [Rep vs Type context]. +-- | The kind of holes. +data Hole + +-- See Note [Rep vs Type context]. +-- | A hole in the Rep context. +type RepHole :: forall a hole. a -> hole +data family RepHole x + +-- See Note [Rep vs Type context]. +-- | A hole in the Type context. +type TypeHole :: forall hole. GHC.Type -> hole +data family TypeHole a + +-- | For annotating an uninstantiated built-in type, so that it gets handled by the right instance +-- or type family. type BuiltinHead :: forall k. k -> k data family BuiltinHead f +-- | Take an iterated application of a built-in type and elaborate every function application +-- inside of it to 'TypeAppRep', plus annotate the head with 'BuiltinHead'. +-- The idea is that we don't need to process built-in types manually if we simply add some +-- annotations for instance resolution to look for. Think what we'd have to do manually for, say, +-- 'ToHoles': traverse the spine of the application and collect all the holes into a list, which is +-- troubling, because type applications are left-nested and lists are right-nested, so we'd have to +-- use accumulators or an explicit 'Reverse' type family. And then we also have 'KnownTypeAst' and +-- 'ToBinds', so handling built-in types in a special way for each of those would be a hassle, +-- especially given the fact that type-level Haskell is not exactly good at computing things. +-- With the 'ElaborateBuiltin' approach we get 'KnownTypeAst', 'ToHoles' and 'ToBinds' for free. type ElaborateBuiltin :: forall k. k -> k type family ElaborateBuiltin a where ElaborateBuiltin (f x) = ElaborateBuiltin f `TyAppRep` x @@ -470,13 +576,14 @@ type family ElaborateBuiltin a where -- | A constraint for \"@a@ is a 'KnownTypeAst' by means of being included in @uni@\". type KnownBuiltinTypeAst uni a = KnownTypeAst uni (ElaborateBuiltin a) -class KnownTypeAst uni (a :: k) where - type ToHoles a :: [GHC.Type] +type KnownTypeAst :: forall k. (GHC.Type -> GHC.Type) -> k -> GHC.Constraint +class KnownTypeAst uni a where + -- | Return every part of the type that can be a to-be-instantiated type variable. + -- For example, in @Integer@ there's no such types and in @(a, b)@ it's the two arguments + -- (@a@ and @b@) and the same applies to @a -> b@ (to mention a type that is not built-in). + type ToHoles a :: [Hole] type ToHoles a = ToHoles (ElaborateBuiltin a) - -- One can't directly put a PLC type variable into lists or tuples ('SomeConstantPoly' 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 :: [GADT.Some TyNameRep] @@ -493,12 +600,14 @@ instance (KnownTypeAst uni a, KnownTypeAst uni b) => KnownTypeAst uni (a -> b) w type ToBinds (a -> b) = Merge (ToBinds a) (ToBinds b) toTypeAst _ = TyFun () (toTypeAst $ Proxy @a) (toTypeAst $ Proxy @b) + {-# INLINE toTypeAst #-} instance uni `Contains` f => KnownTypeAst uni (BuiltinHead f) where type ToHoles (BuiltinHead f) = '[] type ToBinds (BuiltinHead f) = '[] toTypeAst _ = mkTyBuiltin @_ @f () + {-# INLINE toTypeAst #-} -- | Delete all @x@s from a list. type family Delete x xs :: [a] where @@ -518,7 +627,8 @@ type family Merge xs ys :: [a] where -- @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 ListToBinds :: forall a. [a] -> [GADT.Some TyNameRep] +type family ListToBinds xs type instance ListToBinds '[] = '[] type instance ListToBinds (x ': xs) = Merge (ToBinds x) (ListToBinds xs) From f7bd7ddeb3e1af7a58263ecdbab85142bd44afb0 Mon Sep 17 00:00:00 2001 From: effectfully Date: Fri, 7 Jan 2022 22:32:44 +0300 Subject: [PATCH 10/13] More docs --- .../src/PlutusCore/Constant/Debug.hs | 16 +++--- .../src/PlutusCore/Constant/Meaning.hs | 55 ++++++++----------- .../src/PlutusCore/Constant/Typed.hs | 7 +++ .../Golden/UnsafeCoerceEl.plc.golden | 1 + 4 files changed, 38 insertions(+), 41 deletions(-) create mode 100644 plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerceEl.plc.golden diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs index f85877e43b9..08ddc7e59ce 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs @@ -22,8 +22,6 @@ type TermDebug = Term TyName Name DefaultUni DefaultFun () -- -- >>> :t enumerateDebug False -- enumerateDebug False :: Bool --- >>> :t enumerateDebug $ Just 'a' --- enumerateDebug $ Just 'a' :: Maybe Char -- >>> :t enumerateDebug $ \_ -> () -- enumerateDebug $ \_ -> () -- :: Opaque @@ -31,12 +29,12 @@ type TermDebug = Term TyName Name DefaultUni DefaultFun () -- (TyVarRep ('TyNameRep "a" 0)) -- -> () -- >>> :t enumerateDebug 42 --- :1:16-17: error: +-- :1:16: error: -- • Built-in functions are not allowed to have constraints -- To fix this error instantiate all constrained type variables -- • In the first argument of ‘enumerateDebug’, namely ‘42’ -- In the expression: enumerateDebug 42 -enumerateDebug :: forall a j. EnumerateFromTo 0 j TermDebug a => a -> a +enumerateDebug :: forall a j. SpecializeFromTo 0 j TermDebug a => a -> a enumerateDebug = id -- | Instantiate type variables in the type of a value using 'EnumerateFromTo' and check that it's @@ -45,9 +43,10 @@ enumerateDebug = id -- >>> :t inferDebug False -- inferDebug False :: Bool -- >>> :t inferDebug $ Just 'a' --- :1:1-21: error: --- • There's no 'KnownType' instance for Maybe Char --- Did you add a new built-in type and forget to provide a 'KnownType' instance for it? +-- :1:1: error: +-- • No instance for (KnownPolytype +-- (ToBinds (Maybe Char)) TermDebug '[] (Maybe Char) (Maybe Char)) +-- arising from a use of ‘inferDebug’ -- • In the expression: inferDebug $ Just 'a' -- >>> :t inferDebug $ \_ -> () -- inferDebug $ \_ -> () @@ -58,8 +57,7 @@ enumerateDebug = id inferDebug :: forall a binds args res j. ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ Merge (ListToBinds args) (ToBinds res) - , KnownPolytype binds TermDebug args res a, EnumerateFromTo 0 j TermDebug a - , KnownMonotype TermDebug args res a + , KnownPolytype binds TermDebug args res a, SpecializeFromTo 0 j TermDebug a ) => a -> a inferDebug = id diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs index c674e47898c..52b133a527a 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs @@ -238,12 +238,17 @@ type family Lookup n xs where -- @a_2@ etc instead, but @a@, @b@, @c@ etc are nicer. type GetName :: GHC.Type -> Nat -> Symbol type family GetName k i where - GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"] - GetName _ i = Lookup i '["f", "g", "h", "m", "n"] + GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"] + GetName _ i = Lookup i '["f", "g", "h", "m", "n"] + +-- | Like 'id', but a type constructor. +type Id :: forall a. a -> a +data family Id x -- | Try to specialize @a@ as a type representing a PLC type variable. -- @i@ is a fresh id and @j@ is a final one (either @i + 1@ or @i@ depending on whether -- specialization attempt is successful or not). +-- @f@ is for wrapping 'TyVarRep' (see 'HandleHole' for how this is used). type TrySpecializeAsVar :: forall k. Nat -> Nat -> (k -> k) -> k -> GHC.Constraint class TrySpecializeAsVar i j f a | i f a -> j instance @@ -256,28 +261,25 @@ instance , j ~ If (a === var) (i + 1) i ) => TrySpecializeAsVar i j f (a :: k) -type Id :: forall a. a -> a -data family Id x - --- The 'Opaque' wrapper is due to 'TrySpecializeAsVar' trying to unify its last argument with --- an 'Opaque' thing, but here we only want to instantiate the type representations. --- | For looking under special-case types, for example the type of a constant or the type arguments --- of a polymorphic built-in type get specialized as types representing PLC type variables, --- and for 'Emitter' and 'EvaluationResult' we simply recurse into the type that they receive. --- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since --- 'HandleSpecialCases' can specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ --- (including @0@). +-- | First try to specialize the hole using 'TrySpecializeAsVar' and then recurse on the result of +-- that using 'HandleHoles'. +-- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since 'HandleHole' can +-- specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ (including @0@). type HandleHole :: Nat -> Nat -> GHC.Type -> Hole -> GHC.Constraint class HandleHole i j term hole | i term hole -> j +-- In the Rep context @x@ is attempted to be instantiated as a 'TyVarRep'. instance - ( TrySpecializeAsVar i j Id (Id x) + ( TrySpecializeAsVar i j Id (Id x) -- The two 'Id's cancel each other. , HandleHoles j k term x ) => HandleHole i k term (RepHole x) +-- In the Type context @a@ is attempted to be instantiated as a 'TyVarRep' wrapped in @Opaque term@. instance ( TrySpecializeAsVar i j (Opaque term) a , HandleHoles j k term a ) => HandleHole i k term (TypeHole a) +-- | Call 'HandleHole' over each hole from the list, threading the state (the fresh unique) through +-- the calls. type HandleHolesGo :: Nat -> Nat -> GHC.Type -> [Hole] -> GHC.Constraint class HandleHolesGo i j term holes | i term holes -> j instance i ~ j => HandleHolesGo i j term '[] @@ -286,20 +288,15 @@ instance , HandleHolesGo j k term holes ) => HandleHolesGo i k term (hole ': holes) +-- | Get the holes of @x@ and recurse into them. type HandleHoles :: forall a. Nat -> Nat -> GHC.Type -> a -> GHC.Constraint type HandleHoles i j term x = HandleHolesGo i j term (ToHoles x) --- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable by --- first trying to specialize the whole type using 'EnumerateFromToOne' and then recursing on the --- result of that using 'EnumerateFromToRec'. The initial attempt to specialize the type allows us --- to handle the case where the whole type is just a single type variable (such as @undefined :: a@) --- and it also allows us to look into the result type due to 'EnumerateFromToRec' mutually --- recursively calling 'EnumerateFromTo'. I.e. the initial attempt at specialization allows --- 'EnumerateFromToRec' to cut one argument off the type and call 'EnumerateFromTo' over the rest --- of the type and so forth until we get to the result, which is attempted to be specialized just --- like in the @undefined@ case where there are no argument types in the first place. -type EnumerateFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint -type EnumerateFromTo i j term a = HandleHole i j term (TypeHole a) +-- | Specialize each Haskell type variable in @a@ as a type representing a PLC type variable. +-- @i@ is a fresh id and @j@ is a final one as in 'TrySpecializeAsVar', but since 'HandleHole' can +-- specialize multiple variables, @j@ can be equal to @i + n@ for any @n@ (including @0@). +type SpecializeFromTo :: Nat -> Nat -> GHC.Type -> GHC.Type -> GHC.Constraint +type SpecializeFromTo i j term a = HandleHole i j term (TypeHole a) -- See Note [Automatic derivation of type schemes] -- | Construct the meaning for a built-in function by automatically deriving its @@ -310,13 +307,7 @@ type EnumerateFromTo i j term a = HandleHole i j term (TypeHole a) makeBuiltinMeaning :: forall a term cost binds args res j. ( args ~ GetArgs a, a ~ FoldArgs args res, binds ~ Merge (ListToBinds args) (ToBinds res) - , KnownPolytype binds term args res a, EnumerateFromTo 0 j term a - -- This constraint is just to get through 'KnownPolytype' stuck on an unknown type straight - -- to the custom type error that we have in the @Typed@ module. Though, somehow, the error - -- gets triggered even without the constraint when this function in used, but I don't - -- understand how that is possible and it does not work when the function from the @Debug@ - -- module is used. So we're just doing the right thing here and adding the constraint. - , KnownMonotype term args res a + , KnownPolytype binds term args res a, SpecializeFromTo 0 j term a ) => a -> (cost -> FoldArgsEx args) -> BuiltinMeaning term cost makeBuiltinMeaning = BuiltinMeaning (knownPolytype (Proxy @binds) :: TypeScheme term args res) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index c03d3a6daa5..db2a56e03ef 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -536,6 +536,13 @@ We call a thing in a Rep or 'Type' context a 'RepHole' or 'TypeHole' respectivel the name is that the inference machinery looks at the thing and tries to instantiate it, like fill a hole. +We could also have a third type of hole/context, Name, because binders bind names rather than +variables and so it makes sense to infer names sometimes, like for 'TyForallRep' for example. +We don't do that currently, because we don't have such builtins anyway. + +And there could be even fancier kinds of holes like "infer anything" for cases where the hole +is determined by some other part of the signature. We don't have that either, for the same reason. + For the user defining a builtin this all is pretty much invisible. -} diff --git a/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerceEl.plc.golden b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerceEl.plc.golden new file mode 100644 index 00000000000..ef3a9750e3d --- /dev/null +++ b/plutus-core/plutus-core/test/TypeSynthesis/Golden/UnsafeCoerceEl.plc.golden @@ -0,0 +1 @@ +(all a (type) (all b (type) (fun [ (con list) a ] [ (con list) b ]))) \ No newline at end of file From 0b360ad5283caf09271f74367f3863b408f88805 Mon Sep 17 00:00:00 2001 From: effectfully Date: Fri, 7 Jan 2022 22:56:28 +0300 Subject: [PATCH 11/13] A bit more docs --- plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index db2a56e03ef..00af59534cd 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -703,7 +703,7 @@ readKnownConstant mayCause term = asConstant mayCause term >>= oneShot \case -- 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 a@ (and for brevity). +-- 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 @@ -711,6 +711,11 @@ readKnownConstant mayCause term = asConstant mayCause term >>= oneShot \case -- 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 term => KnownTypeIn uni term a where -- | Convert a Haskell value to the corresponding PLC term. -- The inverse of 'readKnown'. From f10c8487fe7e9a57013b6d0418fde67e1e7daf2b Mon Sep 17 00:00:00 2001 From: effectfully Date: Tue, 11 Jan 2022 00:36:31 +0300 Subject: [PATCH 12/13] Note [Unlifting values of built-in types] --- .../src/PlutusCore/Constant/Debug.hs | 4 +- .../src/PlutusCore/Constant/Meaning.hs | 2 +- .../src/PlutusCore/Constant/Typed.hs | 60 +++++++++++++++++++ 3 files changed, 63 insertions(+), 3 deletions(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs index 08ddc7e59ce..bec58ea988b 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Debug.hs @@ -34,8 +34,8 @@ type TermDebug = Term TyName Name DefaultUni DefaultFun () -- To fix this error instantiate all constrained type variables -- • In the first argument of ‘enumerateDebug’, namely ‘42’ -- In the expression: enumerateDebug 42 -enumerateDebug :: forall a j. SpecializeFromTo 0 j TermDebug a => a -> a -enumerateDebug = id +specializeDebug :: forall a j. SpecializeFromTo 0 j TermDebug a => a -> a +specializeDebug = id -- | Instantiate type variables in the type of a value using 'EnumerateFromTo' and check that it's -- possible to construct a 'TypeScheme' out of the resulting type. Example usages: diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs index 52b133a527a..21b3aacc081 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs @@ -239,7 +239,7 @@ type family Lookup n xs where type GetName :: GHC.Type -> Nat -> Symbol type family GetName k i where GetName GHC.Type i = Lookup i '["a", "b", "c", "d", "e", "i", "j", "k", "l"] - GetName _ i = Lookup i '["f", "g", "h", "m", "n"] + GetName _ i = Lookup i '["f", "g", "h", "m", "n"] -- For higher-kinded types. -- | Like 'id', but a type constructor. type Id :: forall a. a -> a diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 00af59534cd..483d5687bbb 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -682,6 +682,66 @@ builtins this is rarely the case as most of the time we want aggressive inlining and the "just compute the damn thing" behavior. -} +{- Note [Unlifting values of built-in types] +It's trivial to unlift from a term a value of a monomorphic type like 'Integer': just check that +the term is a constant, extract the type tag and check it for equality with the type tag of +'Integer'. + +Things work the same way for a fully monomorphized polymorphic type, i.e. @(Integer, Bool@) is not +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 term 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 +need to write a function from a @[a]@ for some arbitrary built-in @a@ to @[Opaque term 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 +perfectly linear algorithms quadratic. See https://github.com/input-output-hk/plutus/pull/4215 for +how that would look like. + +So the problem is that we can't convert in O(1) time a @[a]@ coming from a constant of +statically-unknown type (that @a@ is existential) to @[a']@ where @a'@ is known statically. +Thus it's impossible to instantiate @a@ in Haskell's + + nullList :: [a] -> Bool + +so that there's a 'TypeScheme' for this function. + +One non-solution would be to instantiate @a@, then recurse on the type, construct a new function +that defers to the original @nullList@ but wraps its argument in a specific way (more on that below) +making it possible to assign a 'TypeScheme' to the resulting function. Astonishingly enough, that +could actually work and if we ever write a paper on builtins, we should mention that example, but: + +1. such a trick requires a generic machinery that knows how to check that the head of the builtin + application is a particular built-in type. We used to have that, but it was just way too slow +2. that would only work for functions that don't care about @a@ at all. But for example when + elaborating @cons :: a -> [a] -> [a]@ as a Plutus builtin we need to unlift both the arguments + and check that their @a@s are equal + (See Note [Representable built-in functions over polymorphic built-in types]) + and it either way too complex or even impossible to do that automatically within some generic + machinery + +So what we do is we simply require the user to write + + nullList :: Opaque term [a] -> Bool + +and unlift a @[a]@ manually within the definition of the builtin. This works, because the +existential @a@ never escapes the definition of the builtin. I.e. it's fine to unpack an existential +and use it immediately without ever exposing the existential parts to the outside and it's not fine +to try to return a value having an existential inside of it, which is what unlifting of @[a]@ would +amount to. + +Could we somehow align the unlifting machinery so that it does not construct values of particular +types, but rather feeds them to a continuation or something, so that the existential parts never +try to escape? Maybe, but see point 2 from the above, we do want to get our hands on the particular +universes sometimes and point 1 prevents us from doing that generically, so it doesn't seem like +we could do that within some automated machinery. + +Overall, asking the user to manually unlift from @Opaque term [a]@ is just always going to be +faster than any kind of fancy encoding. +-} + +-- See Note [Unlifting values of built-in types]. -- | Convert a constant embedded into a PLC term to the corresponding Haskell value. readKnownConstant :: forall term a err cause. (AsUnliftingError err, KnownBuiltinType term a) From f6426c19c2f5b8f4f24a3ff97d8ac11ff4355b8a Mon Sep 17 00:00:00 2001 From: effectfully Date: Tue, 11 Jan 2022 00:43:14 +0300 Subject: [PATCH 13/13] Proofreading --- plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs index 483d5687bbb..6167cf48141 100644 --- a/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs +++ b/plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs @@ -718,7 +718,7 @@ could actually work and if we ever write a paper on builtins, we should mention elaborating @cons :: a -> [a] -> [a]@ as a Plutus builtin we need to unlift both the arguments and check that their @a@s are equal (See Note [Representable built-in functions over polymorphic built-in types]) - and it either way too complex or even impossible to do that automatically within some generic + and it's either way too complex or even impossible to do that automatically within some generic machinery So what we do is we simply require the user to write