-- | This module assigns types to built-ins. -- See the @plutus/plutus-core/docs/Constant application.md@ -- article for how this emerged. {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE StrictData #-} module PlutusCore.Builtin.TypeScheme ( TypeScheme (..) , argProxy , FoldArgs , FoldArgsEx , typeSchemeToType ) where import PlutusCore.Builtin.KnownKind import PlutusCore.Builtin.KnownType import PlutusCore.Builtin.KnownTypeAst import PlutusCore.Core import PlutusCore.Evaluation.Machine.ExBudget import PlutusCore.Evaluation.Machine.ExMemory import PlutusCore.Name import Data.Kind qualified as GHC (Type) import Data.Proxy import Data.Text qualified as Text import GHC.TypeLits infixr 9 `TypeSchemeArrow` -- | Type schemes of primitive operations. -- @as@ is a list of types of arguments, @r@ is the resulting type. -- E.g. @Text -> Bool -> Integer@ is encoded as @TypeScheme val [Text, Bool] Integer@. data TypeScheme val (args :: [GHC.Type]) res where TypeSchemeResult :: KnownType val res => TypeScheme val '[] res TypeSchemeArrow :: KnownType val arg => TypeScheme val args res -> TypeScheme val (arg ': args) res TypeSchemeAll :: (KnownSymbol text, KnownNat uniq, KnownKind kind) -- Here we require the user to manually provide the unique of a type variable. -- That's nothing but silly, but I do not see what else we can do with the current design. => Proxy '(text, uniq, kind) -> TypeScheme val args res -> TypeScheme val args res argProxy :: TypeScheme val (arg ': args) res -> Proxy arg argProxy :: TypeScheme val (arg : args) res -> Proxy arg argProxy TypeScheme val (arg : args) res _ = Proxy arg forall k (t :: k). Proxy t Proxy -- | Turn a list of Haskell types @args@ into a functional type ending in @res@. -- -- >>> :set -XDataKinds -- >>> :kind! FoldArgs [Text, Bool] Integer -- FoldArgs [Text, Bool] Integer :: * -- = Text -> Bool -> Integer type family FoldArgs args res where FoldArgs '[] res = res FoldArgs (arg ': args) res = arg -> FoldArgs args res -- | Calculates the parameters of the costing function for a builtin. type family FoldArgsEx args where FoldArgsEx '[] = ExBudget FoldArgsEx (arg ': args) = ExMemory -> FoldArgsEx args -- | Convert a 'TypeScheme' to the corresponding 'Type'. -- Basically, a map from the PHOAS representation to the FOAS one. typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) () typeSchemeToType :: TypeScheme val args res -> Type TyName (UniOf val) () typeSchemeToType sch :: TypeScheme val args res sch@TypeScheme val args res TypeSchemeResult = TypeScheme val args res -> Type TyName (UniOf val) () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst TypeScheme val args res sch typeSchemeToType sch :: TypeScheme val args res sch@(TypeSchemeArrow TypeScheme val args res schB) = () -> Type TyName (UniOf val) () -> Type TyName (UniOf val) () -> Type TyName (UniOf val) () forall tyname (uni :: * -> *) ann. ann -> Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann TyFun () (Proxy arg -> Type TyName (UniOf val) () forall a (uni :: * -> *) (x :: a) (proxy :: a -> *). KnownTypeAst uni x => proxy x -> Type TyName uni () toTypeAst (Proxy arg -> Type TyName (UniOf val) ()) -> Proxy arg -> Type TyName (UniOf val) () forall a b. (a -> b) -> a -> b $ TypeScheme val (arg : args) res -> Proxy arg forall val arg (args :: [*]) res. TypeScheme val (arg : args) res -> Proxy arg argProxy TypeScheme val args res TypeScheme val (arg : args) res sch) (Type TyName (UniOf val) () -> Type TyName (UniOf val) ()) -> Type TyName (UniOf val) () -> Type TyName (UniOf val) () forall a b. (a -> b) -> a -> b $ TypeScheme val args res -> Type TyName (UniOf val) () forall val (args :: [*]) res. TypeScheme val args res -> Type TyName (UniOf val) () typeSchemeToType TypeScheme val args res schB typeSchemeToType (TypeSchemeAll Proxy '(text, uniq, kind) proxy TypeScheme val args res schK) = case Proxy '(text, uniq, kind) proxy of (Proxy '(text, uniq, kind) _ :: Proxy '(text, uniq, kind)) -> let text :: Text text = String -> Text Text.pack (String -> Text) -> String -> Text forall a b. (a -> b) -> a -> b $ Proxy text -> String forall (n :: Symbol) (proxy :: Symbol -> *). KnownSymbol n => proxy n -> String symbolVal @text Proxy text forall k (t :: k). Proxy t Proxy uniq :: Int uniq = Integer -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Integer -> Int) -> Integer -> Int forall a b. (a -> b) -> a -> b $ Proxy uniq -> Integer forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Integer natVal @uniq Proxy uniq forall k (t :: k). Proxy t Proxy a :: TyName a = Name -> TyName TyName (Name -> TyName) -> Name -> TyName forall a b. (a -> b) -> a -> b $ Text -> Unique -> Name Name Text text (Unique -> Name) -> Unique -> Name forall a b. (a -> b) -> a -> b $ Int -> Unique Unique Int uniq in () -> TyName -> Kind () -> Type TyName (UniOf val) () -> Type TyName (UniOf val) () forall tyname (uni :: * -> *) ann. ann -> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann TyForall () TyName a (SingKind kind -> Kind () forall k. SingKind k -> Kind () demoteKind (SingKind kind -> Kind ()) -> SingKind kind -> Kind () forall a b. (a -> b) -> a -> b $ KnownKind kind => SingKind kind forall k. KnownKind k => SingKind k knownKind @kind) (Type TyName (UniOf val) () -> Type TyName (UniOf val) ()) -> Type TyName (UniOf val) () -> Type TyName (UniOf val) () forall a b. (a -> b) -> a -> b $ TypeScheme val args res -> Type TyName (UniOf val) () forall val (args :: [*]) res. TypeScheme val args res -> Type TyName (UniOf val) () typeSchemeToType TypeScheme val args res schK {- Note [Pattern matching on built-in types] At the moment we really only support direct pattern matching on enumeration types: 'Void', 'Unit', 'Bool' etc. This is because the denotation of a builtin cannot construct general terms (as opposed to constants), only juggle the ones that were provided as arguments without changing them. So e.g. if we wanted to add the following data type: newtype AnInt = AnInt Int as a built-in type, we wouldn't be able to add the following function as its pattern matcher: matchAnInt :: AnInt -> (Int -> r) -> r matchAnInt (AnInt i) f = f i because currently we cannot express the @f i@ part using the builtins machinery as that would require applying an arbitrary Plutus Core function in the denotation of a builtin, which would allow us to return arbitrary terms from the builtin application machinery, which is something that we originally had, but decided to abandon due to performance concerns. But it's still possible to have @AnInt@ as a built-in type, it's just that instead of trying to make its pattern matcher into a builtin we can have the following builtin: anIntToInt :: AnInt -> Int anIntToInt (AnInt i) = i which fits perfectly well into the builtins machinery. Although that becomes annoying for more complex data types. For tuples we need to provide two projection functions ('fst' and 'snd') instead of a single pattern matcher, which is not too bad, but to get pattern matching on lists we need three built-in functions: @null@, @head@ and @tail@ and to require `Bool` to be in the universe to be able to define a PLC equivalent of matchList :: [a] -> r -> (a -> [a] -> r) -> r matchList xs z f = if null xs then z else f (head xs) (tail xs) If a constructor stores more than one value, the corresponding projection function packs them into a (possibly nested) pair, for example for data Data = Constr Integer [Data] | <...> we have (pseudocode): unConstrData (Constr i ds) = (i, ds) In order to get pattern matching over 'Data' we need a projection function per constructor as well as with lists, but writing (where the @Data@ suffix indicates that a function is a builtin that somehow corresponds to a constructor of 'Data') if isConstrData d then uncurry fConstr $ unConstrData d else if isMapData d then fMap $ unMapData d else if isListData d then fList $ unListData d else <...> is tedious and inefficient and so instead we have a single @chooseData@ builtin that matches on its @Data@ argument and chooses the appropriate branch (type instantiations and strictness concerns are omitted for clarity): chooseData (uncurry fConstr $ unConstrData d) (fMap $ unMapData d) (fList $ unListData d) <...> d which, for example, evaluates to @fMap es@ when @d@ is @Map es@ On the bright side, this encoding of pattern matchers does work, so maybe it's indeed worth to prioritize performance over convenience, especially given the fact that performance is of a concern to every single end user while the inconvenience is only a concern for the compiler writers and we don't add complex built-in types too often. -} {- Note [Representable built-in functions over polymorphic built-in types] In Note [Pattern matching on built-in types] we talked about how general higher-order polymorphic built-in functions are troubling, but polymorphic built-in functions can be troubling even in the first-order case. In a Plutus program we always pair constants of built-in types with their tags from the universe, which means that in order to produce a constant embedded into a program we need the tag of the type of that constant. We can't get that tag from a Plutus type -- those are gone at runtime, so the only place we can get a type tag from during evaluation is some already existing constant. I.e. the following built-in function is representable: tail : all a. [a] -> [a] because for constructing the result we need a type tag for @[a]@, but we have a value of that type as an argument and so we can extract the type tag from it. Same applies to swap : all a b. (a, b) -> (b, a) since 'SomeConstantOf' always contains a type tag for each type that a polymorphic built-in type is instantiated with and so constructing a type tag for @(b, a)@ given type tags for @a@ and @b@ is unproblematic. And so neither cons : all a. a -> [a] -> [a] is troubling (even though that ones requires checking at runtime that the element to be prepended is of the same type as the type of the elements of the list as it's impossible to enforce this kind of type safety in Haskell over possibly untyped PLC). However consider the following imaginary builtin: nil : all a. [a] we can't represent it for two reasons: 1. we don't have any argument providing us a type tag for @a@ and hence we can't construct a type tag for @[a]@ 2. it would be a very unsound builtin to have. We can only instantiate built-in types with other built-in types and so allowing @nil {some_non_built_in_type}@ would be a lie that couldn't reduce to anything since it's not even possible to represent a built-in list with non-built-in elements (even if there's zero of them) "Wait, but wouldn't @cons {some_non_built_in_type}@ be a lie as well?" -- No! Since @cons@ does not just construct a list filled with elements of a non-built-in type but also expects one as an argument and providing such an argument is impossible, 'cause it's pretty much the same thing as populating 'Void' -- both values are equally unrepresentable. And so @cons {some_non_built_in_type}@ is a way to say @absurd@, which is perfectly fine to have. Finally, comma :: all a b. a -> b -> (a, b) is representable (because we can require arguments to be constants carrying universes with them, which we can use to construct the resulting universe), but is still a lie, because instantiating that builtin with non-built-in types is possible and so the PLC type checker won't throw on such an instantiation, which will become 'EvalutionFailure' at runtime the moment unlifting of a non-constant is attempted when a constant is expected. So could we still get @nil@ or a safe version of @comma@ somehow? Well, we could have this weirdness: nilOfTypeOf : all a. [a] -> [a] i.e. ask for an already existing list, but ignore the actual list and only use the type tag. But since we're ignoring the actual list, can't we just not pass it in the first place? And instead pass around our good old friends, singletons. We should be able to do that, but it hasn't been investigated. Perhaps something along the lines of adding the following constructor to 'DefaultUni': DefaultUniProtoSing :: DefaultUni (Esc (Proxy @GHC.Type)) and then defining nil : all a. sing a -> [a] and then the Plutus Tx compiler can provide a type class or something for constructing singletons for built-in types. -}