Skip navigation

Not the kind of reflection (I think!) one finds in Java, or even for meta-programming in Coq or Idris or such.  I am speaking of the principle from the algebra of programming that is called reflection (not quite sure why).  It is a property relating eliminations and constructions of datatypes.  It says that folding with the constructors is the identity.  For example, take lists in Haskell, with foldr (I specialized this from Foldable a to just [a])

foldr :: (a -> b -> b) -> b -> [a] -> b

and constructors

(:) :: a -> [a] -> [a]
[] :: [a]

Instantiating (implicitly) type variable b with [a], we can write

foldr (:) []

and this is equivalent to the identity function.  All it does is go through the list and interpret cons as cons, nil as nil.  So we have the valid equation

foldr (:) [] = id

It is known (although I am not sure where you can find this in a paper) that if you have parametricity and reflection, you can derive induction.  Unary parametricity for Church-encoded lists, say, is essentially the predicate

\ l : [a] .

forall x : * . forall c : a -> x -> x . forall n : x .

forall R : x -> * .

(forall h : a . forall t : x . R t -> R (c h t)) ->

R n ->

R (l c n)

 

In words, it says that if you are doing a foldr with c and n, and n satisfies R and c preserves R, then R holds of the foldr of l with c and n (i.e., the elimination l c n).

Now, if we just instantiate this with (:) for c and [] for n, we have a statement of list induction — almost.  We get to conclude the predicate R for (l (:) []), not just for l.  But hey, if we have reflection, we know that doing a fold right with (:) and [] is the identity, so we can get R l from R (l (:) []).

That is great as a technical trick — and we have used this in Cedille — but it seems to come out of nowhere.  Actually, reflection is a consequence of initiality for the initial algebra of the datatype, so it is definitely not out of nowhere.  But still it is not clear why parametricity + reflection should yield induction.  What is the intuition for that?

Actually, I have a little intuition to offer.  With induction, we are trying to summarize an infinite number of cases in some finite way.  This finite way is with the constructors for the datatype.  There are infinitely many natural numbers, say, but they are all constructed by finite application of successor to zero.  So the constructors summarize our infinite set of values of the datatype.

If we are in the mindset — as we are here in Cedille land — of not taking constructors and datatypes for granted, we might ask: but how do you know you correctly summarized that infinite set of values using your functions you call constructors (since with a lambda encoding, the constructors are just more lambda terms, not different in kind from all the others you are using).  My intuition about reflection is that it contributes an essential property towards knowing you have the correct summary of your infinite set of data.  You offer some set of functions and claim that all the data can be built using those.  For this to be correct, we would reasonably expect that doing an elimination with a piece of data and those functions should rebuild that piece of data.  Otherwise, what kind of a representation scheme is it that one has?  Perhaps your functions define some permutation of the data?  So eliminating l with your functions f and x would result in a different list l’?  At least this seems exotic.  And maybe one could argue that if reflection does not hold, then parametricity will not give you induction, except for predicates that respect your representation scheme (i.e., for predicates where the elimination does act like the identity).

So for purposes of deriving induction from parametricity, I guess we can say that reflection is telling us that our representation scheme is universal: any predicate we can prove from parametricity will also hold inductively.

Writing this out suggests the intriguing possibility that using different representation schemes, one could  derive induction for predicates respecting the scheme, without needing reflection.  Or similarly, one could demand, in the statement of induction, that the predicate one is proving respects reflection, and then reflection would not need to be proved once and for all.

Hope you are in good health, and thanks for reading.

 

I decided to start recording a podcast, called “The Iowa Type Theory Commute”.  I don’t have the podcast listed in any directories yet, but you can find it on my web page here:

http://www.cs.uiowa.edu/~astump/ittc.html

The RSS feed is:

https://feeds.buzzsprout.com/728558.rss

Just one episode is there at the moment, but I will record some more soon.  I am thinking that some episodes will be more specialized, but the first is for a very general audience.

 

Here at Cedille HQ, we are still beavering away on … wait for it … lambda encodings!  Seriously?  You guys only do this?  Well, if you asked me five years ago what would I be (still) working on five years in the future I would not have said lambda encodings.  But maybe I would not have said “not lambda encodings” (I would have said, though, for dang sure, “not deep learning” :-)).  Well, the reason we have to spend all this time on lambda encodings is that they determine the kind of terminating programs you can write in Cedille, where all data are lambda encoded and recursion is implemented just using the lambda encoding (so there is no recursion built in primitively to the system; rather, it is defined using a terminating fragment of pure typed lambda calculus).  And if you asked me, do you think you will still be interested in programs — say software — in five years, I would have said emphatically yes — but not Software 2.0.  🙂

