[PL-sem-jr] Followup on today's talk

[Vasileios Koutavas]

On Tue, 19 Oct 2004, Felix S Klock wrote:

> 
> On Oct 19, 2004, at 7:08 AM, Vasileios Koutavas wrote:
> > 1) non-recursive equations don't work: s_0 = s_1 -> s_2
> > 2) even recursive equations don't work: s_0 = s_1 -> s_0
> > 3) but there are other recursive equations that work (at least for 
> > typing
> > Omega):
> >      s_0 = s_0 -> (s_0 -> s_0)
> > and more generally:
> >     forall s_1.  s_0 = s_0 -> s_1
> >
> > I don't know if #3 can type arbitrary terms because it can type Omega, 
> > and
> > barendregt's one-line justification of why s_0 = s_0 -> s_0 does, 
> > makes me
> > think that #3 probably doesn't have this power.
> 
> If I'm understanding your notation, your #3 is something like the 
> following:
> 
> sigma_#3 = mu alpha . (alpha -> (alpha -> alpha))

I basically talked about equations of types, and not the types themselves. 
So #3 (the 3rd case study) says that any type that satisfies the equation:

	sigma_0 = sigma_0 -> sigma_1	(general case)

can type Omega. Of course sigma_0 = mu alpha. (alpha -> (alpha -> alpha)) 
is a solution to this equation.

Note that the types that satisfy this recursive equation need to have 
recursion only in the argument. eg: sigma_0 = mu alpha. (alpha -> beta) 
also satisfies the equation (from what I understood)

> 
> And yes, I believe that this does have a derivation for Omega : sigma_#3
> 
> 1. My intuition here is this:
> sigma_0 = (mu alpha . (alpha -> alpha))  is able to type everything 
> because you can expand AND retract it to fit whatever you are trying to 
> type.
> sigma_0
> approx (sigma_0 -> sigma_0)
> approx ((sigma_0 -> sigma_0) -> sigma_0)
> approx (sigma_0 -> (sigma_0 -> sigma_0))
> approx ...
> 
> So for whatever closed term you hand me, I'll just expand sigma_0 to 
> fit it.  [[ Not a formal proof, just my intuition here ]]
> 

By playing with possible equations of which their solutions can type 
Omega, I saw that you only need recursion in the argument. But is this 
powerfull enough for all other closed terms?

I think the answer here is in domain theory, which is where barendregt 
refers to, to explain why sigma_0 = sigma_0 -> sigma_0 types all terms 
(page 167, before def 4.1.9)


> 2. sigma_#3 = (mu alpha . (alpha -> (alpha -> alpha)))
> should also be able to type arbitrary terms; its infinite tree is the 
> same as the infinite tree for sigma_0, which satisfies the definition 
> of approx.
> 
> I admit that this was not my initial intuition about sigma_#3 though.  
> At first I agreed with you that it would not be able to type all terms. 
>   But now I think it can.
> 
> I am now curious about whether there are versions of lambda-mu which 
> distinquish between sigma_#3 and sigma_0, perhaps by putting the 
> individual folds and unfolds into the type derivation itself, rather 
> than shoving them all into a coinductively-defined helper function.  
> Maybe I'll ask Mitch about that.
> 
> 3. There's still the important lesson that these recursive types that 
> we're showing can type any term are not necessarily the *principal* 
> types for the terms they are typing.  Boy, now I really wish I had a 
> chance to give the formal definition for principal types.
> 
> A principal type for M is a type sigma where
> 1. |- M : sigma
> 2. (  |- M : tau  )     implies     Exists a substitution S where 
> S(sigma) = tau
> where a substitution replaces type variables with types (which are 
> possibly just type variables themselves).  See Barendregt's chapter for 
> the gory details.
> 
> Now take K = \xy.x for example.  A principal type for K : alpha -> beta 
> -> alpha.
> 
> But you could easily prove that K : sigma_0 -> (sigma_0 -> sigma_0)   
> [[ this comes as no surprise; just substitute sigma_0 for alpha and 
> beta in the above principal type for K) and thus by retracting twice we 
> get K : sigma_0.
> 
> But K : sigma_0 is *not* a principal type for K; there are lots of 
> other types for K that are valid that we cannot find simply by 
> substituting types into free variables in sigma_0, because there are 
> *no* free variables in sigma_0.  Any substitution on sigma_0 is going 
> to just yield. . . sigma_0.
> 

No objection here. I'm just wondering what is the principal type of 
(\x. x x).

I suspect that principal types are orthogonal to recursive types and maybe 
we sould see them seperately. By the way, where does barendregt mentions 
principal types? It's kind of a pain to spot his subsections :-(

> -Felix


--Vassilis