Towards not mixing signatures in ...

[Patrik Eklund <peklund@cs.umu.se>]

We have been working with "levels of signatures" and thereby been
puzzled about the way type theory seems to have alternate solutions for
Church's 'o' type which appears in his 1940 paper. There seems to a
"consensus in intuition" about Church's 'iota' type, but indeed, the 'o'
type has been treated differently, even by the same authors over times.

Below I try to express my point and I need to choose context and
language in order to make myself as clear as possible. I choose notation
in Agda for this purpose.

I was reading the reference manual of Agda, and the "inductive data type
declaration". I looks to me that it mixes "levels of signatures".
Similarly, type theory in general, including lambda-calculus,
Martin-L??f's type theory, and Homotopy Type Theory, mixes levels of
signatures, or simply doesn't care about that mixture. It is almost like
making the 'o' "untyped".

The declaration

    data Nat : Set where
      zero : Nat
      suc : Nat ??? Nat

defines not just the ordinary Sigma_NAT = (S, Omega) signature, where S
= {Nat} and Omega is

      zero : Nat
      suc : Nat ??? Nat

but it also says that "Nat is Set". This "Set" should then be what
Church denoted as iota in his 1940 paper.

Then it seems to me as '???' in

      suc : Nat ??? Nat

is not the same '???' as in

      add : Nat ??? Nat ??? Nat

where the latter is a lambda term on "another level" as compared to the
former.

In the latter, the '???' is the "function type constructor", which is an
operator on the level of signatures where 'Set', i.e., Church's iota
resides. Denoting this type constructor as '==>', I would have

      ==> : Set ??? Set

on the signature level residing "between" the "primitive level" and the
"lambda level".

This formalization of "levels of signatures"

http://www.glioc.com/files_glioc/ModernEyesOnLambdaCalculus.pdf

requires a strict definition of the category of signatures, and a formal
construction of term monads:

http://www.sciencedirect.com/science/article/pii/S0165011413000997

Generally, I feel 'o' is hard because it reflects "sentence", not
"term". A term has a type given its construction from operators using
sorts, but a sentence "having a sort" is another story. Terms involve
possibilities for composable substitutions, whereas sentences do not
allow for composable "substition" because sentence functors are
"non-monadic". Term functors are monadic.

I wonder if anybody would care to comment.

Best regards,

Patrik

-- 

Prof. Patrik Eklund
Ume?? University
Department of Computing Science
SE-90187 Ume??
Sweden

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

mobile +46 70 586 4414
website www8.cs.umu.se/~peklund
Skype patrikeklund
Virtual office: https://connect.sunet.se/patrikeklund/


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]