So what is a recursion universe?  I hope I reveal something of my personality if I write that I think the name sounds super cool.  🙂  A recursion universe type-theoretically is a view R of an inductive datatype C, together with some operations on R that preserve termination in the presence of structural recursion.  So the type R with those operations is an interface you can use when you are writing a structurally recursive (so terminating) function.  Recursive calls may only be made on elements of type R.  The interface permits you at least to escape the universe by converting a value of type R to C (at which point you cannot recurse on it any more) — this is what is meant by saying R is a view of C (I hope I have my terminology correct there on “view” — please comment if you think I have it scrambled).

Cedille 1.2 (current version) supports histomorphic recursion by — from the perspective of recursion universes — providing a recursion universe that has an operation out of type R -> F R, where F is the type scheme determining the datatype (so for Nat it would be λ X : ★ . Sum Unit X).  Extracting subdata of type R from a value of  type R is a termination-preserving operation: I cannot write a diverging function by structurally recursing on subdata of subdata if I was allowed to recurse on subdata.

This is a very simple recursion universe, but already it lets us express functions that go beyond what you can naturally write in Coq and Agda.  Division by repeated subtraction using the out function to dig into the dividend (by subtracting the divisor) and still return something of type R, which the function can then recurse on.  Cool!

The realization this past week was that we could hope to define more interesting recursion universes that would allow us to implement other patterns of terminating recursion.  The one I have been after for one year now is divide and conquer, such as is needed for classic mergesort (split the input list roughly in two halves, recurse, then merge).  Splitting the list in two halves and then recursing on the halves is not something you can do in Coq and Agda without reasoning about sizes.  The goal here is to use non-dependent typing only, in order to enforce termination.

Well, having answered the first question in the title, I must leave you hanging for an answer to the second: I have some more work to do to extend Cedille’s recursion universe beyond just out.  I can tell you that I do have an extension, but I am working on a more general one before I post again about this.

I first was keyed into this article of David Turner (see also this nice blog post about it) by a comment somewhere online (can’t find it now) from Conor McBride.  Between functional programming as we know and love it in Haskell, OCaml, even untyped variants like Racket, on the one hand; and mighty type theory (TT) on the other, there is strong FP.  What a great idea!  In Strong FP, we are interested in termination of programs, just like in constructive type theory based on the Curry-Howard isomorphism.  But unlike in type theory, termination is the only property we care about beyond those established by usual static typing.  Strong FP does not make use of dependent types, for example.  It is an intermediate point between FP and TT.

I was really happy to learn about the identification, by Turner, of this intermediate point.  This is partly for reasons of personal history.  I first programmed, as a boy, in BASIC, then some Pascal, and then the appalling C++ (genetic algorithms, in high school).  In college I learned Scheme (those were the good old days) and Java, and then in grad school it was back to C++ to implement most of the first version of the CVC SMT solver.  Awful coding experience to write so much C++ for symbolic manipulation.  Then I discovered … was it OCaml? Haskell? No, a formalism coming from term rewriting called the rho-calculus.  The parts I think I was drawn to were accomplishing what we usually use datatypes and pattern-matching for in functional programming.  So then as an assistant professor it was OCaml, also Coq along the way.  As an associate professor it was Agda, and finally now Haskell is my language of choice for everyday programming.  Of course, I have been working on developing my own languages, with Cedille being by far the most interesting and successful attempt.

What I want to share from this little history is that I came to functional programming from more mainstream programming, and eventually became convinced of its superiority for expressing computational ideas elegantly and concisely.  FP is great!  And Strong FP is greater!

Why do I think Strong FP is even better than FP?  Again, it is coming from personal experience.  When I moved from programming in C++ to OCaml, it was such a fantastic experience.  As I got used to OCaml for language implementation, pattern-matching, type inference, recursion, and such were just such a perfect fit and resulted in such nice code, I couldn’t believe how great it was.  I had heard about this Haskell language, and the fact that you had to use some abstraction called monads to do IO.  I thought this was absurd.  IO is basic to programming, and the fact that some elaborate scheme is required for it in a language to me was almost a reductio ad absurdum for that language.

