-- | 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.
-}