BEGIN:VCALENDAR VERSION:2.0 PRODID:-//Talks.cam//talks.cam.ac.uk// X-WR-CALNAME:Talks.cam BEGIN:VEVENT SUMMARY:Excuse My Extrusion - Conor McBride\, Mathematically Structured Pr ogramming Group\, Department of Computer and Information Sciences\, the U niversity of Strathclyde DTSTART:20160219T140000Z DTEND:20160219T150000Z UID:TALK63138@talks.cam.ac.uk CONTACT:Ohad Kammar DESCRIPTION:Writing this in mid-December\, I can promise only a classical tale of triumph or disaster which I hope to have made constructive by mid- February. I have recently begun to learn about the Cubical Type Theory of Coquand et al.\, as an effective computational basis for Voevodsky's Univa lent Foundations\, inspired by a model of type theory in cubical sets. It is in some ways compelling in its simplicity\, but in other ways intimidat ing in its complexity. In order to get to grips with it\, I have begun to develop my own much less subtle variation on the theme. If I am lucky\, I shall get away with it. If I am unlucky\, I shall have learned more about why Cubical Type Theory has to be as subtle as it is.\n\nMy design separat es Coquand's all-powerful "compose" operator into smaller pieces\, dedicat ed to more specific tasks\, such as transitivity of paths. Each type path Q : S = T\, induces a notion of value path s {Q} t\, where either s : S\, or s is &bull\;\, "blob"\, and similarly\, t : T or t = &bull\;. A "blob" at one end indicates that the value at that end of the path is not mandate d by the type. This liberalisation in the formation of "equality" types al lows us to specify the key computational use of paths between types\, extr usion:\n\nif Q : S = T and s : S\, then s &frown\;&bull\; Q : s {Q} &bull\; \n\nThat is\, whenever we have a value s at one end of a type path Q : S = T\, we can extrude that value across the type path\, getting a value path which is s at the S end\, but whose value at the T end is no t specified in advance of explaining how to compute it. Extrusion gives us a notion of coercion-by-equality which is coherent by construction. It is defined by recursion on the structure of type paths. Univalence can be ad ded to the system by allowing the formation of types interpolating two equ ivalent types\, with extrusion demanding the existence of the correspondin g interpolant values\, computed on demand by means of the equivalence.\n\n So far\, there are disconcerting grounds for optimism\, but the whole of t he picture has not yet emerged: I may just have pushed the essential compl exity into one corner\, or the whole thing may be holed below the waterlin e. But if it does turn out to be nonsense\, it will be nonsense for an int eresting reason.\n LOCATION:FW26 END:VEVENT END:VCALENDAR