2020-05-20: Fixed-point operators from recursive types I rak ================================================================ I was reading Marcelo Fiore's PhD thesis this afternoon [0] and came across the following remark: "In the sequel recursion at the level of programs is not considered primitive, instead our viewpoint is that it arises from recursion at the level of types." I've heard many times over the years that you can do this, but I never sat down and worked out how to encode fixed point operators using recursive types. So here it goes. ---------------- - The language - ---------------- Assume we have a language containing the following rule defining a fixed-point operator: G, x : t |- e : t -------------------- (fix) G |- fix(x.e) : t where operationally, ---------------------------------- . fix(x.e) ~~> [fix(x.e) / x] e Also suppose that our language has isorecursive types [1] given by: G |- e : pa.t ---------------------------- (unfold) G |- unfold e : [pa.t/a]t G |- e : [pa.t/a]t ---------------------------- (fold) G |- fold e : pa.t with dynamics ---------------- , fold(v) value ------------------------ , unfold(fold(e)) ~~> e and e ~~> e' --------------------------- . unfold(e) ~~> unfold(e') We also assume abstraction / application: G, x : t |- e : t' ---------------------- (abs) G |- \x.e : t -> t' G |- e : t -> t' G |- e' : t ------------------------------------- (app) G |- ee' : t' with a call-by-value (or CBN if you want) dynamics: ------------- , \x.e value v value --------------------- , (\x.e)v ~~> [v/x]e v value e ~~> f ---------------------- , ve ~~> vf e ~~> f ------------ . eg ~~> fg ---------------- - The encoding - ---------------- We can encode fix(x.e) as f(fold(f)) where f = \y.[(unfold(y))y/x]e. First, this is well-typed: ------------------------------- (var) y : pa.a -> t |- y : pa.a -> t --------------------------------------------- (unfold) ------------------------------ (var) y : pa.a -> t |- unfold(y) : (pa.a -> t) -> t y : pa.a -> t |- y : pa.a -> t -------------------------------------------------------------------------------------- (app) y : pa.a -> t |- (unfold(y))y : t so using substitution / cut we get G, x : t |- e : t -------------------------------------------- (subst) G, y : pa.a -> t |- [(unfold(y))y/x]e : t ----------------------------------------------- (abs) G |- \y.[(unfold(y))y/x]e : (pa.a -> t) -> t where we recognize the term in the bottom as f. Call the above derivation D1. We also get D1 D1 -------------------------- (fold) G |- f : (pa.a -> t) -> t G |- fold(f) : pa.a -> t -------------------------------------------------------- (app) G |- f(fold(f)) : t So we see that our encoding at least has the right type. Next we check that it has the right operational behaviour: fix(x.e) === f(fold(f)) ~~> [(unfold(fold(f))fold(f)/x] e ??? [f(fold(f))/x] e === [fix(x.e)/x] e The question is, how do I show the step labelled '???'? To be continued... [0] Fiore, Marcelo P., "Axiomatic Domain Theory in Categories of Partial Maps", PhD thesis, The University of Edinburgh Department of Computer Science, October 1994, v+282 pp. [1] I'm punning on the visual resemblence between 'p' and the non-ASCII greek letter rho, which is my preferred binder for recursive types.