LEADER 07206nam 2200469 450 001 996503466903316 005 20231110221414.0 010 $a3-031-21314-9 035 $a(MiAaPQ)EBC7165837 035 $a(Au-PeEL)EBL7165837 035 $a(CKB)25913955800041 035 $a(PPN)267813090 035 $a(EXLCZ)9925913955800041 100 $a20230422d2022 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aTrends in functional programming $e23rd International Symposium, TFP 2022, virtual event, March 17-18, 2022, revised selected papers /$fedited by Wouter Swierstra, Nicolas Wu 210 1$aCham, Switzerland :$cSpringer,$d[2022] 210 4$dİ2022 215 $a1 online resource (200 pages) 225 1 $aLecture Notes in Computer Science ;$vv.13401 311 08$aPrint version: Swierstra, Wouter Trends in Functional Programming Cham : Springer International Publishing AG,c2023 9783031213137 320 $aIncludes bibliographical references and index. 327 $aIntro -- Preface -- Organization -- Contents -- Project Paper: Embedding Generic Monadic Transformer into Scala -- 1 Introduction -- 2 Embedding Generic Monadic Cps Transform into Scala -- 2.1 Monads Parametrization -- 2.2 Translation of Higher-Order Functions -- 2.3 Call-Chain Substitutions -- 2.4 Automatic Coloring -- 3 Related Work -- 4 Conclusion and Further Work -- References -- Towards a Language for Defining Reusable Programming Language Components -- 1 Introduction -- 2 CS by Example -- 2.1 Data Types and Functions -- 2.2 Effects and Handlers -- 2.3 Order of Evaluation, Suspension, and Enactment -- 2.4 Modules and Imports -- 2.5 Composable Data Types and Functions -- 3 Defining Reusable Language Components in CS -- 3.1 A Signature for Reusable Components -- 3.2 A Language Component for Arithmetic Expressions -- 3.3 Implementing Functions as a Reusable Effect -- 3.4 Example Usage -- 4 Related Work -- 5 Future Work -- 6 Conclusion -- References -- Deep Embedding with Class -- 1 Introduction -- 1.1 Research Contribution -- 2 Deep Embedding -- 3 Shallow Embedding -- 3.1 Tagless-Final Embedding -- 4 Lifting the Backends -- 5 Existential Data Types -- 5.1 Unbraiding the Semantics from the Data -- 6 Transformation Semantics -- 6.1 Convolution -- 6.2 Pattern Matching -- 6.3 Chaining Semantics -- 7 Generalised Algebraic Data Types -- 8 Conclusion -- 9 Related Work -- A Appendix -- A.1 Data Type Definitions -- A.2 Smart Constructors -- A.3 Semantics Classes and Data Types -- A.4 GDict instances -- A.5 Evaluator Instances -- A.6 Printer Instances -- A.7 Optimisation Instances -- References -- Understanding Algebraic Effect Handlers via Delimited Control Operators -- 1 Introduction -- 2 S0: A Calculus of Shift0 and Dollar -- 3 h: A Calculus of Effect Handlers -- 4 Adding and Removing the Return Clause -- 4.1 Translating Between Dollar and Reset0. 327 $a4.2 Translating Between Handlers with and Without Return Clause -- 4.3 Correctness -- 5 Deriving a CPS Translation -- 5.1 CPS Translation of Shift0 and Dollar -- 5.2 CPS Translation of Effect Handlers -- 5.3 Macro Translation from h to S0 -- 5.4 Composing Macro and CPS Translations -- 6 Deriving a Type System from the CPS Translation -- 6.1 Type System of Shift0 and Dollar -- 6.2 Type System of Effect Handlers -- 6.3 Applying the CPS Approach -- 6.4 Soundness -- 7 Related Work -- 8 Conclusion and Future Perspectives -- References -- Reducing the Power Consumption of IoT with Task-Oriented Programming -- 1 Introduction -- 1.1 Research Contribution -- 2 Task-Oriented Programming -- 2.1 mTask -- 3 Energy Efficient IoT Nodes -- 4 Scheduling Tasks Efficiently -- 4.1 Evaluation Interval -- 4.2 Basic Refresh Rates -- 4.3 Deriving Refresh Rates -- 4.4 User Defined Refresh Rates -- 5 Running Tasks on Interrupts -- 6 Implementing Refresh Rates -- 7 Scheduling Tasks -- 8 Resulting Power Reductions -- 8.1 Power Saving -- 9 Related Work -- 10 Conclusion -- References -- Semantic Equivalence of Task-Oriented Programs in TopHat -- 1 Introduction -- 2 The TopHat Language -- 2.1 Editors -- 2.2 Sequential Composition -- 2.3 Parallel Composition -- 2.4 Observations -- 2.5 Semantics -- 3 Contextual Equivalence -- 4 Expression Equivalence -- 5 Task Conditions -- 5.1 Failing Tasks -- 5.2 Finished Tasks -- 5.3 Stuck Tasks -- 5.4 Running Tasks -- 6 Task Equivalence -- 7 Laws on Tasks -- 8 Conclusions -- A Appendix -- A.1 Failing -- A.2 Inputs -- A.3 Value -- References -- Algorithm Design with the Selection Monad -- 1 Introduction -- 2 Selection Functions -- 2.1 Pairs of Selection Functions -- 2.2 Password Example -- 2.3 Iterated Product of Selection Functions -- 2.4 Dependently Typed Version -- 2.5 Extended Password Example -- 2.6 Selection Functions Form a Monad. 327 $a2.7 History-Dependent Product of Selection Functions -- 2.8 Efficiency Drawbacks of This Implementation -- 3 Greedy Algorithms -- 4 Examples of Greedy Algorithms -- 4.1 Password Example -- 4.2 Prim's Algorithm -- 4.3 Greedy Graph Walking -- 5 Correctness -- 6 Limited Lookahead -- 6.1 Graph Example -- 7 Iterated Product -- 7.1 Examples -- 8 Conclusion and Future Work -- A Proof that Product Equals Sequence -- References -- Sound and Complete Type Inference for Closed Effect Rows -- 1 Introduction -- 2 Motivation -- 2.1 Algebraic Effects and Handlers -- 2.2 Naive Hindley-Milner Type Inference with Algebraic Effects and Handlers -- 2.3 Type Inference with open and close -- 3 Implicitly Typed Calculus for Algebraic Effects and Handlers -- 3.1 Syntax -- 3.2 Declarative Type Inference Rules -- 4 Syntax-Directed Type Inference Rules -- 4.1 Type Substitution -- 4.2 Type Ordering -- 4.3 Inference Rules with open and close -- 4.4 Principles on the Use of [let] Rule -- 4.5 Fragility of [let] Rule -- 5 Type Inference Algorithm -- 5.1 Auxiliary Functions -- 5.2 Unification Algorithm -- 5.3 Type Inference Algorithm -- 6 Related Work -- 7 Conclusion and Future Work -- A System F + restrict -- B Type-Directed Translation to System F+restrict -- References -- Towards Efficient Adjustment of Effect Rows -- 1 Introduction -- 2 Overview -- 2.1 Effect Handlers -- 2.2 Evidence Passing Semantics and Row-Based Effect System -- 2.3 Effect Type Adjustment for Function Types -- 2.4 Motivating Open Floating -- 3 System Fpwo -- 3.1 Syntax -- 3.2 Dynamic Semantics -- 3.3 Static Semantics -- 3.4 Effect Rows and Closed Prefix Relation -- 4 Open Floating -- 4.1 Design of Algorithm -- 4.2 Organization of Definition -- 4.3 The Definition -- 4.4 Example -- 5 Evaluation -- 5.1 Ideal Case -- 5.2 Failure Case -- 6 Future Work -- 7 Related Work -- 8 Conclusion -- References -- Author Index. 410 0$aLecture Notes in Computer Science 606 $aFunctional programming (Computer science) 615 0$aFunctional programming (Computer science) 676 $a910.5 702 $aSwierstra$b Wouter 702 $aWu$b Nicolas 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996503466903316 996 $aTrends in Functional Programming$91947569 997 $aUNISA