negative and fractional types?

[Henry Story]

Hi,

I was just watching the great introduction videos to category theory
by Bartosz Milewski [1], which is a delight to a programmer like me.

Anyway in the session one Algebraical datatypes he explains that one can do
most of what one does in high school algebra with types. Except that types form
a semi-ring and so it is not clear what division and fractions are, even though
they seem to work.

In the notes on that talk someone pointed to
"The Two Dualities of Computation: Negative and Fractional Types"
by Roshan P. James and Amy Sabry
https://www.cs.indiana.edu/~sabry/papers/rational.pdf

Before I get lost in that, I just wanted to ask what the HoTT answer
was for that, and as an extra if it meshes with that paper (which
I noticed has not been cited that much)

Henry


[1] which I really recommend
https://www.youtube.com/user/DrBartosz/videos

[Gershom B]

The negative and fractional types work presents a different type
system than the MLTT-based one in HoTT, for a language with a very
different view of "computation". There is some recent work that
relates the reversible approach (in general, but sans an explicit
computational interpretation of negative and fractional types -- i.e.
restricted to the semiring fragment) to univalent universes: "From
Reversible Programs to Univalent Universes and Back", Jacques Carette,
Chao-Hong Chen, Vikraman Choudhury, Amr Sabry,
https://arxiv.org/abs/1708.02710

--Gershom

> --
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Jacques Carette]

Right.  And you'll notice that the James-Sabry paper was never
published. That's because the type system presented there 'collapses'
and the only model is a singleton.

I've continued to work with Amr on negative and fractional types. We
have lots of speculative Agda code -- some of which even exhibits types
whose natural Groupoid interpretation has a fractional cardinality.
[Negative types still elude us].  This has also not been published,
because the referees thought what we exhibited was a theoretical oddity
and wanted more practical interpretations. They weren't wrong... our
construction achieved our aims, but was otherwise short of compelling.

We're still looking.

Note that a more combinatorial approach to 'types, namely Joyal's theory
of Species, does exhibit negative and fractional structures. However,
these are somehow outside the Species framework -- one can form a Ring
of Virtual Species (i.e. w/ negatives), but this is quite disappointing
since one would expect more categorical structure (i.e. 1-algebra
structure) rather than just 0-algebra structure.  People (see various
posts on MathOverflow) have speculated about certain categories of
cobordisms being able to fill in the gaps, but no one has yet (to my
knowledge) worked out the details.

I've been working on this problem for close to 4 years now, and I would
say that the problem is still wide open.

Jacques