Tony's Wiki

Encoding CP with distributive recursive types - refined

9 min read

TL;DR: If we want to close the fixpoint at top level when calling new, instead of closing fixpoint for each traits (which I presume will cause some problems with the operational semantics), due to the use of calling constructors from the self reference in implementing the doubleNum trait, we might need to use bounded polymorphism (to enable virtual constructors) + structural unfolding rule (to allow type parameters in unfold annotations) to achieve the desired compositional typing.

TOC

  • Compositional interfaces are the same:
  • [[#implementing-the-evalnum-trait-is-usual-does-not-require-self-reference|Implementing the evalNum trait is usual, does not require self-reference]]
  • [[#implementing-doublenum-requires-self-reference---v1|Implementing doubleNum requires self-reference - v1]]
  • Composition and type checking
  • [[#attempt-1---parameterizing-doublenum|Attempt 1 - parameterizing doubleNum]]
  • [[#attempt-2---parameterizing-doublenum—refining-with-intersection-types|Attempt 2 - parameterizing doubleNum + refining with intersection types]]
    • [[#Attempt 2 - parameterizing doubleNum + refining with intersection types#What can we do with the new typing? - does not help|What can we do with the new typing? - does not help]]
  • Attempt 3 - How about bounded polymorphism + structural unfolding?
    • [[#Attempt 3 - How about bounded polymorphism + structural unfolding?#Composition again: success?|Composition again: success?]]

After understanding the Trait compositions in CP, let’s refine the example presented in Encoding CP with distributive recursive types

Compositional interfaces are the same:

except that we are now adding a layer of mu to every (compositional) method interface

Source Language:

type NumSig<Exp> = { Lit : Int -> Exp; Add : Exp -> Exp -> Exp };
type IEval = { eval : Int };
type IDouble = { double : Self };

-- ** elaborates to:
type NumSig<Exp> = { Lit : Int -> Exp; Add : Exp -> Exp -> Exp };
type IEval = mu X. { eval : Int };
type IDouble = mu X. { double : X };



type IEvalDouble = IEval & IDouble 
	-- eval and double can be implemented on their own
				 <: mu X. ({ eval : Int } & { double : X } )
type IEvalDouble' = mu X. ({ eval : Int } & { double : X } )
	-- eval double needs to be mutually defined
	-- so IEvalDouble is a subtype of IEvalDouble'

-- Implication: maybe it is a good idea to keep interfaces defined as
--              IEvalDouble instead of IEvalDouble'
--              until all the compositions are completed 
--              (calling the `new` constrcutor)

Implementing the evalNum trait is usual, does not require self-reference

evalNum (self: Top) : NumSig<IEval> = {
   Lit (val: Int) = fold [IEval] { eval = val } ;
   Add (e1 : IEval ) (e2 : IEval) = fold [IEval] 
      { eval = (unfold [ IEval ] e1).eval + (unfold [ IEval ] e2).eval }
}

The only difference to current CP is that we add some dummy folds so the output type is a recursive type mu X. {eval : Int}

Implementing doubleNum requires self-reference - v1

In order to call the constructor, we have to use self reference in the doubleNum trait, so that we can call self.Lit, self.Add, …

doubleNum (self: NumSig<IDouble>) : NumSig<IDouble> = {
   Lit (val: Int) = fold [IDouble] { double = self.Lit (val + val) } ;
   Add (e1 : IDouble ) (e2 : IDouble) = fold [IDouble]
      { double = self.Add 
	      (unfold [IDouble] e1).double  
	      (unfold [IDouble] e2).double
}

-- Type checking `doubleNum`
-- { double = self.Lit (val + val) }  : { double : IDouble }
--		 fold [IDouble] { ..... }   : IDouble
--		(unfold [IDouble] e1).double : IDouble
--		unfold [IDouble] e1 : { double : IDouble }
--		e1 : IDouble

-- if we write the trait type, doubleNum has the type
--     Trait[NumSig<IDouble>, NumSig<IDouble>]

-- FYI:
-- NumSig<IDouble> = {
--    Lit : Int -> mu X. { double : X }
--    Add : mu X. { double : X }
--       -> mu X. { double : X }
--       -> mu X. { double : X }
-- }

Composition and type checking

We wish to compose the two traits

  • doubleNum : Trait[NumSig<IDouble>,NumSig<IDouble>] and
  • evalNum : Trait[NumSig<IEval>

However, in order to do so, we have to first close the doubleNum fixpoint into Trait[NumSig<IDouble>] and then merge Trait[NumSig<IEval>] & Trait[NumSig<IDouble>] in order to obtain the final type NumSig<IEvalDouble>.

e1 : NumSig<IEvalDouble> = 
	(fix [NumSig<IEval>] evalNum) ,, (fix [NumSig<IDouble>] doubleNum)

Question: can we instead write: (fix NumSig<IEvalDouble> (evalNum,,doubleNum))?

We get Trait[NumSig<IDouble>, NumSig<IEvalDouble>] from evalNum ,, doubleNum, this is not an instantiable trait! (provided type NumSig<IEvalDouble> is not a subtype of the required type NumSig<IDouble> )

Not with the current traits! Because the input type of the doubleNum trait is NumSig<IDouble>, and it is not a subtype/supertype of NumSig<IEvalDouble>. (due to the both covariant and contravariant occurrences of Exp in the Add constructor)

Attempt 1 - parameterizing doubleNum

Can we parameterize the doubleNum trait?

doubleNum[Exp] (self: NumSig<Exp>) : ? = {
   Lit (val: Int) = fold [IDouble] { double = self.Lit (val + val) } ;
   Add (e1 : IDouble ) (e2 : IDouble) = fold [IDouble]
      { double = 
		    self.Add (unfold [IDouble] e1).double  (unfold [IDouble] e2).double
} -- type error! because we get the parameterized `{ double : Exp }` type before applying the fold constructor, but the fold requires a concrete `IDouble = mu X. { double : X }` recursive type annotation

Attempt 2 - parameterizing doubleNum + refining with intersection types

Can we use intersection type to ensure that there is a IDouble interface?

I think the best we can do to type doubleNum is as follows:

doubleNum[Exp] (self: NumSig<IDouble, IDouble & Exp>) 
	: NumSig<IDouble & Exp, IDouble> = {
   Lit (val: Int) = fold [IDouble] { double = self.Lit (val + val) } ;
   Add (e1 : IDouble & Exp ) (e2 : IDouble & Exp ) = fold [IDouble]
      { double = self.Add 
		      (unfold [IDouble] e1).double  
		      (unfold [IDouble] e2).double
}

Justification for “best” typing:

Given that iso-recursive unfold/folds only allow concrete recursive types in the annotation, the typings for the following items are fixed (cannot be further parameterized/generalized ):

fold [IDouble] { double = self.Lit (val + val) } : IDouble
(unfold [IDouble] e1).double : IDouble
(unfold [IDouble] e2).double : IDouble
fold [IDouble] { ... } ( in the Add constructor) : IDouble


1. Therefore, for the output type of the Lit constructors, they have to be `IDouble`, not `Exp`.
2. Note that we are applying the self reference at `self.Add (unfold [IDouble] e1).double`, the input type of the `self.Add` constructor must be `IDouble` and nothing more else.
3. The output type of `self`-reference, or the input type of the constructors, can be relaxed to a parametrized type `IDouble & Exp`, so `Exp` can be later instantiated with more interfaces.

What can we do with the new typing? - does not help


e2 : NumSig<IEvalDouble> = new evalNum ,, doubleNum @ IEval


evalNum ,, doubleNum @ IEval has the type:
     Trait[NumSig<IEval>] 
   & Trait[NumSig<IDouble, IEvalDouble>, NumSig<IEvalDouble, IDouble]
<: Trait[NumSig<IDouble, IEvalDouble>, NumSig<IEvalDouble, IEvalDouble>]

NumSig<IEvalDouble, IEvalDouble> <: NumSig<IDouble, IEvalDouble> ?
IDouble <: IEvalDouble ? No!

The expected subtyping does not hold, the composed trait it not instantiable.

Attempt 3 - How about bounded polymorphism + structural unfolding?

doubleNum[Exp <: IDouble] (self: NumSig<Exp>) 
	: NumSig<Exp, IDouble> = {
   Lit (val: Int) = fold [IDouble] { double = self.Lit (val + val) } ;
   Add (e1 : Exp ) (e2 : Exp ) = fold [IDouble]
      { double = self.Add (unfold [Exp] e1).double  (unfold [Exp] e2).double } 

Lit constructor has type { Lit : Int -> IDouble } because
{ double = self.Lit (val + val) } : { double : Exp } <: { double : IDouble}


Add constructor has type { Add : Exp -> Exp -> IDouble } because

1)
	e1 : Exp
	Exp <: IDouble = mu X. {double : X}
	{double : Exp} = { double : X } [ X |-> Exp ]
	--------------------------------------- struct-unfold
	(unfold [Exp] e1) : { double : Exp }
	---------------------------------------
	(unfold [Exp] e1).double : Exp 
2)
	self.Add : Exp -> Exp -> Exp
3)
	{ double = ... } : { double : Exp } <: { double : IDouble }



In this definition:

doubleNum has the type: 
	Forall(Exp <: IDouble).Trait[NumSig<Exp>, NumSig<Exp,IDouble>]

Composition again: success?

e3 : NumSig<IEvalDouble> = new evalNum ,, doubleNum @ (IEval & IDouble)

evalNum ,, doubleNum @ (IEval & IDouble) has the type:
     Trait[NumSig<IEval>] 
   & Trait[NumSig<IEvalDouble>, NumSig<IEvalDouble, IDouble>]
<: Trait[NumSig<IEvalDouble>, NumSig<IEvalDouble, IEvalDouble>]

OK this merge is instantiable

However, for bounded quantification + distributivity subtyping, the metetheory is not clear (might be hard)

Recall that we only have restricted results for bounded quantification + intersection types (without distributivity) in JFP

Attempt 4 - structural rules + encoding F<: with intersection types

doubleNum[Exp] (self: NumSig<IDouble & Exp>) 
	: NumSig<IDouble & Exp, IDouble > = {
   Lit (val: Int) = fold [IDouble] { double = self.Lit (val + val) } ;
   Add (e1 : IDouble & Exp ) (e2 : IDouble & Exp ) = fold [IDouble]
      { double = self.Add 
		      (unfold [IDouble & Exp] e1).double  
		      (unfold [IDouble & Exp] e2).double
} 

Type checking:
1)
	e1 : IDouble & Exp
	IDouble & Exp <: IDouble = mu X. {double : X}
	{double : IDouble & Exp} = { double : X } [ X |-> IDouble & Exp ]
	--------------------------------------- struct-unfold
	(unfold [IDouble & Exp] e1) : { double : IDouble & Exp }
	---------------------------------------
	(unfold [IDouble & Exp] e1).double : IDouble & Exp
2)
    self.Add : IDouble & Exp -> IDouble & Exp -> IDouble & Exp
3)
    { double = ... } : { double : IDouble & Exp } <: { double : IDouble }
4)
    fold [IDouble] { double = ... } : IDouble


Note that the structural rule for folding is:
	e : A [a |-> B ]
	mu a. A <: B
	----------------
	fold [B] e : B
	
IDouble & Exp are not supertypes of IDouble, so we only get IDouble as the output

the final type of the trait is: 
	Forall(Exp).Trait[NumSig<IDouble & Exp>, NumSig<IDouble & Exp, IDouble>]




e : X 
mu a. A & X <: mu a. B 
--------------- structural unfolding 
unfold [A] e : B [X/a]


e : mu a. A
--------------- structural unfolding 
unfold [mu a. A] e : A [A/a]




so 
evalNum ,, doubleNum @ (IEval) has the type:
     Trait[NumSig<IEval>] 
   & Trait[NumSig<IEvalDouble>, NumSig<IEvalDouble, IDouble>]
<: Trait[NumSig<IEvalDouble>, NumSig<IEvalDouble>]

Graph View

Backlinks