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

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

[Oct. 19th, 2003|05:31 pm]
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 / 3

And 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 τi

where Δ'(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.

[User Picture]From: amuzulo
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!
(Reply) (Thread)
[User Picture]From: bastetsguardian
2003-10-19 06:59 pm (UTC)
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?
(Reply) (Thread)
[User Picture]From: rjmccall
2003-10-20 02:44 am (UTC)
It appears to simply be &tau;: τ.
(Reply) (Parent) (Thread)
[User Picture]From: jcreed
2003-10-20 07:53 am (UTC)
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.
(Reply) (Parent) (Thread)
From: eub
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?
(Reply) (Thread)
[User Picture]From: jcreed
2003-10-20 07:51 am (UTC)

Re: I lack the brain to read this now if ever but

Yeah, it's exactly that kind of thing that inspires me to such horrors.
(Reply) (Parent) (Thread)