NDLI: Functional pearl: getting a quick fix on comonads

Please wait, while we are loading the content...

Improving Haskell types with SMT

Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs

Bridging the GUI gap with reactive values and relations

Variations on variants

Freer monads, more extensible effects

Injective type families for Haskell

Déjà Fu: a concurrency testing library for Haskell

Practical probabilistic programming with monads

Guilt free ivory

A typechecker plugin for units of measure: domain-specific constraint solving in GHC Haskell

Formally proving a compiler transformation safe

The remote monad design pattern

Modular reifiable matching: a list-of-functors approach to two-level types

Functional pearl: getting a quick fix on comonads

Type families with class, type classes with family

Improving implicit parallelism

Embedding a full linear Lambda calculus in Haskell

Type-safe runtime code generation: accelerate to LLVM

Functional pearl: getting a quick fix on comonads

Content Provider	ACM Digital Library
Author	Foner, Kenneth
Abstract	A piece of functional programming folklore due to Piponi provides Löb's theorem from modal provability logic with a computational interpretation as an unusual fixed point. Interpreting modal necessity as an arbitrary Functor in Haskell, the "type" of Löb's theorem is inhabited by a fixed point function allowing each part of a structure to refer to the whole. However, Functor's logical interpretation may be used to prove Löb's theorem only by relying on its implicit functorial strength, an axiom not available in the provability modality. As a result, the well known loeb fixed point "cheats" by using functorial strength to implement its recursion. Rather than Functor, a closer Curry analogue to modal logic's Howard inspiration is a closed (semi-)comonad, of which Haskell's ComonadApply typeclass provides analogous structure. Its computational interpretation permits the definition of a novel fixed point function allowing each part of a structure to refer to its own context within the whole. This construction further guarantees maximal sharing and asymptotic efficiency superior to loeb for locally contextual computations upon a large class of structures. With the addition of a distributive law, closed comonads may be composed into spaces of arbitrary dimensionality while preserving the performance guarantees of this new fixed point. From these elements, we construct a small embedded domain-specific language to elegantly express and evaluate multidimensional "spreadsheet-like" recurrences for a variety of cellular automata. .
Starting Page	106
Ending Page	117
Page Count	12
File Format	PDF
ISBN	9781450338080
DOI	10.1145/2804302.2804310
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2015-08-30
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Spreadsheets Haskell Modal logic Closed comonads
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in