Copyright	(c) 2024
License	BSD3
Maintainer	maintainer@example.com
Stability	experimental
Safe Haskell	None
Language	GHC2021

Hindsight.Events.Internal.TypeLevel

Contents

Peano Natural Numbers
- Conversions
Constraint Evidence
Type-Level Comparisons
Type-Level List Utilities

Description

This module provides foundational type-level utilities used throughout the Hindsight event system. These utilities are completely generic and not specific to events.

Peano Numbers

Peano natural numbers (PeanoNat) are used for type-level arithmetic and indexing. They're more amenable to pattern matching than GHC's built-in Nat kind, though we provide conversions between the two.

Constraint Evidence

The Dict type allows us to package up constraint evidence and pass it around at runtime, enabling flexible constraint manipulation.

Type-Level Comparisons

PeanoEqual provides compile-time conditionals based on type-level numbers.

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

Synopsis

data PeanoNat
- = PeanoZero
- | PeanoSucc PeanoNat
class ReifiablePeanoNat (n :: PeanoNat) where
- reifyPeanoNat :: Integer
type family ToPeanoNat (n :: Nat) :: PeanoNat where ...
type family FromPeanoNat (n :: PeanoNat) :: Nat where ...
data Dict c where
- Dict :: forall c. c => Dict c
type family PeanoEqual (a :: PeanoNat) (b :: PeanoNat) (thenResult :: result) (elseResult :: result) :: result where ...
type family ListLength (xs :: [Type]) :: PeanoNat where ...
type family AssertPeanoEqual (actual :: PeanoNat) (expected :: PeanoNat) (errorMsg :: ErrorMessage) where ...

Peano Natural Numbers

data PeanoNat Source #

Type-level Peano natural numbers.

These provide an alternative representation to GHC's Nat that's more suitable for structural recursion and pattern matching at the type level.

0 = PeanoZero
1 = PeanoSucc PeanoZero
2 = PeanoSucc (PeanoSucc PeanoZero)
...

Constructors

PeanoZero
PeanoSucc PeanoNat

class ReifiablePeanoNat (n :: PeanoNat) where Source #

Convert type-level Peano numbers to runtime integers.

This class allows us to "reify" type-level numbers into runtime values, which is necessary for parsing version numbers from JSON and other runtime operations.

Methods

reifyPeanoNat :: Integer Source #

Get the runtime integer value of a Peano number

Instances

Instances details

ReifiablePeanoNat 'PeanoZero Source #
Instance details Defined in Hindsight.Events.Internal.TypeLevel Methods reifyPeanoNat :: Integer Source #
ReifiablePeanoNat n => ReifiablePeanoNat ('PeanoSucc n) Source #
Instance details Defined in Hindsight.Events.Internal.TypeLevel Methods reifyPeanoNat :: Integer Source #

Conversions

type family ToPeanoNat (n :: Nat) :: PeanoNat where ... Source #

Convert GHC's Nat to Peano representation.

This is needed because type families and data families use Nat, but we need PeanoNat for structural pattern matching.

Equations

ToPeanoNat 0 = 'PeanoZero
ToPeanoNat n = 'PeanoSucc (ToPeanoNat (n - 1))

type family FromPeanoNat (n :: PeanoNat) :: Nat where ... Source #

Convert Peano representation back to GHC's Nat.

This is the inverse of ToPeanoNat and is needed for some constraint manipulations where GHC requires Nat.

Equations

FromPeanoNat 'PeanoZero = 0
FromPeanoNat ('PeanoSucc n) = 1 + FromPeanoNat n

Constraint Evidence

data Dict c where Source #

Dictionary carrying constraint evidence.

This allows us to package up constraints and manipulate them at runtime. It's particularly useful for passing around evidence that certain type-level properties hold.

Example use: storing evidence that a payload satisfies serialization constraints so we can retrieve it later when needed.

Constructors

Dict :: forall c. c => Dict c

Type-Level Comparisons

type family PeanoEqual (a :: PeanoNat) (b :: PeanoNat) (thenResult :: result) (elseResult :: result) :: result where ... Source #

Type-level equality check with conditional results.

Returns thenResult if a and b are equal, elseResult otherwise.

This is used for version number matching.

PeanoEqual PeanoZero PeanoZero "yes" "no" = "yes"
PeanoEqual (PeanoSucc PeanoZero) PeanoZero "yes" "no" = "no"

Equations

PeanoEqual n n (thenResult :: result) (_1 :: result) = thenResult
PeanoEqual n m (_1 :: result) (elseResult :: result) = elseResult

Type-Level List Utilities

type family ListLength (xs :: [Type]) :: PeanoNat where ... Source #

Compute the length of a type-level list as a Peano number.

This is used to validate that the number of versions declared in a Versions list matches the MaxVersion annotation.

ListLength '[] = PeanoZero
ListLength '[A] = PeanoSucc PeanoZero
ListLength '[A, B, C] = PeanoSucc (PeanoSucc (PeanoSucc PeanoZero))

Equations

ListLength ('[] :: [Type]) = 'PeanoZero
ListLength (_1 ': xs) = 'PeanoSucc (ListLength xs)

type family AssertPeanoEqual (actual :: PeanoNat) (expected :: PeanoNat) (errorMsg :: ErrorMessage) where ... Source #

Assert that two Peano numbers are equal, producing a custom error if not.

This is a generic type-level equality check with custom error messages. The error message is provided by the caller, allowing this utility to be reused in different contexts.

Example usage:

type CheckListLength xs expectedLen =
  AssertPeanoEqual
    (ListLength xs)
    expectedLen
    ('Text "List length mismatch: expected " ':<>: 'ShowType expectedLen)

Equations

AssertPeanoEqual n n _1 = ()
AssertPeanoEqual _1 _2 errorMsg = TypeError errorMsg :: Constraint