[TYPES] Time for types-as-arithmetic, by analogy with types-as-propositions?

[Fritz Ruehr]

Over the last few years I have noticed a trend of research which draws an analogy between
types (on the one hand) and numbers and arithmetic (on the other): "type arithmetic" 
(calculation of type isomorphisms), derivatives of data types, generating functions and 
power series related to types, etc. (Details and references are relegated below.) 

I wonder if it is time for more overt recognition of a "types-as-arithmetic" analogy, 
like the celebrated types-as-propositions correspondence.

Does anyone else recognize this as a trend? Do you think it is worthy of more focused 
attention, or even just a better, community-endorsed slogan? 

On a more formal level, types (under iso-equivalence), propositions and arithmetic all fit
into (versions of) Tarski's "high school identities", as models of an abstract algebra with
a nice, structured axiomatization. I have used the pithier term "power rings", since they 
extend a commutative semi-ring (for sums and products) with exponentials and related laws 
(e.g., corresponding to currying and to categorical sums and products). (There are, 
of course, problems with bottom / non-termination in some computational interpretations, 
just as for Curry-Howard^H^H^H^H, uhh, types-as-propositions.)

Am I merely glimpsing what others (more categorically sophisticated, no doubt) take for 
granted? Is there an existing terminology for (or a more elaborated literature around)
this analogy between types and arithmetic? Perhaps this is all just about bicartesian closed
categories, but I don't see differentiation and some other ideas described in this context.

In addition to reactions on the general idea, I would also appreciate any pointers to other 
work which might fall under this rubric.

  --  Fritz Ruehr

--------------------------

Ideas, papers and blog posts that exemplify the "types-as-arithmetic" trend include:

* The folklore idea of "type arithmetic", in which one calculates types equivalent up to
  isomorphism by using the usual "high school identities" about addition, multiplication 
  and exponentiation, but interpreting them in terms of disjoint sum, cartesian product
  and function space.
  
* Roberto Di Cosmo's use of these equivalences in his work on type isomorphism [DiC95] 
  (he specifically recognized the relevance of Tarski's identities in this context).

* Application of type arithmetic to the memoization of functions as tries in work by Ralf 
  Hinze [Hin00ab]; see also related work and extensions by Conal Elliott [Ell08] and 
  Dan Piponi [Pip09a].
  
* Conor McBride's work on the differentiation of data types [McB01], where the usual rules 
  for derivatives are re-interpreted for types and shown to correspond to the notion of 
  datatype context used in Huet's zipper construction (see also Conor's "Clowns and
  Jokers" work on dissection [McB06], which Dan Piponi recognizes [Pip09b] as corresponding 
  to finite differences).
  
* Notions of subtraction, division and differentiation for the combinatorial species of Joyal 
  [Joy81]; species can in some ways be seen as an extension or generalization of algebraic 
  datatypes. See Brent Yorgey's Haskell Workshop paper [Yor10a] and his blog [Yor10b] for an
  introduction to species in the context of functional programming and to "virtual species" 
  in particular. Subtraction and division are apparently definable for types by the same 
  Grothendieck construction which generalizes the extension of the naturals to the integers 
  and rationals.

Parts of this "trend" go back much further than the past few years: already in William Burge's
book "Recursive Programming Techniques" [Bur75] we see the use of generating functions and 
power series as a way to think about data types. (There is apparently some related work by
Corrado Boehm and Maria Dezani-Ciancaglini [BDC74] dating to 1974, although I don't have easy 
access to a copy.)

I have myself advocated for a more explicit use of "type arithmetic" in the pedagogy of 
functional programming [Rue08], as well as for more recognition and study of the
corresponding abstract algebra I call "power rings".

References:

[BDC74] A data structure formalization through generating functions. Corrado Boehm and Maria
	Dezani-Ciancaglini, Calcolo vol. 11(#1), Springer, 1974.

[Bur75] Recursive Programming Techniques, William H. Burge, The Systems programming series, 
	Addison-Wesley, 1975.
	
[diC95] Isomorphisms of types: from lambda calculus to information retrieval and language 
	design. Roberto Di Cosmo, Birkhauser, 1995.

[Ell08] Elegant memoization with functional memo tries. Conal Elliott, blog post at URL
	<http://conal.net/blog/posts/elegant-memoization-with-functional-memo-tries/>, 2008.

[Hin00a] Generalizing generalized tries. Ralf Hinze, Journal of Functional Programming, 
	vol. 10(#4), Cambridge, 2000.

[Hin00b] Memo functions, polytypically! Ralf Hinze, WGP '00 (Ponte de Lima), ACM, 2000.

[Joy81] Une theorie combinatoire des series formelles. Andre Joyal, Advances in Mathematics
	vol 42, 1981.

[McB01] The Derivative of a Regular Type is its Type of One-Hole Contexts. Conor McBride,
	available from the author's page at <http://strictlypositive.org/publications.html>, 2001.

[McB06] Clowns to the left of me, jokers to the right. Conor McBride, available from the 
	author's page at <http://strictlypositive.org/calculus/>, 2006.

[Pip09a] Memoizing Polymorphic Functions with High School Algebra and Quantifiers. 
	Dan Piponi (sigfpe), A Neighborhood of Infinity, blog post at URL
	<http://blog.sigfpe.com/2009/11/memoizing-polymorphic-functions-with.html>, 2009.

[Pip09b] Finite Differences of Types. Dan Piponi (sigfpe), A Neighborhood of Infinity, 
	blog post at URL <http://blog.sigfpe.com/2009/09/finite-differences-of-types.html>, 2009.

[Rue08] Tips on Teaching Types and Functions. Fritz Ruehr, FDPE '08 (Victoria), ACM, 2008.
	
[Yor10a] Species and functors and types, oh my! Brent Yorgey, Haskell '10 (Baltimore), ACM, 2010.

[Yor10b] Species subtraction made simple. Brent Yorgey, blog :: Brent -> [String], blog post
	at URL <http://byorgey.wordpress.com/2010/11/24/species-subtraction-made-simple/>, 2010.