WingNews logo WingNews
top | item 34803613

The Logic of Functional Programming

6 points| johnbernier | 3 years ago |lisp-ai.blogspot.com

5 comments

order

johnbernier|3 years ago

In this post I describe my own journey getting in to functional programming. Early on I gained a deep fascination with functional lenses, and their ability to let us focus on a portion of a data structure. Yet it seems to me that this should be part of a larger logical theory of functions.

If we can peer in to focus in on parts a data structure, we should also be able to focus in on parts of functions. To expose how functions behave relative to parts of structures like those determined by lenses. I describe how commutative squares let you do that. A large assortment of references is provided at the end for interested parties who want to know more.

082349872349872|3 years ago

A/ are you familiar with the APL languages? they often emphasise a difference between changing data-at-locations (hylē) and the arrangement-of-the-locations (morphē). Moving forward from them, one gets Squiggol, then Haskell explorations of "deforestation", then ??

B/ I have been playing around with the following idea lately; does it correspond to anything nicely explainable in your theory?

If we have a function f (respecting some sort of structure), we can do 3 (6) particularly nice things with it to get more functions:

    - f°g precompose with a projection (or a section)
    - h°f postcompose with an injection (or a retraction)
    - g*°f°g conjugate with a bijection (or the split of an idempotent)