Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Parametrise the Shelley ledger over Value.
This PR demonstrates a way to parametrise the ledger over value. It paves the way for overriding this type in subsequent eras, without making any semantic changes to the Shelley ledger. Functions in the ledger are now classfied into three groups: - Those that remain universally quantified over eras. - Those that have specific requirements on certain era-parametrised types to work (e.g. that they can be serialised), and - Those that are specific to Shelley. There are two examples of the latter: `consumed` and `produced`. The STS rules are likewise split in two: - Those that remain universally quantified over eras. - Those that are specific to Shelley. The intention is that many will transition to the third (missing) category, where the actual rules specify their exact requirements on the era (see #1804 for an example of how to do this). This was not done because I wanted to get this ready for the meeting and I didn't have time. This PR makes some very deliberate design choices: - The 'Value' type family and any constraints thereon are _not_ lifted into the 'Era' class. Such would imply universality over eras, which is too strong a constraint. They would prevent us, for example, from adding to the `Val` class in future eras, which seems quite plausible. Furthermore, having more explicit constraints at the use site helps our understanding of the code; it is much more obvious _when_ we are relying on certain things, which can be a tool to spot bugs. Note that these constraints do not propogate wildly, because in general they are dispatched through the instantiation of the type family to a specific type in a given era. - It deliberately removes some instances (`Eq` for example) where it seems there is no strong reason to have it. The presence of an `Eq` instance everywhere has bitten us in the past, where for example we have ended up calling `(==)` on a large part of state in the consensus integration, which is an expensive operation. Honestly, I suspect I'll have to add these back to get the tests working, since they rely on them, but I think there's a decent case for making these instances orphans in the testing code instead. This is a *draft* PR for discussion. It does not yet touch the testing code, and is inconsistent about various things (in particular, I stuck `era ~ Shelley c` in a lot of places in a hurry).
- Loading branch information
1 parent
ba2d8d5
commit ce3dac5
Showing
29 changed files
with
773 additions
and
253 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
76 changes: 76 additions & 0 deletions
76
shelley/chain-and-ledger/executable-spec/src/Cardano/Ledger/Core.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,76 @@ | ||
{-# LANGUAGE FlexibleContexts #-} | ||
{-# LANGUAGE FlexibleInstances #-} | ||
{-# LANGUAGE TypeFamilies #-} | ||
{-# LANGUAGE UndecidableInstances #-} | ||
|
||
-- | This module defines core type families which we know to vary from era to | ||
-- era. | ||
-- | ||
-- Families in this module should be indexed on era. | ||
-- | ||
-- It is intended for qualified import: | ||
-- > import qualified Cardano.Ledger.Core as Core | ||
module Cardano.Ledger.Core | ||
( -- * Compactible | ||
Compactible (..), | ||
Compact (..), | ||
ValType, | ||
Value, | ||
) | ||
where | ||
|
||
import Cardano.Binary (FromCBOR (..), ToCBOR (..)) | ||
import Cardano.Prelude (NFData, NoUnexpectedThunks (..)) | ||
import Data.Kind (Type) | ||
import Data.Typeable (Typeable) | ||
|
||
class | ||
( Compactible (Value era), | ||
Eq (Value era), | ||
FromCBOR (CompactForm (Value era)), | ||
FromCBOR (Value era), | ||
NFData (Value era), | ||
NoUnexpectedThunks (Value era), | ||
Show (Value era), | ||
ToCBOR (CompactForm (Value era)), | ||
ToCBOR (Value era), | ||
Typeable (Value era) | ||
) => | ||
ValType era | ||
|
||
type family Value era :: Type | ||
|
||
-- | A value is something which quantifies a transaction output. | ||
|
||
-------------------------------------------------------------------------------- | ||
|
||
-- * Compactible | ||
|
||
-- | ||
-- Certain types may have a "presentation" form and a more compact | ||
-- representation that allows for more efficient memory usage. In this case, | ||
-- one should make instances of the 'Compactible' class for them. | ||
-------------------------------------------------------------------------------- | ||
|
||
class Compactible a where | ||
data CompactForm a :: Type | ||
toCompact :: a -> CompactForm a | ||
fromCompact :: CompactForm a -> a | ||
|
||
newtype Compact a = Compact {unCompact :: a} | ||
|
||
instance | ||
(Typeable a, Compactible a, ToCBOR (CompactForm a)) => | ||
ToCBOR (Compact a) | ||
where | ||
toCBOR = toCBOR . toCompact . unCompact | ||
|
||
instance | ||
(Typeable a, Compactible a, FromCBOR (CompactForm a)) => | ||
FromCBOR (Compact a) | ||
where | ||
fromCBOR = Compact . fromCompact <$> fromCBOR | ||
|
||
-- TODO: consider if this is better the other way around | ||
instance (Eq a, Compactible a) => Eq (CompactForm a) where | ||
a == b = fromCompact a == fromCompact b |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.