hindsight-core
Copyright(c) 2024
LicenseBSD3
Maintainermaintainer@example.com
Stabilityexperimental
Safe HaskellNone
LanguageGHC2021

Hindsight.Events.Internal.Versioning

Description

This module provides the generic machinery for managing versioned type vectors. This is the foundation for event versioning but is completely generic - it could be used for any versioned system.

Version Vectors

An EventVersions is a type-level list of types, indexed by Peano numbers to track their positions. For example:

EventVersions PeanoZero (PeanoSucc (PeanoSucc PeanoZero))
  ≈ [PayloadV0, PayloadV1]

Use FromList to build version vectors from type-level lists.

Constraint Management

VersionConstraints allows us to track that each version in a vector satisfies some constraint (like JSON serialization). HasEvidenceList builds up this evidence inductively.

Payload Extraction

PayloadAtVersion extracts the type at a specific version index, with compile-time bounds checking via ValidateVersionBound.

Note: This is an internal module. Use Hindsight.Events for the public API.

Synopsis

Version Vectors

data EventVersions (startsAt :: PeanoNat) (finalCount :: PeanoNat) where Source #

Type-level vector of versioned payload types.

This GADT represents a non-empty list of types, indexed by Peano numbers. The indices track the "start" and "end" positions in the version sequence.

  • startsAt - The version number where this vector begins
  • finalCount - One past the last version (i.e., length when startsAt = 0)

Constructors:

  • Final - A single-element vector (the last/only version)
  • Then - Prepend a type to an existing vector (earlier versions)

Example: A vector of 3 versions (0, 1, 2):

Then PayloadV0 (Then PayloadV1 (Final PayloadV2))
  :: EventVersions PeanoZero (PeanoSucc (PeanoSucc (PeanoSucc PeanoZero)))

Constructors

Final :: forall (startsAt :: PeanoNat). Type -> EventVersions startsAt ('PeanoSucc startsAt)

Final version in the vector

Then :: forall (startsAt :: PeanoNat) (finalCount :: PeanoNat). Type -> EventVersions ('PeanoSucc startsAt) finalCount -> EventVersions startsAt finalCount

Prepend an earlier version

type family FromList (payloadList :: [Type]) :: k where ... Source #

Convert a type-level list to an EventVersions GADT

This has a polymorphic kind to allow recursive usage at different indices. The result kind is constrained at usage sites via EventVersionVector.

Equations

FromList '[a] = 'Final a :: EventVersions startsAt ('PeanoSucc startsAt) 
FromList (a ': rest) = 'Then a (FromList rest :: EventVersions ('PeanoSucc startsAt) finalCount) 

Version Vector Queries

type family FinalVersionType (vec :: EventVersions startsAt finalCount) where ... Source #

Extract the final (most recent) type from a version vector.

This traverses the vector structure to find the Final constructor.

Equations

FinalVersionType ('Final t :: EventVersions startsAt ('PeanoSucc startsAt)) = t 
FinalVersionType ('Then t rest :: EventVersions startsAt finalCount) = FinalVersionType rest 

type family PayloadAtVersion (idx :: PeanoNat) (vec :: EventVersions startsAt finalCount) where ... Source #

Extract the type at a specific version index.

Returns a compile error if the index is out of bounds.

Equations

PayloadAtVersion idx ('Final t :: EventVersions startsAt ('PeanoSucc startsAt)) = PeanoEqual idx startsAt t (TypeError ('Text "Version index out of bounds") :: Type) 
PayloadAtVersion idx ('Then t rest :: EventVersions startsAt finalCount) = PeanoEqual idx startsAt t (PayloadAtVersion idx rest) 

Constraint Management

data VersionConstraints (ts :: EventVersions startsAt finalCount) (c :: PeanoNat -> Type -> Constraint) where Source #

Evidence that each version in a vector satisfies some constraint.

This GADT packages up constraint evidence for all elements in an EventVersions vector. It's structurally similar to the vector itself:

The constraint c is indexed by version number and payload type:

c :: PeanoNat -> Type -> Constraint

Example: Prove all versions are serializable:

class (ToJSON payload, FromJSON payload) => Serializable (idx :: PeanoNat) payload
...
evidence :: VersionConstraints myVersions Serializable

Constructors

VersionConstraintsLast :: forall (c :: PeanoNat -> Type -> Constraint) (startsAt :: PeanoNat) t. c startsAt t => (Proxy startsAt, Proxy t) -> VersionConstraints ('Final t :: EventVersions startsAt ('PeanoSucc startsAt)) c

Evidence for a single-element vector

VersionConstraintsCons :: forall (c :: PeanoNat -> Type -> Constraint) (startsAt :: PeanoNat) t (finalCount :: PeanoNat) (ts' :: EventVersions ('PeanoSucc startsAt) finalCount). c startsAt t => (Proxy startsAt, Proxy t) -> VersionConstraints ts' c -> VersionConstraints ('Then t ts') c

Evidence for head + inductive evidence for tail

class HasEvidenceList (startsAt :: PeanoNat) (finalCount :: PeanoNat) (event :: k) (c :: k -> PeanoNat -> Type -> Constraint) (vec :: EventVersions startsAt finalCount) where Source #

Build constraint evidence for all elements in a version vector.

This class provides a way to automatically derive VersionConstraints evidence given:

  1. Evidence that each individual version satisfies the constraint c
  2. The structure of the version vector

The instances mirror the structure of EventVersions:

  • Base case: single-element vector (Final)
  • Inductive case: multi-element vector (Then)

Usage:

getEvidenceList :: VersionConstraints myVersions MyConstraint

Methods

getEvidenceList :: VersionConstraints vec (c event) Source #

Derive the constraint evidence

Instances

Instances details
(c event startsAt payload, HasEvidenceList ('PeanoSucc startsAt) finalCount event c ts) => HasEvidenceList startsAt finalCount (event :: k) (c :: k -> PeanoNat -> Type -> Constraint) ('Then payload ts :: EventVersions startsAt finalCount) Source #

Inductive case: Evidence for multi-version vector

Instance details

Defined in Hindsight.Events.Internal.Versioning

Methods

getEvidenceList :: VersionConstraints ('Then payload ts) (c event) Source #

c event startsAt payload => HasEvidenceList startsAt ('PeanoSucc startsAt) (event :: k) (c :: k -> PeanoNat -> Type -> Constraint) ('Final payload :: EventVersions startsAt ('PeanoSucc startsAt)) Source #

Base case: Evidence for a single-version vector

Instance details

Defined in Hindsight.Events.Internal.Versioning

Methods

getEvidenceList :: VersionConstraints ('Final payload :: EventVersions startsAt ('PeanoSucc startsAt)) (c event) Source #