diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,12 @@ # Changelog for polytropos-core +## 0.1.0.3 — 2026-11-03 + +- Reified Row Morphisms (`RowMorph`): static permutation arrays and `KnownRowMorph` TcPlugin solver for compile-time peephole route fusion. +- Frame-Rule automatic register wiring (`FrameWire`): TcPlugin solver for compile-time gather and scatter plans. +- Poly-kinded `ConstructorIndex` solver supporting effect operations (`Type -> Type`) over open variant rows. +- Coordinated release across all Polytropos packages, benchmarks, and examples. + ## 0.1.0.2 — 2026-10-21 - Coordinated release across all 20 Polytropos packages, benchmarks, and examples. diff --git a/polytropos-core.cabal b/polytropos-core.cabal --- a/polytropos-core.cabal +++ b/polytropos-core.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: polytropos-core -version: 0.1.0.2 +version: 0.1.0.3 synopsis: Row-polymorphic / open ADTs: rows, generic representation, evidence description: Core engine and consumer surface of : @@ -48,6 +48,7 @@ import: warnings exposed-modules: Polytropos , Polytropos.Core + , Polytropos.RowMorph hs-source-dirs: src default-language: GHC2021 build-depends: base >= 4.18 && < 4.23 diff --git a/src/Polytropos.hs b/src/Polytropos.hs --- a/src/Polytropos.hs +++ b/src/Polytropos.hs @@ -222,9 +222,12 @@ , type Variant , type VariantF -- * Row Vocabulary & Types + , type RowOf , type Row + , type SumRowOf , type SumRow , type ProductRow + , type EffectRowOf #if __GLASGOW_HASKELL__ >= 914 , data Variant , data VariantF @@ -252,6 +255,19 @@ , widenVariantF , narrowVariant , narrowVariantF + -- * Reified Row Morphisms & Routing + , RowMorph(..) + , KnownRowMorph(..) + , composeRowMorph + , indexRowMorph + , gatherRep + , scatterRep + , gatherRecord + , scatterRecord + , FramePlan(..) + , FrameWire(..) + , executeFrameScatter + , executeFrameRecord -- * Elimination & Peeling , peel , peelF @@ -308,6 +324,7 @@ ) where import Polytropos.Core +import Polytropos.RowMorph import Data.Functor.Identity (Identity(..)) import Data.Kind (Type) import Data.Primitive.SmallArray (copySmallArray, indexSmallArray, newSmallArray, runSmallArray, sizeofSmallArray, thawSmallArray, writeSmallArray) @@ -339,6 +356,9 @@ 3. Safe Combinators: - Projection (`projectRecord`), widening (`widenVariant`), narrowing (`narrowVariant`), peeling (`peel`), and elimination (`eliminateUniform`). + 4. Poly-Kinded Effect Rows: + - Supports multi-sorted effect rows (`EffectRowOf PolyEffect`, `EffectRowOf PolyHEffect`) + with literal zero-residual index solving (see Note [Poly-Kinded Row Indexing for Multi-Sorted Effects] [ref:note-poly-kinded-indexing]). All of these combinators maintain complete type safety, ensuring that raw memory coercions (`noInlineUnsafeCo`, `unsafeCoerce`) are strictly encapsulated inside proven plugin-driven invariants. @@ -678,6 +698,36 @@ in case drop tag narrowMap of (Just subTag : _) -> Just (RowRep (Rep subTag (repVals rep))) _ -> Nothing + +{------------------------------------------------------------------------------- + Reified Row Morphisms & Routing +-------------------------------------------------------------------------------} + +-- | Contravariant gather for 'Record': extracts sub-record fields in \(\mathcal{O}(|sub|)\) +-- using a reified 'RowMorph'. +-- +-- See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing] +gatherRecord :: RowMorph sub full -> Record full -> Record sub +gatherRecord morph (RowRep rep) = RowRep (gatherRep morph rep) + +-- | Scatter updates for 'Record': overwrites sub-record fields into full record in \(\mathcal{O}(|full|)\) +-- using a reified 'RowMorph'. +-- +-- See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing] +scatterRecord :: RowMorph sub full -> Record sub -> Record full -> Record full +scatterRecord morph (RowRep sub) (RowRep full) = RowRep (scatterRep morph sub full) + +-- | High-level record runner for 'FramePlan': merges the previous frame @frameIn@ +-- and the operation output @opOut@ into the next frame @frameOut@ in two tight loops. +-- +-- See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring] +executeFrameRecord + :: FramePlan frameIn opIn opOut frameOut + -> Record frameIn + -> Record opOut + -> Record frameOut +executeFrameRecord plan (RowRep baseRep) (RowRep opRep) = + RowRep (executeFrameScatter plan baseRep opRep) {------------------------------------------------------------------------------- Elimination & Peeling diff --git a/src/Polytropos/Core.hs b/src/Polytropos/Core.hs --- a/src/Polytropos/Core.hs +++ b/src/Polytropos/Core.hs @@ -75,6 +75,7 @@ , SumRow , SumRowHKD , SumRowF + , EffectRowOf -- * Type-level row metadata , FieldNames , SimpleFieldTypes @@ -301,6 +302,41 @@ tag overwrite, and pointer hand-off! -} +{- Note [Poly-Kinded Row Indexing for Multi-Sorted Effects] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-poly-kinded-indexing] +Algebraic effect systems such as Penelope model effectful computations via +open polycategorical effect rows: + - First-order effect rows: `ef :: RowOf PolyEffect` (or `EffectRowOf PolyEffect`), + where `PolyEffect = Row Type -> Row (Row Type) -> Type`. + - Higher-order effect rows: `eh :: RowOf PolyHEffect` (or `EffectRowOf PolyHEffect`), + where `PolyHEffect = (PortSig -> Type) -> Row PortSig -> Row Type -> Row (Row Type) -> Type`. + +Historically, extensible effect engines (e.g. `polysemy` or `freer-simple`) used Peano-indexed +typeclasses (`Member e r`) requiring O(N) recursive dictionary search at compile time, +and linear type-directed unpacking at runtime. + +In Polytropos, effect rows are simply poly-kinded rows `[Pair Symbol k]` or unlabeled lists `[k]`: +1. Dual Modality Lookup: + - Named symbol lookup: `ConstructorIndex "state" ef` or `FieldIndex "state" ef StateEff` + resolves the 0-based offset of the effect label in O(1) compile time. + - Type-indexed lookup: `ConstructorIndex StateEff ef` or `FieldIndex StateEff ef StateEff` + resolves by matching the higher-kinded effect type constructor `StateEff` via `eqType`. +2. Anonymous and Unlabeled Effect Rows: + - When an effect row is specified without labels (e.g. `'[StateEff, LogEff]`), each entry + is parsed with an empty symbol label (`nilFS`). Type-indexed lookup locates the slot + matching `StateEff` directly. +3. Inferred Effect Resolution: + - For `FieldIndex "label" ef a`, if the expected effect signature `a` is an uninstantiated + type variable, the TcPlugin synthesizes a nominal equality constraint (`a ~# StateEff`), + allowing call-site effect operations (e.g. `sendPolyF @"state"`) to infer the operation's + concrete effect signature automatically without redundant type annotations. +4. Zero-Overhead Core Emission: + - `Polytropos.Plugin` emits literal unboxed `Word#` or `Int#` constants wrapped in the + corresponding dictionary constructor (`evDataConApp`), generating zero residual search loops + or dictionary lookups in Core. +-} + {------------------------------------------------------------------------------- §1 The row vocabulary -------------------------------------------------------------------------------} @@ -379,6 +415,15 @@ -- | Synonym for 'SumRowHKD'. type SumRowF (f :: Type -> Type) = SumRowHKD f +-- | A poly-kinded effect row whose effect specifications have kind @k@. +-- +-- [ref:note-poly-kinded-indexing] +-- Effect rows map effect identifier symbols (or types) to their effect operations. +-- Typical kinds for @k@ include: +-- * @PolyEffect = Row Type -> Row (Row Type) -> Type@ (first-order operations) +-- * @PolyHEffect = (PortSig -> Type) -> Row PortSig -> Row Type -> Row (Row Type) -> Type@ (higher-order operations) +type EffectRowOf k = [Pair Symbol k] + {------------------------------------------------------------------------------- §1b Type-level row metadata (rewritten by TcPlugin) @@ -901,6 +946,8 @@ -- The plugin solves this by inspecting the row and emitting the index as a -- literal (obligation 1, design note §5). -- +-- [ref:note-literal-evidence] +-- [ref:note-poly-kinded-indexing] -- Algorithmic Mechanics: -- When GHC encounters a wanted constraint `FieldIndex "foo" r a`, the plugin -- scans the type-level list `r` for the entry `"foo" ':= a`. It returns the @@ -915,6 +962,8 @@ -- The plugin solves this by inspecting the row and emitting the tag as a -- literal (obligation 2, design note §5). -- +-- [ref:note-literal-evidence] +-- [ref:note-poly-kinded-indexing] -- Algorithmic Mechanics: -- For wanted `ConstructorIndex "Bar" s`, the plugin locates `"Bar"` in the sum -- row `s` and produces an unboxed integer literal `Lit (MachWord t)`. diff --git a/src/Polytropos/RowMorph.hs b/src/Polytropos/RowMorph.hs new file mode 100644 --- /dev/null +++ b/src/Polytropos/RowMorph.hs @@ -0,0 +1,344 @@ +{-| +Module : Polytropos.RowMorph +Description : Reified unboxed row morphisms and primitive gather/scatter operations +Copyright : (c) 2026 The Polytropos Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Reified unboxed row morphisms and primitive gather/scatter operations for @polytropos@. + += Architectural Overview & Rationale + +In conventional polymorphic record and pipeline architectures, wire routing and subrow +projection typically incur either: +1. Opaque runtime closures (@arr (\\(a, (b, c)) -> (b, a))@) that prevent static inspection, + optimizer inlining, and peephole fusion. +2. Inductive type-level searches (@KnownNat@ / inductive dictionary trees) that generate + \(O(N)\) or \(O(N^2)\) pointer-chasing calls at runtime. + +'RowMorph' collapses row routing and projection into a single unboxed 'PrimArray' 'Int' +(backed by a contiguous 'GHC.Exts.ByteArray#' primitive). Each index @i@ in @[0 .. |r1| - 1]@ +contains the literal 0-based slot offset in the target row @r2@. + +== Key Features & Operations + +* __Unboxed Reification:__ 'RowMorph' has zero heap allocation overhead per element, storing + pure integer indices densely in cache lines. +* __\(O(|r1|)\) Category Composition:__ 'composeRowMorph' composes two morphisms in a single + branchless pass, computing @m23(m12(i))@ into a newly allocated 'PrimArray' without intermediate lists. +* __Contravariant Reduct Gather:__ 'gatherRep' extracts an arbitrary subrow or permutation from + an existing 'Polytropos.Core.Rep' in \(O(|sub|)\) time with a single 'Data.Primitive.SmallArray.SmallArray' allocation. +* __In-Place Scatter:__ 'scatterRep' writes back updated subrow slots into an existing 'Rep' + in \(O(|full|)\) time via 'Data.Primitive.SmallArray.thawSmallArray'. +* __Compile-Time Synthesis:__ The evidence class 'KnownRowMorph' is solved directly by + @Polytropos.Plugin@, emitting literal index vectors into Core AST with zero runtime dictionary search. +* __Frame-Rule Auto-Wiring:__ 'FramePlan' and 'FrameWire' generalize binary port routing + to stateful execution frames with automatic output row synthesis (see Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring]). + += Note [Reified Row Morphisms and Gather-Scatter] [tag:note-row-morph-routing] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A row morphism @RowMorph r1 r2@ models a structural embedding / projection map from @r1@ into @r2@. +Rather than representing morphisms as functions @Record r2 -> Record r1@ or type-level inductive +witnesses, 'RowMorph' reifies the mapping as a flat primitive array of integers. + +1. Category Structure: + - Identity: @idMorph = RowMorph [0, 1, .. n-1]@. + - Composition: @composeRowMorph m12 m23@ computes @dstIdx = m23[m12[i]]@ for all @i@. + Associativity @(m1 >>> m2) >>> m3 == m1 >>> (m2 >>> m3)@ holds strictly by array index equality. + +2. Contravariant Reduct / Port Gather: + Given a wider register frame or handler record @full@ and a required sub-signature @sub@, + @gatherRep morph full@ acts as the contravariant reduct \(\mathrm{Mod}(\sigma)(M')\), pulling + exactly the active ports or handler methods into a compact, contiguous memory buffer. + +3. Frame-Rule Auto-Wiring: + 'FramePlan' and 'FrameWire' generalize binary port routing to stateful execution frames: + an operation @(opIn -> opOut)@ inside @(frameIn -> frameOut)@ executes by gathering @opIn@ + from @frameIn@, copying surviving @frameIn@ slots to @frameOut@, and scattering @opOut@ into @frameOut@ + in two tight branchless loops. + See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring]. + += Note [Frame-Rule Automatic Wire Synthesis] [tag:note-frame-rule-wiring] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In polycategorical and symmetric monoidal effect systems (such as Penelope), +computation is organized into multi-input, multi-output arrows or pipeline stages +executed against an ambient state/register frame: + + stage :: Arrow p => p (Record opIn) (Record opOut) + +When executing @stage@ inside a wider frame @frameIn@, the categorical frame rule +states that the ambient context survives unchanged except where explicitly modified: + + frame :: FrameWire frameIn opIn opOut frameOut + => p (Record opIn) (Record opOut) + -> p (Record frameIn) (Record frameOut) + +1. Dual Gather-Scatter Lifecycle: + Execution proceeds in two phases coordinated by 'FramePlan': + a. Contravariant Port Gather: + Before the operation runs, its input ports @opIn@ are gathered from @frameIn@ + via @fpGatherIn :: RowMorph opIn frameIn@. + b. Frame Merge & Output Scatter ('executeFrameScatter'): + After the operation produces @opOut@, the new frame @frameOut@ is synthesized: + - Surviving @frameIn@ slots are written to @frameOut@ via @fpBaseScatter@. + - Output ports @opOut@ are written to @frameOut@ via @fpOpScatter@, overwriting + matching input ports and appending any fresh ports in two tight loops. + +2. Compile-Time Synthesis by Polytropos.Plugin: + Rather than performing associative map lookups or recursive type-level list + rewriting at runtime, the evidence class 'FrameWire' is solved directly by + the typechecker plugin: + - Sub-Row & Type Verification: Asserts that every port in @opIn@ exists in @frameIn@. + If polymorphic port type variables are present, nominal equality constraints + (@inTy ~# fTy@) are emitted, driving bidirectional port inference across pipeline stages. + - Canonical Row Overwrite: Computes @RowOverwrite frameIn opOut@ where matching labels + in @frameIn@ receive updated types from @opOut@, untouched labels are preserved in + their original order, and new labels from @opOut@ are appended. + - Automatic Output Row Unification: Emits a wanted nominal equality constraint + @frameOut ~# synthOutTy@. When chaining stages @stage1 >&> stage2@, downstream + frame outputs are automatically inferred without manual type signatures. + - Literal Core AST Synthesis: Synthesizes a call to 'unsafeMkFramePlan' with + pre-computed integer lists for @gatherIdxs@, @baseIdxs@, and @opIdxs@, + which bake directly into unboxed 'PrimArray' arrays in the binary with zero + heap traversal. +-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RoleAnnotations #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} + +module Polytropos.RowMorph + ( -- * Reified Row Morphisms + RowMorph(..) + , KnownRowMorph(..) + , unsafeMkRowMorph + , composeRowMorph + , indexRowMorph + -- * Record Gather & Scatter over Rep + , gatherRep + , scatterRep + -- * Frame-Rule Auto-Wiring Plan + , FramePlan(..) + , FrameWire(..) + , unsafeMkFramePlan + , executeFrameScatter + ) where + +import Control.Monad.ST + ( runST + ) +import Data.Kind + ( Constraint + , Type + ) +import Data.Primitive.PrimArray + ( PrimArray + , indexPrimArray + , newPrimArray + , primArrayFromList + , sizeofPrimArray + , unsafeFreezePrimArray + , writePrimArray + ) +import Data.Primitive.SmallArray + ( indexSmallArray + , newSmallArray + , runSmallArray + , sizeofSmallArray + , thawSmallArray + , writeSmallArray + ) +import Polytropos.Core + ( Rep(..) + ) + +{------------------------------------------------------------------------------- + Reified Row Morphisms +-------------------------------------------------------------------------------} + +-- | A compile-time synthesized slot injection map from @r1@ into @r2@. +-- +-- Each index @i@ in @[0 .. |r1| - 1]@ maps to its target slot in @[0 .. |r2| - 1]@. +-- Backed by an unboxed 'PrimArray' 'Int' with nominal type role parameters, +-- preventing illicit coercions across distinct row types. +-- +-- See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing] +type RowMorph :: forall {k1} {k2}. k1 -> k2 -> Type +type role RowMorph nominal nominal +newtype RowMorph (r1 :: k1) (r2 :: k2) = RowMorph + { unRowMorph :: PrimArray Int } + deriving stock (Eq, Show) + +-- | Solved by @Polytropos.Plugin@ into a static 'RowMorph' CAF constant. +-- +-- When @r1@ is a subrow or permutation of @r2@, the compiler plugin synthesizes +-- the literal permutation array and emits the instance dictionary directly into Core AST. +type KnownRowMorph :: forall {k1} {k2}. k1 -> k2 -> Constraint +class KnownRowMorph (r1 :: k1) (r2 :: k2) where + rowMorph :: RowMorph r1 r2 + +-- | Entry point called by Core expressions synthesized by @Polytropos.Plugin@. +-- +-- Must be marked @NOINLINE@ to establish an optimization barrier for the Core simplifier. +unsafeMkRowMorph :: forall {k1} {k2} (r1 :: k1) (r2 :: k2). [Int] -> RowMorph r1 r2 +{-# NOINLINE unsafeMkRowMorph #-} +unsafeMkRowMorph idxs = RowMorph (primArrayFromList idxs) + +-- | Reads the target slot index for the @i@-th entry of @r1@. +indexRowMorph :: RowMorph r1 r2 -> Int -> Int +{-# INLINE indexRowMorph #-} +indexRowMorph (RowMorph arr) !i = indexPrimArray arr i + +-- | Category composition for 'RowMorph': \(\mathcal{O}(|r1|)\) primitive array indexing. +-- +-- Given morphisms @m12 : r1 -> r2@ and @m23 : r2 -> r3@, computes @m13 : r1 -> r3@ +-- where each slot @i@ in @r1@ maps to @m23(m12(i))@ in @r3@. +-- +-- See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing] +composeRowMorph :: RowMorph r1 r2 -> RowMorph r2 r3 -> RowMorph r1 r3 +{-# INLINE composeRowMorph #-} +composeRowMorph (RowMorph m12) (RowMorph m23) = RowMorph $ runST $ do + let !n = sizeofPrimArray m12 + out <- newPrimArray n + let go !i + | i >= n = unsafeFreezePrimArray out + | otherwise = do + let !midIdx = indexPrimArray m12 i + !dstIdx = indexPrimArray m23 midIdx + writePrimArray out i dstIdx + go (i + 1) + go 0 + +{------------------------------------------------------------------------------- + Record Gather & Scatter over Rep +-------------------------------------------------------------------------------} + +-- | Contravariant reduct / port gather: extracts @sub@ slots from @full@ in \(\mathcal{O}(|sub|)\). +-- +-- Directly implements \(\mathrm{Mod}(\sigma)(M')\) for handler records, input port frames, +-- and structural subrow extraction with a single 'SmallArray' allocation. +-- +-- See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing] +gatherRep :: RowMorph sub full -> Rep f a -> Rep f b +{-# INLINE gatherRep #-} +gatherRep (RowMorph morph) (Rep _ srcArr) = Rep 0 $ runSmallArray $ do + let !n = sizeofPrimArray morph + dstArr <- newSmallArray n (error "gatherRep: uninitialized slot") + let go !i + | i >= n = pure dstArr + | otherwise = do + let !srcIdx = indexPrimArray morph i + writeSmallArray dstArr i (indexSmallArray srcArr srcIdx) + go (i + 1) + go 0 + +-- | Overwrites @sub@ slots inside an existing @full@ record in \(\mathcal{O}(|full|)\). +-- +-- Preserves the runtime constructor tag of the target representation while updating +-- matching slots in place via array thawing and non-overlapping writes. +scatterRep :: RowMorph sub full -> Rep f a -> Rep f b -> Rep f b +{-# INLINE scatterRep #-} +scatterRep (RowMorph morph) (Rep _ subArr) (Rep t fullArr) = Rep t $ runSmallArray $ do + let !fullLen = sizeofSmallArray fullArr + !subLen = sizeofPrimArray morph + dstArr <- thawSmallArray fullArr 0 fullLen + let go !i + | i >= subLen = pure dstArr + | otherwise = do + let !targetIdx = indexPrimArray morph i + writeSmallArray dstArr targetIdx (indexSmallArray subArr i) + go (i + 1) + go 0 + +{------------------------------------------------------------------------------- + Frame-Rule Auto-Wiring Plan +-------------------------------------------------------------------------------} + +-- | Concrete execution plan for wiring an operation @(opIn -> opOut)@ +-- inside a live register frame @(frameIn -> frameOut)@. +-- +-- See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing] +-- See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring] +type FramePlan :: forall {k1} {k2} {k3} {k4}. k1 -> k2 -> k3 -> k4 -> Type +data FramePlan frameIn opIn opOut frameOut = FramePlan + { fpOutSize :: {-# UNPACK #-} !Int + , fpGatherIn :: !(RowMorph opIn frameIn) + -- ^ Gathers the operation's input ports from @frameIn@. + , fpBaseScatter :: !(RowMorph frameIn frameOut) + -- ^ Places surviving @frameIn@ ports into @frameOut@. + , fpOpScatter :: !(RowMorph opOut frameOut) + -- ^ Places @opOut@ ports into @frameOut@ (overwriting collided @frameIn@ ports). + } + deriving stock (Eq, Show) + +-- | Solved by @Polytropos.Plugin@: +-- 1. Verifies @opIn@ is a subrow of @frameIn@ (unifying port types). +-- 2. Synthesizes @frameOut ~ RowOverwrite frameIn opOut@. +-- 3. Emits the 'FramePlan' dictionary. +-- +-- See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring] +type FrameWire :: forall {k1} {k2} {k3} {k4}. k1 -> k2 -> k3 -> k4 -> Constraint +class FrameWire frameIn opIn opOut frameOut where + framePlan :: FramePlan frameIn opIn opOut frameOut + +-- | Entry point called by Core expressions synthesized by @Polytropos.Plugin@ for 'FrameWire'. +-- +-- See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring] +unsafeMkFramePlan + :: forall {k1} {k2} {k3} {k4} (frameIn :: k1) (opIn :: k2) (opOut :: k3) (frameOut :: k4). + Int + -> [Int] + -> [Int] + -> [Int] + -> FramePlan frameIn opIn opOut frameOut +{-# NOINLINE unsafeMkFramePlan #-} +unsafeMkFramePlan outSz gatherIdxs baseIdxs opIdxs = FramePlan + { fpOutSize = outSz + , fpGatherIn = unsafeMkRowMorph gatherIdxs + , fpBaseScatter = unsafeMkRowMorph baseIdxs + , fpOpScatter = unsafeMkRowMorph opIdxs + } + +-- | Merges the previous frame @frameIn@ and the operation output @opOut@ +-- into the next frame @frameOut@ in two tight, branchless loops. +-- +-- See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring] +executeFrameScatter + :: FramePlan frameIn opIn opOut frameOut + -> Rep f a + -> Rep f b + -> Rep f c +{-# INLINE executeFrameScatter #-} +executeFrameScatter (FramePlan !outSz _ (RowMorph baseMap) (RowMorph opMap)) (Rep _ baseArr) (Rep _ opArr) = + Rep 0 $ runSmallArray $ do + let !baseLen = sizeofPrimArray baseMap + !opLen = sizeofPrimArray opMap + dst <- newSmallArray outSz (error "executeFrameScatter: uninitialized slot") + let copyBase !i + | i >= baseLen = pure () + | otherwise = do + let !dstIdx = indexPrimArray baseMap i + writeSmallArray dst dstIdx (indexSmallArray baseArr i) + copyBase (i + 1) + copyOp !j + | j >= opLen = pure dst + | otherwise = do + let !dstIdx = indexPrimArray opMap j + writeSmallArray dst dstIdx (indexSmallArray opArr j) + copyOp (j + 1) + copyBase 0 + copyOp 0 diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -27,6 +27,8 @@ import Control.Monad.ST (runST) import Data.Functor.Identity (Identity(..)) +import Data.Kind (Type) +import Data.Primitive.PrimArray (sizeofPrimArray) import Data.Primitive.SmallArray (indexSmallArray) import GHC.Exts (Any) import Test.Tasty (TestTree, defaultMain, testGroup) @@ -34,6 +36,7 @@ import Polytropos.Core import Polytropos +import Polytropos.RowMorph {------------------------------------------------------------------------------- Slot helpers @@ -424,6 +427,112 @@ unslot (fieldAt 9 res) @?= (290 :: Int) ] +rowMorphTests :: TestTree +rowMorphTests = testGroup "row-morph" + [ testCase "unsafeMkRowMorph and indexRowMorph round-trip" $ do + let m = unsafeMkRowMorph [2, 0, 1] :: RowMorph '[ "c" := Char, "a" := Int, "b" := Bool ] '[ "a" := Int, "b" := Bool, "c" := Char ] + sizeofPrimArray (unRowMorph m) @?= 3 + indexRowMorph m 0 @?= 2 + indexRowMorph m 1 @?= 0 + indexRowMorph m 2 @?= 1 + + , testCase "composeRowMorph fuses morphisms in O(|r1|)" $ do + let m12 = unsafeMkRowMorph [1, 0] :: RowMorph '[ "b" := Bool, "a" := Int ] '[ "a" := Int, "b" := Bool ] + m23 = unsafeMkRowMorph [2, 0] :: RowMorph '[ "a" := Int, "b" := Bool ] '[ "b" := Bool, "x" := Char, "a" := Int ] + m13 = composeRowMorph m12 m23 + sizeofPrimArray (unRowMorph m13) @?= 2 + indexRowMorph m13 0 @?= 0 + indexRowMorph m13 1 @?= 2 + + , testCase "gatherRep extracts sub-slots in specified order" $ do + let full = productRep [slot (10 :: Int), slot True, slot ("hello" :: String)] + m = unsafeMkRowMorph [2, 0] :: RowMorph '[ "c" := String, "a" := Int ] '[ "a" := Int, "b" := Bool, "c" := String ] + sub = gatherRep m full + repArity sub @?= 2 + unslot (fieldAt 0 sub) @?= ("hello" :: String) + unslot (fieldAt 1 sub) @?= (10 :: Int) + + , testCase "scatterRep overwrites sub-slots in existing rep" $ do + let full = productRep [slot (10 :: Int), slot True, slot ("hello" :: String)] + sub = productRep [slot (42 :: Int), slot ("world" :: String)] + m = unsafeMkRowMorph [0, 2] :: RowMorph '[ "a" := Int, "c" := String ] '[ "a" := Int, "b" := Bool, "c" := String ] + res = scatterRep m sub full + repArity res @?= 3 + unslot (fieldAt 0 res) @?= (42 :: Int) + unslot (fieldAt 1 res) @?= True + unslot (fieldAt 2 res) @?= ("world" :: String) + + , testCase "gatherRecord and scatterRecord over Record" $ do + let rFull = insertField (Field @"a") (10 :: Int) + $ insertField (Field @"b") True + $ insertField (Field @"c") ("polytropos" :: String) + $ emptyRecord + morph = unsafeMkRowMorph [1, 0] :: RowMorph '[ "b" := Bool, "a" := Int ] '[ "a" := Int, "b" := Bool, "c" := String ] + rSub = gatherRecord morph rFull + unslot (fieldAt 0 (unRowRep rSub)) @?= True + unslot (fieldAt 1 (unRowRep rSub)) @?= (10 :: Int) + let rSub' = insertField (Field @"b") False $ insertField (Field @"a") (99 :: Int) emptyRecord + rUpdated = scatterRecord morph rSub' rFull + unslot (fieldAt 0 (unRowRep rUpdated)) @?= (99 :: Int) + unslot (fieldAt 1 (unRowRep rUpdated)) @?= False + unslot (fieldAt 2 (unRowRep rUpdated)) @?= ("polytropos" :: String) + + , testCase "executeFrameScatter merges base frame and operation outputs" $ do + let frameIn = productRep [slot (1 :: Int), slot ("old" :: String)] + opOut = productRep [slot ("new" :: String)] + plan = unsafeMkFramePlan 2 [0] [0, 1] [1] :: FramePlan '[ "id" := Int, "status" := String ] '[ "id" := Int ] '[ "status" := String ] '[ "id" := Int, "status" := String ] + frameOut = executeFrameScatter plan frameIn opOut + repArity frameOut @?= 2 + unslot (fieldAt 0 frameOut) @?= (1 :: Int) + unslot (fieldAt 1 frameOut) @?= ("new" :: String) + + , testCase "executeFrameRecord merges base frame and operation outputs" $ do + let fIn = insertField (Field @"id") (1 :: Int) + $ insertField (Field @"status") ("old" :: String) + $ emptyRecord + opOut = insertField (Field @"status") ("new" :: String) + $ insertField (Field @"extra") True + $ emptyRecord + plan = unsafeMkFramePlan 3 [0] [0, 1] [1, 2] + :: FramePlan '[ "id" := Int, "status" := String ] + '[ "id" := Int ] + '[ "status" := String, "extra" := Bool ] + '[ "id" := Int, "status" := String, "extra" := Bool ] + fOut = executeFrameRecord plan fIn opOut + unslot (fieldAt 0 (unRowRep fOut)) @?= (1 :: Int) + unslot (fieldAt 1 (unRowRep fOut)) @?= ("new" :: String) + unslot (fieldAt 2 (unRowRep fOut)) @?= True + ] + +-- | Mock higher-kinded effect signatures for EffectRowOf testing. +type MockPolyEffect = RowOf Type -> RowOf (RowOf Type) -> Type +data MockStateEff (ins :: RowOf Type) (outs :: RowOf (RowOf Type)) +data MockLogEff (ins :: RowOf Type) (outs :: RowOf (RowOf Type)) + +type MockEffectRow = EffectRowOf MockPolyEffect +type MyCoreEf = '[ "state" := MockStateEff, "log" := MockLogEff ] :: MockEffectRow + +instance FieldIndex "state" MyCoreEf MockStateEff where + fieldIndex = 0 + +instance FieldIndex "log" MyCoreEf MockLogEff where + fieldIndex = 1 + +instance ConstructorIndex "state" MyCoreEf where + constructorIndex = 0 + +instance ConstructorIndex "log" MyCoreEf where + constructorIndex = 1 + +effectRowTests :: TestTree +effectRowTests = testGroup "poly-kinded effect rows" + [ testCase "FieldIndex and ConstructorIndex over EffectRowOf" $ do + fieldIndex @_ @"state" @MyCoreEf @MockStateEff @?= 0 + fieldIndex @_ @"log" @MyCoreEf @MockLogEff @?= 1 + constructorIndex @_ @"state" @MyCoreEf @?= 0 + constructorIndex @_ @"log" @MyCoreEf @?= 1 + ] + main :: IO () main = defaultMain $ testGroup "polytropos-core" [ productTests @@ -431,4 +540,6 @@ , evidenceTests , consumerTests , simdTests + , rowMorphTests + , effectRowTests ]