Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Builtins] Disentangle 'KnownTypeAst' from 'KnownTypeIn' #4312

Merged
merged 13 commits into from
Jan 11, 2022
Merged

[Builtins] Disentangle 'KnownTypeAst' from 'KnownTypeIn' #4312

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
c1beb8a
[Builtins] Disentangle 'KnownTypeAst' from 'KnownTypeIn'
effectfully Jan 5, 2022
20fd9d8
Use class synonyms
effectfully Jan 5, 2022
4693b29
Drop some '~'
effectfully Jan 5, 2022
c42a9f2
Back to type synonyms
effectfully Jan 5, 2022
00740cd
Much better 'TypeScheme' inference machinery
effectfully Jan 6, 2022
8fcee47
Remove a now redundant dependency
effectfully Jan 6, 2022
7d3c855
fix 'nix'
effectfully Jan 6, 2022
d0f9195
Cleaning up
effectfully Jan 6, 2022
4ba7a72
Add some docs
effectfully Jan 7, 2022
f7bd7dd
More docs
effectfully Jan 7, 2022
0b360ad
A bit more docs
effectfully Jan 7, 2022
f10c848
Note [Unlifting values of built-in types]
effectfully Jan 10, 2022
f6426c1
Proofreading
effectfully Jan 10, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Cleaning up
  • Loading branch information
@effectfully
effectfully committed Jan 6, 2022
commit d0f9195bbcaf75e791483fd068ba9a1e1dfabebc
4 changes: 1 addition & 3 deletions plutus-core/plutus-core/examples/PlutusCore/Examples/Builtins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
91 changes: 11 additions & 80 deletions plutus-core/plutus-core/src/PlutusCore/Constant/Meaning.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

master:
Screenshot from 2022-01-07 22-42-36

this branch:
Screenshot from 2022-01-07 22-43-04

-- 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
Expand All @@ -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
Expand Down
66 changes: 21 additions & 45 deletions plutus-core/plutus-core/src/PlutusCore/Constant/Typed.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,8 @@ module PlutusCore.Constant.Typed
, FromConstant (..)
, HasConstant
, HasConstantIn
, RepInfer
, TypeInfer
, RepHole
, TypeHole
, KnownBuiltinTypeAst
, KnownTypeAst (..)
, Merge
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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 ()
Expand All @@ -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
Expand Down