Jason (jcreed) wrote,

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.

  • (no subject)

    After getting home from work immediately appeared to be a traintastrophe in the making, went to see Esther Schor talk about her book "Bridge of…

  • (no subject)

    Went to a series of maker-y talks hosted by Pivotal. The last one, by the woman who runs Genspace, "New York City's Community Biolab" was pretty…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded