varsigma : lambda :: ___ : arrow

(figured I'd have put this question here, since its something that we may go back and forth on, and the latex document is not for that)

This is regarding the following interaction:

\fmarnote{What/where is some arrow type $\leadsto$ such that
  $\varsigma$:$\lambda$::$\leadsto$:$\to$?  It seems it may be $[l_i : B_i]$,
  since label reference \emph{is} invocation.  If true, we may do well to
  explicitly point this out.}

\cmarnote{What the heck are you talking about?  I don't understand this at all.}

My point was this: in the type systems for the lambda calculus, there is the very important type constructor, arrow, which is the essence of how we abstract over the behavior of an actual term, by describing it as belong to a "function space." So that's what the arrow type constructor is for.

My question was, what is the corresponding essential type constructor in Jim and Palsberg system? The object language doesn't have the same sort of beta reduction that we're used to seeing (its there, sort of, its just hidden). So it wasn't immediately clear to me what the corresponding type constructor was.

My current hypothesis is that $[l_i : B_i]$ is the type I'm looking for; this describes an object which, when asked for the result of its l_i method, will return an object of type B_i. But this is only a hypothesis, and while it makes things clearer for me, you're the one writing this section, so I thought I'd ask you about it (and suggest that you add some sort of explanation along these lines, so that the reader can use their knowledge of the lambda calculus as leverage in understanding the varsigma calculus).

If you think such an analogy hurts more than it helps, that is fine. It was just a stray thought I had while on the plane, and it took me long enough to come up with an answer I was happy with that I thought I should bring it up.