But then I actually tried writing some pure functional programs for things I cared about.  At first it was rather hard and unintuitive, but when I finally got my code (I do not remember what this was for, but I have a distinct recollection of the experience) through the compiler (and it might have been Agda at that point instead of Haskell, I don’t remember), it just worked.  It was tricky and maybe I even had some bad experience writing it in OCaml using mutable data structures — or maybe I just wrote it in pure style in OCaml.  The details are lost to my memory.  But the important point is not: despite the fact that it seemed like a straightjacket, pure FP led to a better solution to my problem.

And if you think pure FP is pure, wait till you get a load of strong FP, which is just pure FP with a requirement of uniform termination for your programs (they have to terminate for all inputs).  If FP shows that more restrictions — deeply motivated, natural, elegant restrictions — leads to better code, strong FP could be expected to do this even more.  Even if not, we get static assurance of termination, which could be a big improvement to code quality (and Turner provides other arguments in favor).

If this is such a great idea, why haven’t we all heard about strong FP and why isn’t there -XStrongFP for ghc?  I do not know the social history or anything like that, but on the technical side, it looks like there is a simple explanation: strong FP has to bite off the part of TT that has caused some of the most difficulties, namely termination checking.  The requirements Turner lists for recursion and inductive data are (1) primitive operations must be total (no problem if we have none!), (2) only positive recursive types are allowed (yes, we know this one well from TT and it creates some headaches but nothing too terrible), and (3) recursion must be structurally decreasing.  It is (3) that is quite brittle and has led to interesting research on, for example, type-based termination.   I glanced at a later paper of Turner’s on strong FP, and there was a fancier version of (3), but still it requires some syntactic check on program code separate from typing.

I believe that strong FP can make an exciting surge forward if it is type-based.  But not in the sense of Barthe et al., and others (Abel comes to mind), where, at a high level, we enrich types with sizes of data structures, and use recursion on those sizes to ensure termination.  This approach will not work for strong FP, if we conceive strong FP as by design something weaker than TT.  Let us not allow ourselves dependent or term-indexed types (no refinement types, nothing like that).  We essentially just have System F (or F-omega, or something similar), and we want to use typing to ensure termination.  Is this possible?

Of course  it is!  System F’s types ensure termination already. But we don’t want to program with Church-encoded data in pure lambda calculus.  We would like to use familiar notation for pattern-matching and recursion.  Of course we understand the recursion has to be restricted somehow to ensure termination.  And I am saying that we should set ourselves the goal of using typing — without dependent types — for such restriction.  Can this be done?

No.  Wait, yes, of course, that’s why I am leading into this this way.  In Cedille, we have implemented a (type-based) form of histomorphic recursion, based ultimately on Mendler-style lambda encodings of data, which have efficient accessors; but this is not actually relevant for considering the interface.  It is sufficient to understand that we have a proof of termination for any term whose type is a datatype (and this is enough, since recursive functions must then terminate since any call to them that produces a value in a datatype is terminating).  And this type-based histomorphic recursion is a big extension in practical expressive power to syntactically checked structural recursion.  When you are coding a pattern-matching recursion in Cedille for some function F, in the various clauses for F (that is, the cases for different forms of the inductive data you are doing a pattern-matching recursion on), you get the following:

  • a type Type/F, which abstracts (hides) the datatype;
  • a function F which takes in something of that abstract type Type/F, and then returns whatever you are defining F recursively to return; and
  • evidence that Type/F is D-like, where D is the datatype you are matching on, and being “D-like” allows you to:
    • pattern-match on the data
    • cast the data back to type D.

This interface has nothing to do with sizes of data structures.  And yet it is sufficient to code some quite tricky examples.  We can do natural-number division this was as iterated subtraction.  Ok, that is not too tricky but in Coq and Agda the code uses a four-argument function that merges subtraction and division so the termination checker can verify it is terminating.  Yuck.  We can do a form of mergesort, which is definitely in the realm of trickier.  In Agda this is done with sized types.  The challenge problem we just managed to solve as a strong functional program using Cedille’s histomorphic recursion is Harper’s continuation-based regular expression matcher, which has been posed as a challenge problem by several researchers in the theorem-proving community.  Coq has a solution, for example, that requires reasoning about the size of the list that is being consumed by the matcher, particularly as one calls the continuation.  Our solution does not use dependent types at all.  So in some sense, there is no termination reasoning.  Instead, one has to code to the above interface, which certainly is tricky in this case, but again, requires no formalized reasoning about terms and functions.  It just requires programmer ingenuity to figure out how to fit your algorithm into that interface.

Well, I’ve been going on enough about this.  Hope all is well with any QA9 readership making it this far.  🙂

 

I was very pleased to be invited to give an invited talk at the LOLA 2019 workshop.  My slides and the screencast talk are here and here.