Rational Types

The paper entitled “The Two Dualities of Computation: Negative and Fractional Types” (by Roshan James and Amr Sabry) presents negative and fractional types, as an addition to standard algebraic datatypes (void, unit, sums and products, mostly). The paper suggests that negative and fractional types have been misunderstood in previous works and that, while both present types of continuations, they have different meanings (the easy-to-understand explanation is debit vs credit debt). The authors extend an interesting language that they have previously created, whose semantics are based on isomorphisms with negative types presenting backtracking, and fractional types presenting constraint propagation.

Whether backtracking and constraint propagation can be considered the same thing, and why we observe negative and fractional types differently in terms of why the paper suggests that fractional types introduce a fresh logic variable while negative types don’t (I think this has to do with one of them starting with the void type, and the other the unit, but can’t prove it either way) is an interesting debate that I would like to ask the authors about.

Presentation

Here’s a presentation that tries (and fails) to explain the paper better.

Implementation

I’ve implemented the base pie language like the paper suggested. It is in this repo for anyone to inspect and upgrade.