Notes from a Medium-Sized Island [entries|archive|friends|userinfo]
Jason

 [ website | My Website ] [ userinfo | livejournal userinfo ] [ archive | journal archive ]

 [Oct. 19th, 2003|05:31 pm] Jason Question for the types crowd:Let Δ be the type of functions f : nat -> nat such that f(x) <= x. This can be thought of as the infinite product type 1 x 2 x 3 x 4 x ... or a dependent product or whatever you prefer.Now the idea of having a type operator which is somehow "a thing that takes τ to Δ x exp(τ)" where exp is to be read as, yes, the exponential function, is not such a crazy thing if we think of power series. Say Δ(i) is the "ith truncation" of Δ (i + 1) x (i + 2) x ... So we could sayΔ x exp(τ) = Σi Δ(i) x τi(to reflect the power series exp(x) = 1 + x + x^2/2! + x^3/3! + ...)Now we also have a nice power series for -ln(1-x), 1 + x + x^2/2 + x^3 / 3And moreover -ln(1-x) = ln(1/(1-x)), and α list is a reasonable interpretation of 1/(1-α) since it is the type solution of β = 1 + α x β just as 1/(1-x) is the solution of y = 1 + xy.In this way we can come up with a reasonable interpretation in types of Δ x ln(τ list), asΣi Δ'(i) x τiwhere Δ'(i) is the infinite product 1 x 2 x 3 x 4 x ... with the ith term absent.Given all this nonsense, one might therefore hope, by way of hand-waving and "algebra", that the typeΔ x (Δ x σ -> τ list)(where the arrow is the function type constructor, think of it as an exponentiation) might somehow be related to the typeΔ x exp(Δ x ln(τ list) x σ)Ideally by an isomorphism, but I doubt things work out that cleanly. Any ideas how to do this? I have this vague feeling that someone already did this sort of thing in the literature. Link Reply

From:
2003-10-19 02:41 pm (UTC)

### two types of people...

There are two types of people in this world: those who seperate people into two types, and those who don't.

Sorry, couldn't resist!
 From: 2003-10-19 06:59 pm (UTC) (Link)
How are you identifying f: nat \to nat with an element of that infinite product, or a dependent type? Other than that it seemed like it could be interesting. I really liked your motivation for defining ln (\tau list) in that way, very pretty. How does one get the \tau letter that you used?
 From: 2003-10-20 02:44 am (UTC) (Link)
It appears to simply be &tau;: τ.
 From: 2003-10-20 07:53 am (UTC) (Link)
Terms at the infinite product type are infinite tuples. Identify the nth slot of the tuple with the function's output f(n). The fact that the nth slot of the tuple has type n (thought of as {0,...,n-1}) corresponds to the restriction that f(n) <= n.
From:
2003-10-20 12:31 am (UTC)

### I lack the brain to read this now if ever but

you caught Andreas Blass's paper and the POP talk last year on imaginary types?