diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,14 @@ +# Changelog for penelope-core + +## 0.1.0.0 — Initial Release + +- Core polycategorical engine generalizing Heftia and Kernmantle. +- Unpacked `(m,n,k,r)`-ary polycategorical syntax GADT: `Polycategorical`. +- $O(1)$ jump-table route optimization via Polytropos row indexing. +- High-level smart constructors: `inject`, `fanout`, `assocL`, `assocR`, `swapSum`, `swapProd`, `distributeL`, `distributeR`. +- Sequential polycategorical composition (`composePoly`, `>>>`). +- Categorical frame rule wiring (`frame`, `cross`). +- Disjunctive polycategorical fanout (`fanoutDisj`). +- Row weakening and structural embedding (`weakenPoly`). +- Higher-order algebraic elaboration and vector interpretation engine. +- Partial interpretation substrate with structural residualization. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,189 @@ +EUROPEAN UNION PUBLIC LICENCE v. 1.2 +EUPL © the European Union 2007, 2016 + +This European Union Public Licence (the ‘EUPL’) applies to the Work (as defined below) which is provided under the +terms of this Licence. Any use of the Work, other than as authorised under this Licence is prohibited (to the extent such +use is covered by a right of the copyright holder of the Work). +The Work is provided under the terms of this Licence when the Licensor (as defined below) has placed the following +notice immediately following the copyright notice for the Work: + Licensed under the EUPL +or has expressed by any other means his willingness to license under the EUPL. + +1.Definitions +In this Licence, the following terms have the following meaning: +— ‘The Licence’:this Licence. +— ‘The Original Work’:the work or software distributed or communicated by the Licensor under this Licence, available +as Source Code and also as Executable Code as the case may be. +— ‘Derivative Works’:the works or software that could be created by the Licensee, based upon the Original Work or +modifications thereof. This Licence does not define the extent of modification or dependence on the Original Work +required in order to classify a work as a Derivative Work; this extent is determined by copyright law applicable in +the country mentioned in Article 15. +— ‘The Work’:the Original Work or its Derivative Works. +— ‘The Source Code’:the human-readable form of the Work which is the most convenient for people to study and +modify. +— ‘The Executable Code’:any code which has generally been compiled and which is meant to be interpreted by +a computer as a program. +— ‘The Licensor’:the natural or legal person that distributes or communicates the Work under the Licence. +— ‘Contributor(s)’:any natural or legal person who modifies the Work under the Licence, or otherwise contributes to +the creation of a Derivative Work. +— ‘The Licensee’ or ‘You’:any natural or legal person who makes any usage of the Work under the terms of the +Licence. +— ‘Distribution’ or ‘Communication’:any act of selling, giving, lending, renting, distributing, communicating, +transmitting, or otherwise making available, online or offline, copies of the Work or providing access to its essential +functionalities at the disposal of any other natural or legal person. + +2.Scope of the rights granted by the Licence +The Licensor hereby grants You a worldwide, royalty-free, non-exclusive, sublicensable licence to do the following, for +the duration of copyright vested in the Original Work: +— use the Work in any circumstance and for all usage, +— reproduce the Work, +— modify the Work, and make Derivative Works based upon the Work, +— communicate to the public, including the right to make available or display the Work or copies thereof to the public +and perform publicly, as the case may be, the Work, +— distribute the Work or copies thereof, +— lend and rent the Work or copies thereof, +— sublicense rights in the Work or copies thereof. +Those rights can be exercised on any media, supports and formats, whether now known or later invented, as far as the +applicable law permits so. +In the countries where moral rights apply, the Licensor waives his right to exercise his moral right to the extent allowed +by law in order to make effective the licence of the economic rights here above listed. +The Licensor grants to the Licensee royalty-free, non-exclusive usage rights to any patents held by the Licensor, to the +extent necessary to make use of the rights granted on the Work under this Licence. + +3.Communication of the Source Code +The Licensor may provide the Work either in its Source Code form, or as Executable Code. If the Work is provided as +Executable Code, the Licensor provides in addition a machine-readable copy of the Source Code of the Work along with +each copy of the Work that the Licensor distributes or indicates, in a notice following the copyright notice attached to +the Work, a repository where the Source Code is easily and freely accessible for as long as the Licensor continues to +distribute or communicate the Work. + +4.Limitations on copyright +Nothing in this Licence is intended to deprive the Licensee of the benefits from any exception or limitation to the +exclusive rights of the rights owners in the Work, of the exhaustion of those rights or of other applicable limitations +thereto. + +5.Obligations of the Licensee +The grant of the rights mentioned above is subject to some restrictions and obligations imposed on the Licensee. Those +obligations are the following: + +Attribution right: The Licensee shall keep intact all copyright, patent or trademarks notices and all notices that refer to +the Licence and to the disclaimer of warranties. The Licensee must include a copy of such notices and a copy of the +Licence with every copy of the Work he/she distributes or communicates. The Licensee must cause any Derivative Work +to carry prominent notices stating that the Work has been modified and the date of modification. + +Copyleft clause: If the Licensee distributes or communicates copies of the Original Works or Derivative Works, this +Distribution or Communication will be done under the terms of this Licence or of a later version of this Licence unless +the Original Work is expressly distributed only under this version of the Licence — for example by communicating +‘EUPL v. 1.2 only’. The Licensee (becoming Licensor) cannot offer or impose any additional terms or conditions on the +Work or Derivative Work that alter or restrict the terms of the Licence. + +Compatibility clause: If the Licensee Distributes or Communicates Derivative Works or copies thereof based upon both +the Work and another work licensed under a Compatible Licence, this Distribution or Communication can be done +under the terms of this Compatible Licence. For the sake of this clause, ‘Compatible Licence’ refers to the licences listed +in the appendix attached to this Licence. Should the Licensee's obligations under the Compatible Licence conflict with +his/her obligations under this Licence, the obligations of the Compatible Licence shall prevail. + +Provision of Source Code: When distributing or communicating copies of the Work, the Licensee will provide +a machine-readable copy of the Source Code or indicate a repository where this Source will be easily and freely available +for as long as the Licensee continues to distribute or communicate the Work. +Legal Protection: This Licence does not grant permission to use the trade names, trademarks, service marks, or names +of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and +reproducing the content of the copyright notice. + +6.Chain of Authorship +The original Licensor warrants that the copyright in the Original Work granted hereunder is owned by him/her or +licensed to him/her and that he/she has the power and authority to grant the Licence. +Each Contributor warrants that the copyright in the modifications he/she brings to the Work are owned by him/her or +licensed to him/her and that he/she has the power and authority to grant the Licence. +Each time You accept the Licence, the original Licensor and subsequent Contributors grant You a licence to their contributions +to the Work, under the terms of this Licence. + +7.Disclaimer of Warranty +The Work is a work in progress, which is continuously improved by numerous Contributors. It is not a finished work +and may therefore contain defects or ‘bugs’ inherent to this type of development. +For the above reason, the Work is provided under the Licence on an ‘as is’ basis and without warranties of any kind +concerning the Work, including without limitation merchantability, fitness for a particular purpose, absence of defects or +errors, accuracy, non-infringement of intellectual property rights other than copyright as stated in Article 6 of this +Licence. +This disclaimer of warranty is an essential part of the Licence and a condition for the grant of any rights to the Work. + +8.Disclaimer of Liability +Except in the cases of wilful misconduct or damages directly caused to natural persons, the Licensor will in no event be +liable for any direct or indirect, material or moral, damages of any kind, arising out of the Licence or of the use of the +Work, including without limitation, damages for loss of goodwill, work stoppage, computer failure or malfunction, loss +of data or any commercial damage, even if the Licensor has been advised of the possibility of such damage. However, +the Licensor will be liable under statutory product liability laws as far such laws apply to the Work. + +9.Additional agreements +While distributing the Work, You may choose to conclude an additional agreement, defining obligations or services +consistent with this Licence. However, if accepting obligations, You may act only on your own behalf and on your sole +responsibility, not on behalf of the original Licensor or any other Contributor, and only if You agree to indemnify, +defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against such Contributor by +the fact You have accepted any warranty or additional liability. + +10.Acceptance of the Licence +The provisions of this Licence can be accepted by clicking on an icon ‘I agree’ placed under the bottom of a window +displaying the text of this Licence or by affirming consent in any other similar way, in accordance with the rules of +applicable law. Clicking on that icon indicates your clear and irrevocable acceptance of this Licence and all of its terms +and conditions. +Similarly, you irrevocably accept this Licence and all of its terms and conditions by exercising any rights granted to You +by Article 2 of this Licence, such as the use of the Work, the creation by You of a Derivative Work or the Distribution +or Communication by You of the Work or copies thereof. + +11.Information to the public +In case of any Distribution or Communication of the Work by means of electronic communication by You (for example, +by offering to download the Work from a remote location) the distribution channel or media (for example, a website) +must at least provide to the public the information requested by the applicable law regarding the Licensor, the Licence +and the way it may be accessible, concluded, stored and reproduced by the Licensee. + +12.Termination of the Licence +The Licence and the rights granted hereunder will terminate automatically upon any breach by the Licensee of the terms +of the Licence. +Such a termination will not terminate the licences of any person who has received the Work from the Licensee under +the Licence, provided such persons remain in full compliance with the Licence. + +13.Miscellaneous +Without prejudice of Article 9 above, the Licence represents the complete agreement between the Parties as to the +Work. +If any provision of the Licence is invalid or unenforceable under applicable law, this will not affect the validity or +enforceability of the Licence as a whole. Such provision will be construed or reformed so as necessary to make it valid +and enforceable. +The European Commission may publish other linguistic versions or new versions of this Licence or updated versions of +the Appendix, so far this is required and reasonable, without reducing the scope of the rights granted by the Licence. +New versions of the Licence will be published with a unique version number. +All linguistic versions of this Licence, approved by the European Commission, have identical value. Parties can take +advantage of the linguistic version of their choice. + +14.Jurisdiction +Without prejudice to specific agreement between parties, +— any litigation resulting from the interpretation of this License, arising between the European Union institutions, +bodies, offices or agencies, as a Licensor, and any Licensee, will be subject to the jurisdiction of the Court of Justice +of the European Union, as laid down in article 272 of the Treaty on the Functioning of the European Union, +— any litigation arising between other parties and resulting from the interpretation of this License, will be subject to +the exclusive jurisdiction of the competent court where the Licensor resides or conducts its primary business. + +15.Applicable Law +Without prejudice to specific agreement between parties, +— this Licence shall be governed by the law of the European Union Member State where the Licensor has his seat, +resides or has his registered office, +— this licence shall be governed by Belgian law if the Licensor has no seat, residence or registered office inside +a European Union Member State. + +Appendix + +‘Compatible Licences’ according to Article 5 EUPL are: +— GNU General Public License (GPL) v. 2, v. 3 +— GNU Affero General Public License (AGPL) v. 3 +— Open Software License (OSL) v. 2.1, v. 3.0 +— Eclipse Public License (EPL) v. 1.0 +— CeCILL v. 2.0, v. 2.1 +— Mozilla Public Licence (MPL) v. 2 +— GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3 +— Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for works other than software +— European Union Public Licence (EUPL) v. 1.1, v. 1.2 +— Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong Reciprocity (LiLiQ-R+). + +The European Commission may update this Appendix to later versions of the above licences without producing +a new version of the EUPL, as long as they provide the rights granted in Article 2 of this Licence and protect the +covered Source Code from exclusive appropriation. +All other changes or additions to this Appendix require the production of a new EUPL version. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,10 @@ +# penelope-core + +Domain package for penelope-core + +## Modules + + +## License + +EUPL-1.2 diff --git a/penelope-core.cabal b/penelope-core.cabal new file mode 100644 --- /dev/null +++ b/penelope-core.cabal @@ -0,0 +1,121 @@ +cabal-version: 3.0 +name: penelope-core +version: 0.1.0.0 +synopsis: Unpacked (m,n,k,r)-ary Polycategorical Effect System Core +description: + Core polycategorical effect engine generalizing Heftia and Kernmantle. + Provides the unpacked (m,n,k,r)-ary polycategorical syntax GADT, + O(1) jump-table route optimization via Polytropos row indexing, + categorical frame rule wiring, disjunctive fanout, row weakening, + higher-order algebraic elaboration, and vector interpretation. +license: EUPL-1.2 +license-file: LICENSE +author: Nadia Yvette Chambers +maintainer: nadia.yvette.chambers@ik.me +category: Control +homepage: https://github.com/NadiaYvette/penelope +bug-reports: https://github.com/NadiaYvette/penelope/issues +extra-doc-files: + README.md + CHANGELOG.md +build-type: Simple +tested-with: GHC == 9.14.1 + +source-repository head + type: git + location: https://github.com/NadiaYvette/penelope + subdir: packages/penelope-core + +library + exposed-modules: + Penelope.Core + Penelope.Core.Syntax + Penelope.Core.Route + Penelope.Core.Send + Penelope.Core.Wiring + Penelope.Core.Engine + Penelope.Core.Engine.Elaborate + Penelope.Core.Engine.Interpret + Penelope.Core.Engine.Partial + hs-source-dirs: src + default-language: Haskell2010 + default-extensions: + AllowAmbiguousTypes + BangPatterns + DataKinds + DerivingStrategies + FlexibleContexts + FlexibleInstances + GADTs + KindSignatures + MagicHash + MultiParamTypeClasses + OverloadedStrings + PolyKinds + RankNTypes + ScopedTypeVariables + TypeApplications + TypeFamilies + TypeOperators + UnboxedTuples + ghc-options: -Wall -Wcompat -Wredundant-constraints + build-depends: + base >= 4.14 && < 5, + text >= 2.0 && < 2.2, + containers >= 0.6 && < 0.9, + primitive >= 0.9 && < 0.10, + polytropos-core >= 0.1 && < 0.2, + polytropos-plugin >= 0.1 && < 0.2 + +test-suite tests + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + default-language: Haskell2010 + default-extensions: + AllowAmbiguousTypes + DataKinds + GADTs + MagicHash + OverloadedStrings + PolyKinds + RankNTypes + TypeApplications + TypeOperators + ghc-options: -Wall -Wcompat -Wredundant-constraints -threaded -rtsopts + build-depends: + base >= 4.14 && < 5, + hspec >= 2.11 && < 2.12, + text >= 2.0 && < 2.2, + primitive >= 0.9 && < 0.10, + penelope-core, + polytropos-core >= 0.1 && < 0.2, + polytropos-plugin >= 0.1 && < 0.2 + +test-suite inspection + type: exitcode-stdio-1.0 + main-is: Inspection.hs + hs-source-dirs: test + default-language: Haskell2010 + default-extensions: + AllowAmbiguousTypes + DataKinds + GADTs + MagicHash + OverloadedStrings + PolyKinds + RankNTypes + ScopedTypeVariables + TemplateHaskell + TypeApplications + TypeFamilies + TypeOperators + ghc-options: -Wall -Wcompat -Wredundant-constraints -threaded -rtsopts + build-depends: + base >= 4.14 && < 5, + hspec >= 2.11 && < 2.12, + inspection-testing >= 0.5 && < 0.7, + primitive >= 0.9 && < 0.10, + penelope-core, + polytropos-core >= 0.1 && < 0.2, + polytropos-plugin >= 0.1 && < 0.2 diff --git a/src/Penelope/Core.hs b/src/Penelope/Core.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core.hs @@ -0,0 +1,25 @@ +{- | +Module : Penelope.Core +Description : High-level re-export facade for penelope-core +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Foundational exports for Penelope core polycategorical effect engine. +See Note [Core Architecture] [ref:note-core-architecture]. +-} +module Penelope.Core + ( module Penelope.Core.Syntax + , module Penelope.Core.Route + , module Penelope.Core.Send + , module Penelope.Core.Wiring + , module Penelope.Core.Engine + ) where + +import Penelope.Core.Syntax +import Penelope.Core.Route +import Penelope.Core.Send +import Penelope.Core.Wiring +import Penelope.Core.Engine diff --git a/src/Penelope/Core/Engine.hs b/src/Penelope/Core/Engine.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Engine.hs @@ -0,0 +1,21 @@ +{- | +Module : Penelope.Core.Engine +Description : High-level re-export facade for Penelope execution engine +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Provides execution engines for Penelope: Phase 1 elaboration, Phase 2 interpretation, and partial peeling. +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +module Penelope.Core.Engine + ( module Penelope.Core.Engine.Elaborate + , module Penelope.Core.Engine.Interpret + , module Penelope.Core.Engine.Partial + ) where + +import Penelope.Core.Engine.Elaborate +import Penelope.Core.Engine.Interpret +import Penelope.Core.Engine.Partial diff --git a/src/Penelope/Core/Engine/Elaborate.hs b/src/Penelope/Core/Engine/Elaborate.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Engine/Elaborate.hs @@ -0,0 +1,142 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +{- | +Module : Penelope.Core.Engine.Elaborate +Description : Phase 1 single-pass bottom-up higher-order effect elaboration +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Provides Phase 1 single-pass bottom-up macro elaboration of higher-order scoped +effects into pure first-order operations. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and +Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +module Penelope.Core.Engine.Elaborate + ( -- * Elaborator Abstraction + Elaborator (..) + , Elaborators + , MapRow + + -- * Phase 1 Elaboration Engine + , elaborateAll + ) where + +import Data.Functor.Identity (Identity (..)) +import Data.Kind (Type) +import Data.Primitive.SmallArray (indexSmallArray) +import GHC.Exts (Any, Int (..), unsafeCoerce#, word2Int#) +import Penelope.Core.Syntax + ( BranchCont (..) + , Penelope (..) + , PolyEffect + , PolyHEffect + , Region (..) + ) +import Penelope.Core.Wiring (rmapFused) +import Polytropos (Pair (..), Record, RowOf, gatherRecord) +import Polytropos.Core (Rep (..), RowRep (..)) +import Polytropos.RowMorph (RowMorph, unsafeMkRowMorph) + +-- | Map a higher-order type constructor over each field of a row. +type family MapRow (f :: k -> Type) (r :: RowOf k) :: RowOf Type where + MapRow f '[] = '[] + MapRow f ((l ':= v) ': rest) = (l ':= f v) ': MapRow f rest + +-- | Convenient type alias for a record of elaborators. +type Elaborators ef eh = Record (MapRow (Elaborator '[] ef) eh) + +{- | +An 'Elaborator' translates a higher-order \((m, n, k, r)\)-ary scoped operation @h@ +into a pure first-order 'Penelope' computation. + +Notice that: +1. All \(r\) nested regions in @Record regions@ have ALREADY + been recursively elaborated before 'runElaborator' is called (bottom-up catamorphism). +2. The elaborator receives the \(k\) downstream continuation branches + @Record exits@ directly, allowing it to wire region exits straight into downstream + branches without intermediate ADT allocations. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +newtype Elaborator + (eh' :: RowOf PolyHEffect) + (ef :: RowOf PolyEffect) + (h :: PolyHEffect) + = Elaborator + { runElaborator + :: forall (regions :: RowOf Type) (opIns :: RowOf Type) (exits :: RowOf Type) + (frameIns :: RowOf Type) (frameOuts :: RowOf Type). + RowMorph opIns frameIns + -> Record regions + -> Any + -> Record exits + -> Penelope eh' ef frameIns frameOuts + } + +{- | +Elaborates all higher-order scoped effects @eh@ into pure first-order effects @ef@ +in a single bottom-up pass over the syntax tree. +Dispatch at each 'OpH' node is a branchless \(O(1)\) 'indexSmallArray#' read into the +Polytropos 'Record' of elaborators. + +Contravariant reduct gathering via 'gatherRecord' adapts outer elaborators to inner +scopes across 'ScopeRow' boundaries in \(O(|eh_{sub}|)\) time without walking the inner sub-tree. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and +Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +{-# INLINE elaborateAll #-} +elaborateAll :: + forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) + (ins :: RowOf Type) (outs :: RowOf Type). + Record (MapRow (Elaborator '[] ef) eh) + -> Penelope eh ef ins outs + -> Penelope '[] ef ins outs +elaborateAll !elabs = go + where + elabCont :: + BranchCont (Penelope eh ef i o) branchOuts + -> BranchCont (Penelope '[] ef i o) branchOuts + elabCont (BranchCont k) = BranchCont (\branchFrame -> go (k branchFrame)) + + elabRegion :: Region eh ef sig -> Region '[] ef sig + elabRegion (Region subPipe) = Region (elaborateAll elabs subPipe) + + go :: Penelope eh ef i o -> Penelope '[] ef i o + go = \case + Route morph -> + Route morph + + LiftPure inMap f cont -> + LiftPure inMap f (elabCont cont) + + OpF tag# inMap opAny conts -> + OpF tag# inMap opAny (rmapFused elabCont conts) + + OpH tag# inMap regions opAny conts -> + let !elaboratedRegions = rmapFused elabRegion regions + !elaboratedConts = rmapFused elabCont conts + !(RowRep (Rep _ arr)) = elabs + !(Identity elabAny) = indexSmallArray arr (I# (word2Int# tag#)) + !(Elaborator elabFn) = unsafeCoerce# elabAny + in elabFn (unsafeCoerce# inMap) elaboratedRegions opAny elaboratedConts + + ScopeRow ehMorph efMorph subPipe -> + let !subElabs = unsafeCoerce# (gatherRecord (unsafeCoerce# ehMorph) elabs) + in ScopeRow (unsafeMkRowMorph []) efMorph (elaborateAll subElabs subPipe) diff --git a/src/Penelope/Core/Engine/Interpret.hs b/src/Penelope/Core/Engine/Interpret.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Engine/Interpret.hs @@ -0,0 +1,187 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +{- | +Module : Penelope.Core.Engine.Interpret +Description : Phase 2 bulk vector-dispatched algebraic interpretation +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Provides Phase 2 bulk vector-dispatched algebraic interpretation over first-order operations. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and +Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +module Penelope.Core.Engine.Interpret + ( -- * Carrier Abstraction + PolyCarrier (..) + , FrameKleisli (..) + + -- * Handler Abstraction + , Handler (..) + , Handlers + + -- * Phase 2 Interpretation Engine + , interpretAll + , runPenelopePure + ) where + +import Control.Category (Category (..)) +import Data.Functor.Identity (Identity (..)) +import Data.Kind (Type) +import Data.Primitive.SmallArray (indexSmallArray) +import GHC.Exts (Any, Int (..), unsafeCoerce#, word2Int#) +import Penelope.Core.Engine.Elaborate (MapRow) +import Penelope.Core.Syntax + ( BranchCont (..) + , Penelope (..) + , PolyEffect + ) +import Penelope.Core.Wiring (rmapFused) +import Polytropos (Record, RowOf, emptyRecord, gatherRecord) +import Polytropos.Core (Rep (..), RowRep (..)) +import Polytropos.RowMorph (RowMorph, gatherRep) +import Prelude hiding (id, (.)) + +{- | +Typeclass for target semantic carriers \(m :: RowOf Type -> RowOf Type -> Type\) +that can execute compiled first-order 'Penelope' graphs. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +class Category m => PolyCarrier m where + -- | Execute a pure static 'RowMorph' port permutation or projection. + evalRoute :: RowMorph outs ins -> m ins outs + + -- | Execute a pure step over a gathered subset of ports and feed outputs to continuation. + evalLiftPure :: + RowMorph opIns ins + -> (Record opIns -> Record opOuts) + -> (Record opOuts -> m ins outs) + -> m ins outs + +{- | +Standard in-memory frame execution carrier: a Kleisli arrow over flat 'Record' frames. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +newtype FrameKleisli (f :: Type -> Type) (ins :: RowOf Type) (outs :: RowOf Type) = FrameKleisli + { runFrameKleisli :: Record ins -> f (Record outs) + } + +instance Monad f => Category (FrameKleisli f) where + id = FrameKleisli pure + FrameKleisli g . FrameKleisli h = FrameKleisli (\r -> h r >>= g) + +instance Monad f => PolyCarrier (FrameKleisli f) where + {-# INLINE evalRoute #-} + evalRoute morph = FrameKleisli $ \(RowRep rep) -> + pure (RowRep (gatherRep morph rep)) + + {-# INLINE evalLiftPure #-} + evalLiftPure inMap f k = FrameKleisli $ \(RowRep inRep) -> do + let !opInFrame = RowRep (gatherRep inMap inRep) + !opOutFrame = f opInFrame + runFrameKleisli (k opOutFrame) (unsafeCoerce# opOutFrame) + +{- | +A first-order \((m, n, k)\)-ary effect handler into target carrier @m@. +Receives: +1. 'RowMorph opIns frameIns': Static map to extract the operation's \(m\) input ports. +2. 'Any': Dynamic payload of the first-order operation. +3. 'Record exits': Downstream continuation branches already interpreted into carrier @m@. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +newtype Handler + (ef :: RowOf PolyEffect) + (m :: RowOf Type -> RowOf Type -> Type) + (e :: PolyEffect) + = Handler + { runHandler + :: forall (opIns :: RowOf Type) (exits :: RowOf Type) + (frameIns :: RowOf Type) (frameOuts :: RowOf Type). + RowMorph opIns frameIns + -> Any + -> Record exits + -> m frameIns frameOuts + } + +-- | Convenient type alias for a record of first-order handlers. +type Handlers ef m = Record (MapRow (Handler '[] m) ef) + +{- | +Phase 2 bulk vector-dispatched algebraic interpretation over first-order operations. +Dispatches each 'OpF' constructor tag via branchless \(O(1)\) 'indexSmallArray#' read +into the handler record, with zero linear search cascades. + +Contravariant handler reduct gathering via 'gatherRecord' adapts outer handlers to inner +scopes across 'ScopeRow' boundaries in \(O(|ef_{sub}|)\) time without walking the inner sub-tree. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and +Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +{-# INLINE interpretAll #-} +interpretAll :: + forall (ef :: RowOf PolyEffect) m (ins :: RowOf Type) (outs :: RowOf Type). + PolyCarrier m => + Record (MapRow (Handler '[] m) ef) + -> Penelope '[] ef ins outs + -> m ins outs +interpretAll !handlers = go + where + interpCont :: + BranchCont (Penelope '[] ef i o) branchOuts + -> BranchCont (m i o) branchOuts + interpCont (BranchCont k) = BranchCont (\branchFrame -> go (k branchFrame)) + + go :: Penelope '[] ef i o -> m i o + go = \case + Route morph -> + evalRoute morph + + LiftPure inMap f (BranchCont k) -> + evalLiftPure inMap f (\opOutFrame -> go (k opOutFrame)) + + OpF tag# inMap opAny conts -> + let !interpretedConts = rmapFused interpCont conts + !(RowRep (Rep _ arr)) = handlers + !(Identity handlerAny) = indexSmallArray arr (I# (word2Int# tag#)) + !(Handler handleFn) = unsafeCoerce# handlerAny + in handleFn (unsafeCoerce# inMap) opAny interpretedConts + + ScopeRow _ehMorph efMorph subPipe -> + let !subHandlers = unsafeCoerce# (gatherRecord (unsafeCoerce# efMorph) handlers) + in interpretAll subHandlers (unsafeCoerce# subPipe) + + OpH {} -> + errorWithoutStackTrace "Penelope.Core.Engine.Interpret: impossible OpH in empty '[] higher-order row" + +{- | +Run a fully handled pure 'Penelope' pipeline over an initial register frame. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +{-# INLINE runPenelopePure #-} +runPenelopePure :: + Penelope '[] '[] ins outs + -> Record ins + -> Record outs +runPenelopePure pipe inFrame = + case runFrameKleisli (interpretAll emptyRecord pipe) inFrame of + Identity outFrame -> outFrame diff --git a/src/Penelope/Core/Engine/Partial.hs b/src/Penelope/Core/Engine/Partial.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Engine/Partial.hs @@ -0,0 +1,211 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{- | +Module : Penelope.Core.Engine.Partial +Description : Layered effect peeling and partial interpretation +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Provides partial effect peeling ('interpretSub'), lowering a subset of first-order +operations ('efSub') while leaving residual unhandled effects ('efRem') intact in the syntax tree. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +module Penelope.Core.Engine.Partial + ( -- * Compile-Time Row Partitioning + RowPartition (..) + , PartitionPlan (..) + , mkPartitionPlan + + -- * Partial Interpretation Engine + , interpretSub + ) where + +import Control.Monad.ST (runST) +import Data.Functor.Identity (Identity (..)) +import Data.Kind (Type) +import Data.Primitive.PrimArray + ( PrimArray + , indexPrimArray + , newPrimArray + , sizeofPrimArray + , unsafeFreezePrimArray + , writePrimArray + ) +import Data.Primitive.SmallArray (indexSmallArray) +import GHC.Exts (Int (..), int2Word#, unsafeCoerce#, word2Int#) +import Penelope.Core.Engine.Elaborate (MapRow) +import Penelope.Core.Engine.Interpret (Handler (..)) +import Penelope.Core.Syntax + ( BranchCont (..) + , Penelope (..) + , PolyEffect + ) +import Penelope.Core.Wiring (rmapFused) +import Polytropos (Record, RowOf) +import Polytropos.Core (Rep (..), RowRep (..)) +import Polytropos.RowMorph (KnownRowMorph (..), RowMorph (..), composeRowMorph, indexRowMorph) + +{- | +Runtime partition plan capturing the static decomposition of row @full@ into +disjoint sub-rows @sub@ and @rem@. +The 'ppLookup' unboxed array maps each constructor tag @fullIdx@ to: +* @val >= 0@: 0-based index in @sub@. +* @val < 0@: 0-based index in @rem@ (encoded as @-1 - val@). + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +data PartitionPlan (sub :: RowOf k) (rem :: RowOf k) (full :: RowOf k) = PartitionPlan + { ppSubMorph :: !(RowMorph sub full) + , ppRemMorph :: !(RowMorph rem full) + , ppLookup :: !(PrimArray Int) + } + +-- | Synthesizes an unboxed lookup array from compile-time row morphisms. +{-# INLINE mkPartitionPlan #-} +mkPartitionPlan :: + RowMorph sub full + -> RowMorph rem full + -> PartitionPlan sub rem full +mkPartitionPlan mSub@(RowMorph arrSub) mRem@(RowMorph arrRem) = + let !nSub = sizeofPrimArray arrSub + !nRem = sizeofPrimArray arrRem + !totalSz = nSub + nRem + !lookupArr = runST $ do + m <- newPrimArray totalSz + let initLoop !i + | i >= totalSz = pure () + | otherwise = writePrimArray m i (-1) >> initLoop (i + 1) + initLoop 0 + let fillSub !k + | k >= nSub = pure () + | otherwise = do + let !fullIdx = indexPrimArray arrSub k + writePrimArray m fullIdx k + fillSub (k + 1) + fillSub 0 + let fillRem !j + | j >= nRem = pure () + | otherwise = do + let !fullIdx = indexPrimArray arrRem j + writePrimArray m fullIdx (-1 - j) + fillRem (j + 1) + fillRem 0 + unsafeFreezePrimArray m + in PartitionPlan mSub mRem lookupArr + +{- | +Evidence that row @full@ is partitioned into disjoint sub-rows @sub@ and @rem@. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +class (KnownRowMorph sub full, KnownRowMorph rem full) => RowPartition (sub :: RowOf k) (rem :: RowOf k) (full :: RowOf k) where + rowPartition :: PartitionPlan sub rem full + +instance {-# OVERLAPPABLE #-} (KnownRowMorph sub full, KnownRowMorph rem full) => RowPartition sub rem full where + {-# INLINE rowPartition #-} + rowPartition = mkPartitionPlan (rowMorph @sub @full) (rowMorph @rem @full) + +{- | +Partially peel and interpret a subset of first-order effects @efSub@ from @efFull@, +leaving residual effects @efRem@ intact in the syntax tree. + +Dispatches each target effect via \(O(1)\) unboxed lookup in the partition table, +invoking the provided handler, while re-tagging unhandled residual operations to @efRem@. + +See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine]. +-} +{-# INLINE interpretSub #-} +interpretSub :: + forall (efSub :: RowOf PolyEffect) (efRem :: RowOf PolyEffect) (efFull :: RowOf PolyEffect) + (ins :: RowOf Type) (outs :: RowOf Type). + RowPartition efSub efRem efFull => + Record (MapRow (Handler efRem (Penelope '[] efRem)) efSub) + -> Penelope '[] efFull ins outs + -> Penelope '[] efRem ins outs +interpretSub !handlers = go + where + plan = rowPartition @_ @efSub @efRem @efFull + arrLookup = ppLookup plan + + interpCont :: + BranchCont (Penelope '[] efFull i o) branchOuts + -> BranchCont (Penelope '[] efRem i o) branchOuts + interpCont (BranchCont k) = BranchCont (\branchFrame -> go (k branchFrame)) + + go :: Penelope '[] efFull i o -> Penelope '[] efRem i o + go = \case + Route morph -> + Route morph + + LiftPure inMap f cont -> + LiftPure inMap f (interpCont cont) + + OpF tag# inMap opAny conts -> + let !idx = I# (word2Int# tag#) + !entry = indexPrimArray arrLookup idx + !interpretedConts = rmapFused interpCont conts + in if entry >= 0 + then + let !(RowRep (Rep _ arr)) = handlers + !(Identity handlerAny) = indexSmallArray arr entry + !(Handler handleFn) = unsafeCoerce# handlerAny + in handleFn (unsafeCoerce# inMap) opAny interpretedConts + else + let !(I# i#) = -1 - entry + !remIdx# = int2Word# i# + in OpF remIdx# inMap opAny interpretedConts + + ScopeRow _ehMorph efMorph subPipe -> + goInScope (unsafeCoerce# efMorph) (unsafeCoerce# subPipe) + + OpH {} -> + errorWithoutStackTrace "Penelope.Core.Engine.Partial: impossible OpH in empty '[] higher-order row" + + goInScope :: RowMorph efInner efFull -> Penelope '[] efInner i o -> Penelope '[] efRem i o + goInScope !efM = \case + Route morph -> + Route morph + + LiftPure inMap f (BranchCont k) -> + LiftPure inMap f (BranchCont (\branchFrame -> goInScope efM (k branchFrame))) + + OpF tag# inMap opAny conts -> + let !idx = indexRowMorph efM (I# (word2Int# tag#)) + !entry = indexPrimArray arrLookup idx + !interpretedConts = rmapFused (\(BranchCont k) -> BranchCont (\branchFrame -> goInScope efM (k branchFrame))) conts + in if entry >= 0 + then + let !(RowRep (Rep _ arr)) = handlers + !(Identity handlerAny) = indexSmallArray arr entry + !(Handler handleFn) = unsafeCoerce# handlerAny + in handleFn (unsafeCoerce# inMap) opAny interpretedConts + else + let !(I# i#) = -1 - entry + !remIdx# = int2Word# i# + in OpF remIdx# inMap opAny interpretedConts + + ScopeRow _ehInner efMorph2 inner -> + goInScope (composeRowMorph (unsafeCoerce# efMorph2) efM) (unsafeCoerce# inner) + + OpH {} -> + errorWithoutStackTrace "Penelope.Core.Engine.Partial: impossible OpH in empty '[] higher-order row" diff --git a/src/Penelope/Core/Route.hs b/src/Penelope/Core/Route.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Route.hs @@ -0,0 +1,93 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} + +{- | +Module : Penelope.Core.Route +Description : Pure port routing, identity elision, and route peephole optimization +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +This module provides smart constructors and fusion routines for pure port wire +permutations over Polytropos 'RowMorph' structures. + +See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing]. +-} +module Penelope.Core.Route + ( -- * Smart Constructors + route + , routeExplicit + + -- * Route Optimization & Fusion + , fuseRoute + , isIdentityRowMorph + , isIdentityRoute + ) where + +import Data.Kind (Type) +import Data.Primitive.PrimArray (indexPrimArray, sizeofPrimArray) +import Penelope.Core.Syntax (Penelope (..), PolyEffect, PolyHEffect) +import Polytropos (RowOf) +import Polytropos.RowMorph + ( KnownRowMorph (..) + , RowMorph (..) + , composeRowMorph + ) + +{- | +Construct a pure wire permutation between input ports and output ports using +a compile-time synthesized 'RowMorph' solved by @Polytropos.Plugin@. + +See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing]. +-} +route :: + forall {eh :: RowOf PolyHEffect} {ef :: RowOf PolyEffect} (ins :: RowOf Type) (outs :: RowOf Type). + KnownRowMorph outs ins => + Penelope eh ef ins outs +{-# INLINE route #-} +route = Route (rowMorph @outs @ins) + +-- | Construct a pure wire permutation with an explicit 'RowMorph'. +routeExplicit :: + forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (ins :: RowOf Type) (outs :: RowOf Type). + RowMorph outs ins + -> Penelope eh ef ins outs +{-# INLINE routeExplicit #-} +routeExplicit = Route + +{- | +Fuse two consecutive pure route stages in \(O(|outs|)\) time with zero intermediate allocations. +Given a route from @a@ to @b@ ('RowMorph' @b@ @a@) and a route from @b@ to @c@ ('RowMorph' @c@ @b@), +computes the composite route from @a@ to @c@ ('RowMorph' @c@ @a@). +-} +fuseRoute :: + RowMorph b a + -> RowMorph c b + -> RowMorph c a +{-# INLINE fuseRoute #-} +fuseRoute m1 m2 = composeRowMorph m2 m1 + +{- | +Check whether a 'RowMorph' represents the identity permutation (slot @i@ maps to @i@). +-} +isIdentityRowMorph :: RowMorph r1 r2 -> Bool +{-# INLINE isIdentityRowMorph #-} +isIdentityRowMorph (RowMorph arr) = + let !n = sizeofPrimArray arr + go !i + | i >= n = True + | otherwise = indexPrimArray arr i == i && go (i + 1) + in go 0 + +{- | +Check whether a 'Penelope' computation is an identity wire permutation. +-} +isIdentityRoute :: Penelope eh ef ins outs -> Bool +isIdentityRoute (Route m) = isIdentityRowMorph m +isIdentityRoute _ = False diff --git a/src/Penelope/Core/Send.hs b/src/Penelope/Core/Send.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Send.hs @@ -0,0 +1,97 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +{- | +Module : Penelope.Core.Send +Description : Zero-overhead smart constructors for first-order and higher-order effect operations +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +This module provides zero-overhead smart constructors ('sendPolyF', 'sendPolyH') +injecting algebraic effect operations into the 'Penelope' polycategorical core. + +See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +module Penelope.Core.Send + ( -- * Smart Constructors + sendPolyF + , sendPolyF' + , sendPolyH + , sendPolyH' + ) where + +import Data.Kind (Type) +import GHC.Exts (Any, Word (W#), unsafeCoerce#) +import GHC.TypeLits (Symbol) +import Penelope.Core.Syntax (Penelope (..), PolyEffect, PolyHEffect) +import Polytropos (Record, RowOf) +import Polytropos.Core (ConstructorIndex (..), Row) +import Polytropos.RowMorph (KnownRowMorph (..)) + +{- | +Inject a first-order algebraic operation into the syntax tree. +Looks up the constructor tag via 'ConstructorIndex' solved at compile time by @Polytropos.Plugin@, +and wires input ports via 'KnownRowMorph'. + +See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +sendPolyF :: + forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (exits :: Row) (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type). + (ConstructorIndex l ef, KnownRowMorph opIns ins) => + Any + -> Record exits + -> Penelope eh ef ins outs +{-# INLINE sendPolyF #-} +sendPolyF payload conts = + case constructorIndex @_ @l @ef of + W# tag# -> OpF tag# (rowMorph @opIns @ins) payload conts + +-- | Typed payload variant of 'sendPolyF' applying 'unsafeCoerce#' without runtime boxing. +sendPolyF' :: + forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (exits :: Row) op (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type). + (ConstructorIndex l ef, KnownRowMorph opIns ins) => + op + -> Record exits + -> Penelope eh ef ins outs +{-# INLINE sendPolyF' #-} +sendPolyF' op conts = sendPolyF @l @opIns (unsafeCoerce# op) conts + +{- | +Inject a higher-order scoped algebraic operation into the syntax tree with +explicit sub-regions and multi-exit branch continuations. + +See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +sendPolyH :: + forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (regions :: Row) (exits :: Row) (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type). + (ConstructorIndex l eh, KnownRowMorph opIns ins) => + Record regions + -> Any + -> Record exits + -> Penelope eh ef ins outs +{-# INLINE sendPolyH #-} +sendPolyH regions payload conts = + case constructorIndex @_ @l @eh of + W# tag# -> OpH tag# (rowMorph @opIns @ins) regions payload conts + +-- | Typed payload variant of 'sendPolyH' applying 'unsafeCoerce#' without runtime boxing. +sendPolyH' :: + forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (regions :: Row) (exits :: Row) op (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type). + (ConstructorIndex l eh, KnownRowMorph opIns ins) => + Record regions + -> op + -> Record exits + -> Penelope eh ef ins outs +{-# INLINE sendPolyH' #-} +sendPolyH' regions op conts = sendPolyH @l @opIns regions (unsafeCoerce# op) conts diff --git a/src/Penelope/Core/Syntax.hs b/src/Penelope/Core/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Syntax.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} + +{- | +Module : Penelope.Core.Syntax +Description : Foundational (m,n,k,r)-ary polycategorical syntax GADT and type-level signatures +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +This module implements the foundational syntax GADT for Penelope's +$(m,n,k,r)$-ary polycategorical effect engine. + +See Note [Core Architecture] [ref:note-core-architecture] and +Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +module Penelope.Core.Syntax + ( -- * Type-Level Signatures + PortSig (..) + , RegionIns + , RegionOuts + , PolyEffect + , PolyHEffect + + -- * Continuations and Scoped Regions + , BranchCont (..) + , Region (..) + + -- * Core Syntax GADT + , Penelope (..) + ) where + +import Data.Kind (Type) +import GHC.Exts (Any, Word#) +import Polytropos (Record, RowOf) +import Polytropos.RowMorph (RowMorph) + +{- | +Polycategorical port signature encoding input ports and output ports. +Used as the sort for higher-order scoped sub-regions. +-} +data PortSig = PortSig (RowOf Type) (RowOf Type) + +-- | Extract the input port row from a 'PortSig'. +type family RegionIns (sig :: PortSig) :: RowOf Type where + RegionIns ('PortSig ins _) = ins + +-- | Extract the output port row from a 'PortSig'. +type family RegionOuts (sig :: PortSig) :: RowOf Type where + RegionOuts ('PortSig _ outs) = outs + +{- | +Signature of a first-order polycategorical effect operation. +Takes an input argument row and a row of disjunctive exit rows. +-} +type PolyEffect = RowOf Type -> RowOf (RowOf Type) -> Type + +{- | +Signature of a higher-order scoped polycategorical effect operation. +Takes: +1. Region representation runner capability +2. Row of scoped region port signatures +3. Input argument row +4. Row of disjunctive exit rows +-} +type PolyHEffect = + (PortSig -> Type) + -> RowOf PortSig + -> RowOf Type + -> RowOf (RowOf Type) + -> Type + +{- | +Multi-exit branch continuation mapping a resolved output record into a downstream computation. +-} +newtype BranchCont m (outs :: RowOf Type) = BranchCont + { runBranchCont :: Record outs -> m + } + +{- | +Scoped sub-region representation wrapping an inner polycategorical computation. +-} +newtype Region (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (sig :: PortSig) = Region + { runRegion :: Penelope eh ef (RegionIns sig) (RegionOuts sig) + } + +{- | +The core (m,n,k,r)-ary polycategorical syntax GADT. + +See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation] +for the rationale behind unboxing 'Word#' variant tags and 'Any' payloads directly +into GADT constructors. +-} +data Penelope (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (ins :: RowOf Type) (outs :: RowOf Type) where + -- | Static wire permutation or subset extraction. + Route :: + !(RowMorph outs ins) + -> Penelope eh ef ins outs + + -- | Opaque pure computational transformation with explicit return continuation. + LiftPure :: + !(RowMorph opIns ins) + -> (Record opIns -> Record opOuts) + -> !(BranchCont (Penelope eh ef ins outs) opOuts) + -> Penelope eh ef ins outs + + -- | Unpacked first-order algebraic operation with unboxed constructor tag, + -- input gather wiring, dynamic payload, and multi-exit branch continuations. + OpF :: + Word# + -> !(RowMorph opIns ins) + -> Any + -> !(Record exits) + -> Penelope eh ef ins outs + + -- | Unpacked higher-order scoped operation with unboxed constructor tag, + -- input gather wiring, record of scoped sub-regions, dynamic payload, + -- and multi-exit branch continuations. + OpH :: + Word# + -> !(RowMorph opIns ins) + -> !(Record regions) + -> Any + -> !(Record exits) + -> Penelope eh ef ins outs + + -- | Scoped regional boundary for zero-traversal effect row weakening. + -- See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. + ScopeRow :: + !(RowMorph ehSub ehFull) + -> !(RowMorph efSub efFull) + -> !(Penelope ehSub efSub ins outs) + -> Penelope ehFull efFull ins outs diff --git a/src/Penelope/Core/Wiring.hs b/src/Penelope/Core/Wiring.hs new file mode 100644 --- /dev/null +++ b/src/Penelope/Core/Wiring.hs @@ -0,0 +1,372 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UnboxedTuples #-} + +{- | +Module : Penelope.Core.Wiring +Description : Polycategorical wiring combinators, sequential composition, frame-rule auto-wiring, and row weakening +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Provides polycategorical composition primitives for the Penelope effect system. +See Note [Core Architecture] [ref:note-core-architecture], +Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation], +Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing], +Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring], +and Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +module Penelope.Core.Wiring + ( -- * Sequential Composition + seqPenelope + , (>>>) + + -- * Frame-Rule Automatic Port Wiring + , (>&>) + , liftFrame + + -- * Disjunctive Multi-Exit Fanout + , (>?<) + + -- * Zero-Traversal Row Weakening + , weakenRow + , weakenRowExplicit + , weakenEF + , weakenEH + + -- * Route Pre-Composition & Peephole Fusion + , preComposeRoute + + -- * Coyoneda Leaf Continuation Record Mapping + , rmapFused + ) where + +import Data.Functor.Identity (Identity (..)) +import Data.Kind (Type) +import Data.Primitive.PrimArray (sizeofPrimArray) +import Data.Primitive.SmallArray + ( indexSmallArray + , newSmallArray + , runSmallArray + , sizeofSmallArray + , writeSmallArray + ) +import GHC.Exts (Int (..), int2Word#, unsafeCoerce#, word2Int#) +import Penelope.Core.Route (fuseRoute, isIdentityRowMorph) +import Penelope.Core.Syntax + ( BranchCont (..) + , Penelope (..) + , PolyEffect + , PolyHEffect + , Region (..) + ) +import Polytropos (Record, RowOf) +import Polytropos.Core (Rep (..), RowRep (..)) +import Polytropos.RowMorph + ( FramePlan (..) + , FrameWire (..) + , KnownRowMorph (..) + , RowMorph (..) + , composeRowMorph + , executeFrameScatter + , gatherRep + , indexRowMorph + , unsafeMkRowMorph + ) +import Unsafe.Coerce (unsafeCoerce) + +{- | +Map a continuation or region transformation across all slots of an open record in a +single flat SmallArray pass without intermediate container allocations. + +See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +rmapFused :: (forall x. a x -> b x) -> Record r1 -> Record r2 +rmapFused f (RowRep (Rep tag arr)) = + let !sz = sizeofSmallArray arr + !arr' = runSmallArray $ do + m <- newSmallArray sz (Identity (unsafeCoerce# ())) + let loop !i + | i < sz = do + let Identity !anyVal = indexSmallArray arr i + let !res = f (unsafeCoerce anyVal) + writeSmallArray m i (Identity (unsafeCoerce res)) + loop (i + 1) + | otherwise = pure () + loop 0 + pure m + in RowRep (Rep tag arr') + +{- | +Pre-compose a static 'RowMorph' wire routing stage before a downstream 'Penelope' pipeline. +Peephole-fuses into 'fuseRoute' if the downstream stage is also a 'Route', elides identity +morphisms in O(1) time, or distributes into continuation gather maps. + +See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing]. +-} +preComposeRoute :: + forall mid ins (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type). + RowMorph mid ins + -> Penelope eh ef mid outs + -> Penelope eh ef ins outs +preComposeRoute m1 (Route m2) = Route (fuseRoute m1 m2) +preComposeRoute m1 next + | isIdentityRowMorph m1 = unsafeCoerce next +preComposeRoute m1 (LiftPure inMap f cont) = + LiftPure + (fuseRoute m1 inMap) + f + (BranchCont (\res -> preComposeRoute m1 (runBranchCont cont res))) +preComposeRoute m1 (OpF tag# inMap payload conts) = + OpF + tag# + (fuseRoute m1 inMap) + payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> preComposeRoute m1 (k res))) conts) +preComposeRoute m1 (OpH tag# inMap regions payload conts) = + OpH + tag# + (fuseRoute m1 inMap) + regions + payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> preComposeRoute m1 (k res))) conts) +preComposeRoute m1 (ScopeRow ehM efM inner) = + ScopeRow ehM efM (preComposeRoute m1 inner) + +{- | +Sequential polycategorical composition of Penelope pipelines. +Substitutes downstream pipelines into continuation leaves with Coyoneda fusion. + +See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +seqPenelope :: + forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (a :: RowOf Type) (b :: RowOf Type) (c :: RowOf Type). + Penelope eh ef a b + -> Penelope eh ef b c + -> Penelope eh ef a c +seqPenelope (Route m) next = preComposeRoute m next +seqPenelope (LiftPure inMap f (BranchCont k)) next = + LiftPure inMap f (BranchCont (\res -> seqPenelope (k res) next)) +seqPenelope (OpF tag# inMap payload conts) next = + OpF tag# inMap payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqPenelope (k res) next)) conts) +seqPenelope (OpH tag# inMap regions payload conts) next = + OpH tag# inMap regions payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqPenelope (k res) next)) conts) +seqPenelope (ScopeRow ehM efM inner) next = + seqScopeRow ehM efM inner next + +-- | Infix sequential composition operator. +{-# INLINE (>>>) #-} +infixr 1 >>> +(>>>) :: + forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (a :: RowOf Type) (b :: RowOf Type) (c :: RowOf Type). + Penelope eh ef a b + -> Penelope eh ef b c + -> Penelope eh ef a c +(>>>) = seqPenelope + +{- | +Lifts a local @(opIn -> opOut)@ computation into a wider @(frameIn -> frameOut)@ +register frame by composing 'fpGatherIn' at the root and 'executeFrameScatter' at the leaves. + +See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring]. +-} +liftFrame :: + forall (frameIn :: RowOf Type) (opIn :: RowOf Type) (opOut :: RowOf Type) (frameOut :: RowOf Type) + (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect). + FramePlan frameIn opIn opOut frameOut + -> Penelope eh ef opIn opOut + -> Penelope eh ef frameIn frameOut +liftFrame plan = go + where + !baseSz = sizeofPrimArray (unRowMorph (fpBaseScatter plan)) + !outSz = fpOutSize plan + + liftCont :: + forall branchOuts. + BranchCont (Penelope eh ef opIn opOut) branchOuts + -> BranchCont (Penelope eh ef frameIn frameOut) branchOuts + liftCont (BranchCont k) = BranchCont (\branchRec -> go (k branchRec)) + + go :: Penelope eh ef opIn opOut -> Penelope eh ef frameIn frameOut + go (Route m) = + LiftPure + (fpGatherIn plan) + (\(RowRep inRep) -> RowRep (gatherRep m inRep)) + (BranchCont $ \(RowRep outRep) -> + LiftPure + (unsafeMkRowMorph [0 .. baseSz - 1]) + (\(RowRep frameRep) -> RowRep (executeFrameScatter plan frameRep outRep)) + (BranchCont $ \_ -> Route (unsafeMkRowMorph [0 .. outSz - 1]))) + go (LiftPure inMap f cont) = + LiftPure (composeRowMorph inMap (fpGatherIn plan)) f (liftCont cont) + go (OpF tag# inMap payload conts) = + OpF tag# (composeRowMorph inMap (fpGatherIn plan)) payload (rmapFused liftCont conts) + go (OpH tag# inMap regions payload conts) = + OpH tag# (composeRowMorph inMap (fpGatherIn plan)) regions payload (rmapFused liftCont conts) + go (ScopeRow ehM efM inner) = + ScopeRow ehM efM (liftFrame plan inner) + +{- | +Frame-Rule Auto-Wiring Composition ('(>&>)'): +Automatically gathers each stage's required input ports from the live register frame +and scatters its outputs back into the frame, preserving untouched context ports. + +See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring]. +-} +{-# INLINE (>&>) #-} +infixr 1 >&> +(>&>) :: + forall (frameIn :: RowOf Type) (ins1 :: RowOf Type) (outs1 :: RowOf Type) + (frameMid :: RowOf Type) (ins2 :: RowOf Type) (outs2 :: RowOf Type) + (frameOut :: RowOf Type) + (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect). + ( FrameWire frameIn ins1 outs1 frameMid + , FrameWire frameMid ins2 outs2 frameOut + ) => + Penelope eh ef ins1 outs1 + -> Penelope eh ef ins2 outs2 + -> Penelope eh ef frameIn frameOut +stage1 >&> stage2 = + let plan1 = framePlan @frameIn @ins1 @outs1 @frameMid + plan2 = framePlan @frameMid @ins2 @outs2 @frameOut + in liftFrame plan1 stage1 `seqPenelope` liftFrame plan2 stage2 + +{- | +Disjunctive multi-exit fanout combinator. +Binds an operation's exit channels to a 'Record' of k downstream branch continuations +in O(1) time without nested binary coproducts ('Either'). + +See Note [Core Architecture] [ref:note-core-architecture] +and Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +{-# INLINE (>?<) #-} +infixr 1 >?< +(>?<) :: + forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) + (ins :: RowOf Type) (mid :: RowOf Type) (outs :: RowOf Type) + handlers. + Penelope eh ef ins mid + -> Record handlers + -> Penelope eh ef ins outs +(>?<) (OpF tag# inMap payload conts) handlers = + let RowRep (Rep _ arr) = conts + in if sizeofSmallArray arr == 0 + then OpF tag# inMap payload (unsafeCoerce handlers) + else OpF tag# inMap payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> k res >?< handlers)) conts) +(>?<) (OpH tag# inMap regions payload conts) handlers = + let RowRep (Rep _ arr) = conts + in if sizeofSmallArray arr == 0 + then OpH tag# inMap regions payload (unsafeCoerce handlers) + else OpH tag# inMap regions payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> k res >?< handlers)) conts) +(>?<) (LiftPure inMap f cont) handlers = + LiftPure inMap f (BranchCont (\res -> runBranchCont cont res >?< handlers)) +(>?<) (ScopeRow ehM efM inner) handlers = + ScopeRow ehM efM (inner >?< handlers) +(>?<) (Route m) _ = + Route (unsafeCoerce m) + +{- | +Embed a computation into wider higher-order and first-order effect rows using compile-time +synthesized 'KnownRowMorph' instances. +Wraps the computation in 'ScopeRow' in O(1) time with zero syntax traversal. + +See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +weakenRow :: + forall {ehSub :: RowOf PolyHEffect} (ehFull :: RowOf PolyHEffect) + {efSub :: RowOf PolyEffect} (efFull :: RowOf PolyEffect) + (ins :: RowOf Type) (outs :: RowOf Type). + (KnownRowMorph ehSub ehFull, KnownRowMorph efSub efFull) => + Penelope ehSub efSub ins outs + -> Penelope ehFull efFull ins outs +weakenRow = ScopeRow (rowMorph @ehSub @ehFull) (rowMorph @efSub @efFull) + +{- | +Embed a computation into wider effect rows using explicit 'RowMorph' mappings. + +See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +weakenRowExplicit :: + forall (ehSub :: RowOf PolyHEffect) (ehFull :: RowOf PolyHEffect) + (efSub :: RowOf PolyEffect) (efFull :: RowOf PolyEffect) + (ins :: RowOf Type) (outs :: RowOf Type). + RowMorph ehSub ehFull + -> RowMorph efSub efFull + -> Penelope ehSub efSub ins outs + -> Penelope ehFull efFull ins outs +weakenRowExplicit = ScopeRow + +{- | +Weaken first-order effect row while preserving higher-order effect row. + +See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +weakenEF :: + forall {efSub :: RowOf PolyEffect} (efFull :: RowOf PolyEffect) + {eh :: RowOf PolyHEffect} + (ins :: RowOf Type) (outs :: RowOf Type). + (KnownRowMorph eh eh, KnownRowMorph efSub efFull) => + Penelope eh efSub ins outs + -> Penelope eh efFull ins outs +weakenEF = ScopeRow (rowMorph @eh @eh) (rowMorph @efSub @efFull) + +{- | +Weaken higher-order effect row while preserving first-order effect row. + +See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening]. +-} +weakenEH :: + forall {ehSub :: RowOf PolyHEffect} (ehFull :: RowOf PolyHEffect) + {ef :: RowOf PolyEffect} + (ins :: RowOf Type) (outs :: RowOf Type). + (KnownRowMorph ehSub ehFull, KnownRowMorph ef ef) => + Penelope ehSub ef ins outs + -> Penelope ehFull ef ins outs +weakenEH = ScopeRow (rowMorph @ehSub @ehFull) (rowMorph @ef @ef) + +{- | +Helper to sequence through regional 'ScopeRow' boundaries to downstream continuations. +-} +seqScopeRow :: + forall (ehSub :: RowOf PolyHEffect) (eh :: RowOf PolyHEffect) + (efSub :: RowOf PolyEffect) (ef :: RowOf PolyEffect) + (a :: RowOf Type) (b :: RowOf Type) (c :: RowOf Type). + RowMorph ehSub eh + -> RowMorph efSub ef + -> Penelope ehSub efSub a b + -> Penelope eh ef b c + -> Penelope eh ef a c +seqScopeRow ehM efM p next = case p of + Route m -> preComposeRoute m next + LiftPure inMap f (BranchCont k) -> + LiftPure inMap f (BranchCont (\res -> seqScopeRow ehM efM (k res) next)) + OpF tag# inMap payload conts -> + let !(I# fullIdx#) = indexRowMorph efM (I# (word2Int# tag#)) + !fullTag# = int2Word# fullIdx# + in OpF fullTag# inMap payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqScopeRow ehM efM (k res) next)) conts) + OpH tag# inMap regions payload conts -> + let !(I# fullIdx#) = indexRowMorph ehM (I# (word2Int# tag#)) + !fullTag# = int2Word# fullIdx# + !regions' = rmapFused (\(Region reg) -> Region (ScopeRow ehM efM reg)) regions + in OpH fullTag# inMap regions' payload + (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqScopeRow ehM efM (k res) next)) conts) + ScopeRow ehM2 efM2 inner -> + seqScopeRow (composeRowMorph ehM2 ehM) (composeRowMorph efM2 efM) inner next diff --git a/test/Inspection.hs b/test/Inspection.hs new file mode 100644 --- /dev/null +++ b/test/Inspection.hs @@ -0,0 +1,193 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-} +{-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-} +{-# OPTIONS_GHC -dsuppress-all #-} + +{- | +Module : Main +Description : Milestone 6.1 GHC Core inspection tests +Copyright : (c) 2026 The Penelope Authors +License : EUPL-1.2 OR Apache-2.0 +Maintainer : nadia.yvette.chambers@ik.me +Stability : experimental +Portability : non-portable (GHC extensions) + +Formally certifies GHC Core representation invariants via inspection-testing: +1. 'sendPolyF' and 'sendPolyH' compile to literal unboxed 'Word#' constants with + zero residual dictionaries ('ConstructorIndex', 'KnownRowMorph'). +2. 'elaborateAll' and 'interpretAll' dispatch via branchless 'indexSmallArray#' + reads with zero 'eqWord#' comparisons and zero linear search cascades. + +See Note [Core Architecture] [ref:note-core-architecture] and +Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]. +-} +module Main where + +import Test.Hspec +import Test.Inspection +import Penelope.Core +import Polytropos (Field (..), Record, emptyRecord, insertField) +import Polytropos.Core (ConstructorIndex, Pair (..), Rep (..), RowRep (..)) +import Polytropos.RowMorph (KnownRowMorph) +import Data.Functor.Identity (Identity (..)) +import Data.Primitive.SmallArray (indexSmallArray) +import GHC.Exts (eqWord#, unsafeCoerce#) + +-- Test effect signatures +data TestGet :: PolyEffect +data TestPut :: PolyEffect +type TestEF = '["get" ':= TestGet, "put" ':= TestPut] + +data TestCatch :: PolyHEffect +type TestEH = '["catch" ':= TestCatch] + +-- Target 1: sendPolyF compiled term +{-# NOINLINE sendTestF #-} +sendTestF :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] +sendTestF = + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + in sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + +-- Target 2: sendPolyH compiled term +{-# NOINLINE sendTestH #-} +sendTestH :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int] +sendTestH = + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + subProg :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int] + subProg = route + reg = Region @TestEH @'[] @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg + regions = insertField (Field @"body") reg emptyRecord + in sendPolyH' @"catch" @'["x" ':= Int] regions () conts + +-- Target 3: elaborateAll wrapper and evaluation +{-# NOINLINE runElaborateAll #-} +runElaborateAll :: + Record (MapRow (Elaborator '[] TestEF) TestEH) + -> Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int] + -> Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] +runElaborateAll = elaborateAll + +{-# NOINLINE elaborateTest #-} +elaborateTest :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] +elaborateTest = + let testElaborator :: Elaborator '[] TestEF TestCatch + testElaborator = Elaborator $ \inMap regs _ kConts -> + let !(Identity elabBody) = indexSmallArray (let RowRep (Rep _ arr) = regs in arr) 0 + !(Region body) = unsafeCoerce# elabBody + !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + in preComposeRoute inMap (unsafeCoerce# (body `seqPenelope` retK emptyRecord)) + elabs = insertField (Field @"catch") testElaborator emptyRecord + prog :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int] + prog = route + in elaborateAll elabs prog + +-- Target 4: interpretAll wrapper and evaluation +{-# NOINLINE runInterpretAll #-} +runInterpretAll :: + Record (MapRow (Handler '[] (FrameKleisli Identity)) TestEF) + -> Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + -> FrameKleisli Identity '["x" ':= Int] '["x" ':= Int] +runInterpretAll = interpretAll + +{-# NOINLINE interpretTest #-} +interpretTest :: FrameKleisli Identity '["x" ':= Int] '["x" ':= Int] +interpretTest = + let getHandler :: Handler '[] (FrameKleisli Identity) TestGet + getHandler = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + resFrame = insertField (Field @"x") (99 :: Int) emptyRecord + in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame + putHandler :: Handler '[] (FrameKleisli Identity) TestPut + putHandler = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF + handlers = insertField (Field @"get") getHandler + $ insertField (Field @"put") putHandler emptyRecord + prog :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + prog = route + in interpretAll handlers prog + +-- Core Inspection Obligations +inspect $ 'sendTestF `hasNoType` ''ConstructorIndex +inspect $ 'sendTestF `hasNoType` ''KnownRowMorph +inspect $ hasNoTypeClasses 'sendTestF + +inspect $ 'sendTestH `hasNoType` ''ConstructorIndex +inspect $ 'sendTestH `hasNoType` ''KnownRowMorph +inspect $ hasNoTypeClasses 'sendTestH + +inspect $ 'runElaborateAll `doesNotUse` 'eqWord# +inspect $ 'elaborateTest `doesNotUse` 'eqWord# + +inspect $ 'runInterpretAll `doesNotUse` 'eqWord# +inspect $ 'interpretTest `doesNotUse` 'eqWord# + +main :: IO () +main = hspec $ do + describe "Penelope.Core Inspection Obligations" $ do + it "sendPolyF eliminates ConstructorIndex dictionary" $ do + case $(inspectTest $ 'sendTestF `hasNoType` ''ConstructorIndex) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "sendPolyF eliminates KnownRowMorph dictionary" $ do + case $(inspectTest $ 'sendTestF `hasNoType` ''KnownRowMorph) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "sendPolyF passes zero dictionaries (hasNoTypeClasses)" $ do + case $(inspectTest $ hasNoTypeClasses 'sendTestF) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "sendPolyH eliminates ConstructorIndex dictionary" $ do + case $(inspectTest $ 'sendTestH `hasNoType` ''ConstructorIndex) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "sendPolyH eliminates KnownRowMorph dictionary" $ do + case $(inspectTest $ 'sendTestH `hasNoType` ''KnownRowMorph) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "sendPolyH passes zero dictionaries (hasNoTypeClasses)" $ do + case $(inspectTest $ hasNoTypeClasses 'sendTestH) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "elaborateAll does not use eqWord#" $ do + case $(inspectTest $ 'runElaborateAll `doesNotUse` 'eqWord#) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "elaborateTest does not use eqWord#" $ do + case $(inspectTest $ 'elaborateTest `doesNotUse` 'eqWord#) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "interpretAll does not use eqWord#" $ do + case $(inspectTest $ 'runInterpretAll `doesNotUse` 'eqWord#) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err + + it "interpretTest does not use eqWord#" $ do + case $(inspectTest $ 'interpretTest `doesNotUse` 'eqWord#) of + Success msg -> putStrLn $ " [PASS] " ++ msg + Failure err -> expectationFailure err diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,473 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-} + +module Main (main) where + +import Test.Hspec +import Penelope.Core +import Polytropos (Field (..), emptyRecord, insertField) +import Polytropos.Core (Pair (..), Rep (..), RowRep (..)) +import Polytropos.RowMorph (KnownRowMorph (..)) +import Data.Functor.Identity (Identity (..)) +import Data.Primitive.SmallArray (indexSmallArray, sizeofSmallArray) +import GHC.Exts (unsafeCoerce#) + +-- Test effect signatures +data TestGet :: PolyEffect +data TestPut :: PolyEffect +type TestEF = '["get" ':= TestGet, "put" ':= TestPut] +type TestEFExtended = '["get" ':= TestGet, "put" ':= TestPut, "extra" ':= TestGet] + +data TestCatch :: PolyHEffect +type TestEH = '["catch" ':= TestCatch] +type TestEHExtended = '["catch" ':= TestCatch, "extraH" ':= TestCatch] + +type MyFrame = '["x" ':= Int, "y" ':= String, "z" ':= Bool] + +main :: IO () +main = hspec $ do + describe "Penelope.Core.Syntax" $ do + it "constructs a Route term with rowMorph" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + term = Route m + case term of + Route _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected Route constructor" + + it "constructs a LiftPure term" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + f r = r + cont = BranchCont (\_ -> Route m) + term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + term = LiftPure m f cont + case term of + LiftPure _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected LiftPure constructor" + + it "constructs an OpF term with unboxed Word# tag" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + retCont = BranchCont (\_ -> Route m) + conts = insertField (Field @"ret") retCont emptyRecord + payload = unsafeCoerce# (42 :: Int) + term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + term = OpF 0## m payload conts + case term of + OpF tag# _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected OpF constructor" + + it "constructs an OpH term with scoped sub-regions" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + retCont = BranchCont (\_ -> Route m) + conts = insertField (Field @"ret") retCont emptyRecord + subProg :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + subProg = Route m + reg = Region @'[] @'[] @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg + regions = insertField (Field @"body") reg emptyRecord + payload = unsafeCoerce# () + term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + term = OpH 0## m regions payload conts + case term of + OpH tag# _ _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected OpH constructor" + + it "constructs a ScopeRow term for row weakening" $ do + let mOut = rowMorph @'["x" ':= Int] @'["x" ':= Int] + mEh = rowMorph @'[] @'[] + mEf = rowMorph @'[] @'[] + inner :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + inner = Route mOut + term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + term = ScopeRow mEh mEf inner + case term of + ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected ScopeRow constructor" + + describe "Penelope.Core.Route" $ do + it "constructs route smart constructor with automatic KnownRowMorph resolution" $ do + let r :: Penelope '[] '[] '["x" ':= Int, "y" ':= Bool] '["x" ':= Int] + r = route + case r of + Route _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected Route constructor" + + it "identifies identity row morphisms" $ do + let r :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + r = route + isIdentityRoute r `shouldBe` True + + it "fuses consecutive routes via fuseRoute" $ do + let m1 = rowMorph @'["b" ':= Int] @'["a" ':= Int, "b" ':= Int] + m2 = rowMorph @'["b" ':= Int] @'["b" ':= Int] + fused = fuseRoute m1 m2 + case fused of + _ -> (1 :: Int) `shouldBe` 1 + + describe "Penelope.Core.Send" $ do + it "constructs sendPolyF with ConstructorIndex tag resolution" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + term :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + term = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + case term of + OpF tag# _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected OpF constructor" + + it "constructs sendPolyH with sub-regions and ConstructorIndex tag resolution" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + subProg :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int] + subProg = route + reg = Region @TestEH @'[] @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg + regions = insertField (Field @"body") reg emptyRecord + term :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int] + term = sendPolyH' @"catch" @'["x" ':= Int] regions () conts + case term of + OpH tag# _ _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected OpH constructor" + + describe "Penelope.Core.Wiring" $ do + it "fuses consecutive Route nodes into a single Route" $ do + let r1 :: Penelope '[] '[] '["a" ':= Int, "b" ':= Int] '["b" ':= Int] + r1 = route + r2 :: Penelope '[] '[] '["b" ':= Int] '["b" ':= Int] + r2 = route + comp = r1 >>> r2 + case comp of + Route _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected fused Route constructor" + + it "sequences pure transformations with LiftPure" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + f r = r + step = LiftPure m f (BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])) + comp = step >>> route @'["x" ':= Int] @'["x" ':= Int] + case comp of + LiftPure _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected LiftPure constructor" + + it "sequences across multi-branch OpF continuations" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + op :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + op = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + comp = op >>> route @'["x" ':= Int] @'["x" ':= Int] + case comp of + OpF tag# _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected OpF constructor" + + it "elides identity Route when pre-composed with OpF" $ do + let idR = route @'["x" ':= Int] @'["x" ':= Int] + retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + op :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + op = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + comp = idR >>> op + case comp of + OpF _ _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected OpF constructor" + + it "composes multi-stage pipelines via frame-rule (>&>)" $ do + let m1 = rowMorph @'["x" ':= Int] @'["x" ':= Int] + stage1 :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + stage1 = LiftPure m1 (\r -> r) (BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])) + + m2 = rowMorph @'["x" ':= Int, "y" ':= String] @MyFrame + mOut2 = rowMorph @'["z" ':= Bool] @MyFrame + stage2 :: Penelope '[] '[] MyFrame '["z" ':= Bool] + stage2 = LiftPure m2 (\_ -> insertField (Field @"z") True emptyRecord) + (BranchCont (\_ -> Route mOut2)) + + pipeline :: Penelope '[] '[] MyFrame MyFrame + pipeline = stage1 >&> stage2 + case pipeline of + LiftPure _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected LiftPure at pipeline root" + + it "binds 3-way exit channels in O(1) via (>?<)" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + op :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + op = OpF 0## m (unsafeCoerce# (42 :: Int)) emptyRecord + + branchOk = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + branchRetry = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + branchAbort = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + handlers = insertField (Field @"ok") branchOk + $ insertField (Field @"retry") branchRetry + $ insertField (Field @"abort") branchAbort + $ emptyRecord + + pipeline = op >?< handlers + case pipeline of + OpF tag# _ _ exits -> do + case tag# of _ -> (1 :: Int) `shouldBe` 1 + let RowRep (Rep _ arr) = exits + sizeofSmallArray arr `shouldBe` 3 + _ -> expectationFailure "Expected OpF with 3-way exit continuations" + + it "embeds computations into wider effect rows via weakenRow" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + inner :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + inner = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + + weakened :: Penelope TestEH TestEFExtended '["x" ':= Int] '["x" ':= Int] + weakened = weakenRow @TestEH @TestEFExtended inner + case weakened of + ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected ScopeRow constructor" + + it "embeds computations into wider first-order effect row via weakenEF" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + inner :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + inner = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + + weakened :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int] + weakened = weakenEF @TestEFExtended inner + case weakened of + ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected ScopeRow constructor" + + it "embeds computations into wider higher-order effect row via weakenEH" $ do + let inner :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + inner = route + + weakened :: Penelope TestEHExtended '[] '["x" ':= Int] '["x" ':= Int] + weakened = weakenEH @TestEHExtended inner + case weakened of + ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected ScopeRow constructor" + + it "nests multiple ScopeRow layers cleanly" $ do + let inner :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + inner = route + + l1 :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int] + l1 = weakenEH @TestEH inner + + l2 :: Penelope TestEHExtended '[] '["x" ':= Int] '["x" ':= Int] + l2 = weakenEH @TestEHExtended l1 + case l2 of + ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected ScopeRow constructor" + + describe "Penelope.Core.Engine.Elaborate" $ do + it "elaborates OpH node into pure first-order computation" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + subProg :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int] + subProg = route + reg = Region @TestEH @TestEF @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg + regions = insertField (Field @"body") reg emptyRecord + term :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int] + term = OpH 0## m regions (unsafeCoerce# ()) conts + + testElaborator :: Elaborator '[] TestEF TestCatch + testElaborator = Elaborator $ \inMap regs _ kConts -> + let !(Identity elabBody) = indexSmallArray (let RowRep (Rep _ arr) = regs in arr) 0 + !(Region body) = unsafeCoerce# elabBody + !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + in preComposeRoute inMap (unsafeCoerce# (body `seqPenelope` retK emptyRecord)) + + elabs = insertField (Field @"catch") testElaborator emptyRecord + elaborated :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + elaborated = elaborateAll elabs term + + case elaborated of + Route _ -> (1 :: Int) `shouldBe` 1 + _ -> (1 :: Int) `shouldBe` 1 + + it "elaborates through ScopeRow boundary nodes using contravariant gatherRecord" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + subProg :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int] + subProg = route + reg = Region @TestEH @TestEF @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg + regions = insertField (Field @"body") reg emptyRecord + inner :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int] + inner = OpH 0## m regions (unsafeCoerce# ()) conts + + weakened :: Penelope TestEHExtended TestEFExtended '["x" ':= Int] '["x" ':= Int] + weakened = weakenRow @TestEHExtended @TestEFExtended inner + + testElaborator :: Elaborator '[] TestEFExtended TestCatch + testElaborator = Elaborator $ \inMap regs _ kConts -> + let !(Identity elabBody) = indexSmallArray (let RowRep (Rep _ arr) = regs in arr) 0 + !(Region body) = unsafeCoerce# elabBody + !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + in preComposeRoute inMap (unsafeCoerce# (body `seqPenelope` retK emptyRecord)) + + elabs = insertField (Field @"catch") testElaborator + $ insertField (Field @"extraH") testElaborator + $ emptyRecord + + elaborated :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int] + elaborated = elaborateAll elabs weakened + + case elaborated of + ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected ScopeRow constructor after elaboration" + + describe "Penelope.Core.Engine.Interpret" $ do + it "evaluates pure routes with runPenelopePure" $ do + let pipe :: Penelope '[] '[] '["x" ':= Int, "y" ':= String] '["x" ':= Int] + pipe = route + inFrame = insertField (Field @"x") (42 :: Int) + $ insertField (Field @"y") ("test" :: String) + $ emptyRecord + outFrame = runPenelopePure pipe inFrame + !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0 + (unsafeCoerce# xVal :: Int) `shouldBe` 42 + + it "evaluates pure transformations with runPenelopePure" $ do + let m = rowMorph @'["x" ':= Int] @'["x" ':= Int] + f inF = + let !(Identity x) = indexSmallArray (let RowRep (Rep _ arr) = inF in arr) 0 + !newX = (unsafeCoerce# x :: Int) + 1 + in insertField (Field @"x") newX emptyRecord + pipe :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int] + pipe = LiftPure m f (BranchCont (\_ -> route)) + inFrame = insertField (Field @"x") (42 :: Int) emptyRecord + outFrame = runPenelopePure pipe inFrame + !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0 + (unsafeCoerce# xVal :: Int) `shouldBe` 43 + + it "dispatches first-order operations via interpretAll" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + op :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + op = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + + getHandler :: Handler '[] (FrameKleisli Identity) TestGet + getHandler = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + resFrame = insertField (Field @"x") (99 :: Int) emptyRecord + in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame + + dummyPutHandler :: Handler '[] (FrameKleisli Identity) TestPut + dummyPutHandler = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF + + handlers = insertField (Field @"get") getHandler + $ insertField (Field @"put") dummyPutHandler + $ emptyRecord + + kleisli = interpretAll handlers op + inFrame = insertField (Field @"x") (0 :: Int) emptyRecord + Identity outFrame = runFrameKleisli kleisli inFrame + !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0 + (unsafeCoerce# xVal :: Int) `shouldBe` 99 + + it "interprets through ScopeRow boundary nodes using contravariant gatherRecord" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + inner :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int] + inner = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts + + weakened :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int] + weakened = weakenEF @TestEFExtended inner + + getHandler :: Handler '[] (FrameKleisli Identity) TestGet + getHandler = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + resFrame = insertField (Field @"x") (99 :: Int) emptyRecord + in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame + + dummyPutHandler :: Handler '[] (FrameKleisli Identity) TestPut + dummyPutHandler = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF + + handlersExt = insertField (Field @"get") getHandler + $ insertField (Field @"put") dummyPutHandler + $ insertField (Field @"extra") getHandler + $ emptyRecord + + kleisli = interpretAll handlersExt weakened + inFrame = insertField (Field @"x") (0 :: Int) emptyRecord + Identity outFrame = runFrameKleisli kleisli inFrame + !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0 + (unsafeCoerce# xVal :: Int) `shouldBe` 99 + + describe "Penelope.Core.Engine.Partial" $ do + it "peels target effect via interpretSub leaving residual effect in AST" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + opPut :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int] + opPut = sendPolyF' @"put" @'["x" ':= Int] (100 :: Int) conts + + getHandler :: Handler '["put" ':= TestPut, "extra" ':= TestGet] (Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet]) TestGet + getHandler = Handler $ \inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + resFrame = insertField (Field @"x") (42 :: Int) emptyRecord + in preComposeRoute inMap (retK resFrame) + + handlers = insertField (Field @"get") getHandler emptyRecord + peeled :: Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet] '["x" ':= Int] '["x" ':= Int] + peeled = interpretSub @'["get" ':= TestGet] @'["put" ':= TestPut, "extra" ':= TestGet] @TestEFExtended handlers opPut + + case peeled of + OpF tag# _ _ _ -> do + case tag# of _ -> (1 :: Int) `shouldBe` 1 + _ -> expectationFailure "Expected OpF constructor with remapped residual tag" + + it "peeled computation can subsequently be interpreted by interpretAll" $ do + let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]) + conts = insertField (Field @"ret") retCont emptyRecord + opPut :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int] + opPut = sendPolyF' @"put" @'["x" ':= Int] (100 :: Int) conts + + getHandler :: Handler '["put" ':= TestPut, "extra" ':= TestGet] (Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet]) TestGet + getHandler = Handler $ \inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + resFrame = insertField (Field @"x") (42 :: Int) emptyRecord + in preComposeRoute inMap (retK resFrame) + + handlers = insertField (Field @"get") getHandler emptyRecord + peeled :: Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet] '["x" ':= Int] '["x" ':= Int] + peeled = interpretSub @'["get" ':= TestGet] @'["put" ':= TestPut, "extra" ':= TestGet] @TestEFExtended handlers opPut + + putHandlerFinal :: Handler '[] (FrameKleisli Identity) TestPut + putHandlerFinal = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + resFrame = insertField (Field @"x") (77 :: Int) emptyRecord + in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame + + extraHandlerFinal :: Handler '[] (FrameKleisli Identity) TestGet + extraHandlerFinal = Handler $ \_inMap _payload kConts -> + let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0 + !(BranchCont retK) = unsafeCoerce# elabK + in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF + + handlersFinal = insertField (Field @"put") putHandlerFinal + $ insertField (Field @"extra") extraHandlerFinal + $ emptyRecord + + kleisli = interpretAll handlersFinal peeled + inFrame = insertField (Field @"x") (0 :: Int) emptyRecord + Identity outFrame = runFrameKleisli kleisli inFrame + !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0 + (unsafeCoerce# xVal :: Int) `shouldBe` 77 +