The Logic of Functional Programming | Hacker News Reader

The Logic of Functional Programming

lisp-ai.blogspot.com

6 pointsjohnbernier5 comments

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.

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)

The topos of functions Sets^(->) has as its objects functions and as its morphisms m: f -> g function pairs (h,k) that make a commutative square with gh = kf. If we take function pairs like (h,k) as our morphisms then we can do several things to simplify them: like making the two functions in the pair equal or making one of them into an identity.

1. precomposition: with precomposition you should use a function pair (h, 1_b) that has an identity for the second part to form a morphism m: fg -> f like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFswL...

2. postcomposition: with postcomposition you should use a function pair (1_b, k) that has an identity for the first part to form a morphism m: f -> hf like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFsyL...

3. conjugation: with conjugation you can actually use an equal function pair (g,g) to get a morphism from a function f to its conjugate gfg^{-1}. Then we see that this forms a commutative square for gfg^{-1}g = gf. Thusly, there is always a morphism from any function to its conjugate by a bijection like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQSJdLFswL...

Therefore, I would say that precomposition, postcomposition, and conjugation form special types of morphisms between functions defined by special properties like having one function be the identity or having both functions be equal to one another. Then beyond that we can classify these morphisms by rather or not their components are projections, injections, or bijections to get towards what you are speaking about. This all fits in to the perspective that functions are objects in Sets^(->), so that is nice.

I can't say I've ever used APL but I have heard of it. It has some very interesting syntax and notation, but I have made it far enough to actually try it out yet.

Thanks! That gives me enough concrete examples of Sets^(->) to explore your blog further.

As a double-check, to get precomposition m : f -> fg like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFswL... ?

That works for any function f that is precomposed by a bijection. Then the bijection and its inverse cancel out, so that is correct. Many of these examples with regards to precomposition and postcomposition might be embedded in other categories, such as slice categories: C/f or f/C. However, of all the different categories you can use to make a model of functions I have singled out Sets^(->) because it forms a topos.

The property that Sets^(->) is a topos gives us a lot to work with. All impredicative constructive mathematics can be defined internal to Sets^(->). This is interesting because it means almost all mathematics can be done internal to Sets^(->), with functions instead of sets as its first class logical objects.

Secondly, the fact that it is a topos gives us an internal logic in Sets^(->). The internal logic of Sets^(->) is a trivalent logic with three values: true, false, and half truth that fails to satisfy the law of excluded middle. Sets^(->) has its own distinct system of logical operators and connectives which generalize those in classical logic and that can be used on all subobjects.

All aside from that, Sets^(->) has an incredibly remarkable logic of quotients. It has been shown that the dual logic of quotients in Sets^(->) is intuitively similar to the partition pairs construction of Hartmanis and Stearns in Algebraic Structure Theory of Sequential Machines (1966). So the immense power of the topos Sets^(->) is enough to capture their central construction for creating a computational structure theory, and mine.

All this demonstrates that Sets^(->) by itself has an incredibly rich theory which is worthy of further exploration. The theory of Sets^(->) is really the functional counterpart of set theoretic foundations, a foundation for a different kind of function-based mathematics, and the means by which we can create a system of logical reasoning for functional programs.

[1] https://ncatlab.org/nlab/show/topos

[2] https://ncatlab.org/nlab/show/internalization

[3] https://ncatlab.org/nlab/show/internal+logic

[4] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.

Reply on news.ycombinator.com