Tony's Wiki

Encoding CP + negative methods

11 min read

  • Background
  • Task 1 - extending new constructors
  • [[#task-2---extend-the-subst-binary-method---attempt-1|Task 2 - extend the subst binary method - attempt 1]]
    • [[#Task 2 - extend the subst binary method - attempt 1#A failed attempt - Change the self signature|A failed attempt - Change the self signature]]
    • [[#Task 2 - extend the subst binary method - attempt 1#Playing with structural folds?|Playing with structural folds?]]
  • Type system design to the rescue?

TL;DR: We try to add subst method (which is binary method + self returning) to the existing encodings, and find that it seems necessary to further generalize the structural unfolding rule to be polarized to give the trait a modular type signature:

e : A+
A+ <: A- <: mu a. B
--------------------- polarized structural unfolding
unfold [A+, A-] e : B [a+ |-> A+, a- |-> A- ]

Background

In Encoding CP with distributive recursive types - refined we already defined the following:

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;


evalNum (self: Top) : NumSig<IEval> = { Lit = ..., Add = ... }
doubleNum[Exp] (self: NumSig<IDouble & Exp>) 
	: NumSig<IDouble & Exp, IDouble > = { ... }

e1 = new evalNum ,, doubleNum @ IEval : Trait[NumSig<IEvalDouble>]

Task 1 - extending new constructors

type VarSig<Exp> = { Var : String -> Exp };

-- We implement the eval method: 
--    to simplify the function we assume variables evaluate to 1
-- To implement the double method, 
--    we rely on the Add constructor, so the CP-style dependency is needed
evalDoubleVar[Exp] (self : NumSig<IDouble & IEval & Exp> 
						 & VarSig<IDouble & IEval>)
    : VarSig<IDouble & IEval> = {
    Var (s : String) = fold [IEvalDouble'] {
        eval = 1 ;
        double = self.Add (self.Var s) (self.Var s)
    }
};

-- !! Note, here in order to fold IEval and IDouble together 
--    we rely on the fact that IEvalDouble' == IEvalDouble


-- Alternatively, we may write:
--    Var (s : String) = fold [IEval] { eval = ... } ,, 
--						 fold [IDouble] { double = ... }
-- For this example it should also work



e2 = new evalNum ,, doubleNum @ IEval ,, evalDoubleNum @ Top : Trait[NumSig<IEvalDouble> & VarSig<IEvalDouble>]

Task 2 - extend the subst binary method - attempt 1

type ExpSig<Exp> = NumSig<Exp> & VarSig<Exp>;
type ISubst = mu X. { subst : String -> X -> X };

substNum[Exp] (self : ExpSig<ISubst & Exp>) : ExpSig<ISubst & Exp, ISubst> = {
	Lit (val : Int) = fold [ISubst] 
		{ subst (_ : String) (_ : ISubst)  = self.Lit val }
	Add (e1 e2 : ISubst & Exp) = fold [ISubst]
		{ subst (s : String) (v : ISubst & Exp) = self.Add 
				((unfold [ISubst] e1).subst s v)
				((unfold [ISubst] e2).subst s v) }
	Var (s1 : String) = fold [ISubst]
		{ subst (s : String) (v : ISubst & Exp) = 
			if s == s1 then v
					   else (self.Var s1) }
			
}; -- type error!

The type checking fails because:

unfold [ISubst] e1 : { subst : String -> ISubst & Exp -> ISubst & Exp }
                 v : ISubst & Exp
(unfold [ISubst] e1).subst s v : ISubst & Exp

self.Add : ISubst & Exp -> ISubst & Exp -> ISubst & Exp

{ subst ... } : String -> ISubst & Exp -> ISubst & Exp

However, this is not a subtype of the expected output type:
	String -> ISubst -> ISubst

fold [ISubst] { subst ... } fails!

--- We are in a dilemma:
--  1) Either we parameterize the `self` reference with 
--     extra methods (to be composed in the future), as the above codes show, 
--     but this prevents 
--     the subst method of Add constructor from being type checked in the `fold`
--  2) Or we make Add.subst parameter v be ISubst, so the `fold` works
--     but we lose the ability to compose the `subst` trait with others, 
--     it also breaks the `new` constructor design of closing the fixpoint

-- Is there an programming level implication of this design problem?
-- or we could just use a different trait encoding for the `subst` method?

A failed attempt - Change the self signature

Or, we can further refine the signature of the substNum trait?

substNum[Exp] (self : ExpSig<ISubst, ISubst & Exp>)    
				--- the input type of Self is different 
				    : ExpSig<ISubst & Exp, ISubst> = {
	Lit (val : Int) = fold [ISubst] 
		{ subst (_ : String) (_ : ISubst)  = self.Lit val }
	Add (e1 e2 : ISubst & Exp) = fold [ISubst]
		{ subst (s : String) (v : ISubst) = self.Add 
				((unfold [ISubst] e1).subst s v)
				((unfold [ISubst] e2).subst s v) }
	Var (s1 : String) = fold [ISubst]
		{ subst (s : String) (v : ISubst) = 
			if s == s1 then v
					   else (self.Var s1) }
			
};

v : ISubst
(unfold [ISubst] e1).subst s v : ISubst

---------[[[[Here is the difference]]]]]---------
self.Add : ISubst -> ISubst -> ISubst & Exp

{ subst ... } : String -> ISubst -> ISubst & Exp
             <: String -> ISubst -> ISubst

fold [ISubst] { subst ... } : ISubst --- OK!

However, the implemented trait seems not enough to be instantiable

substNum<Exp> :: Trait[ExpSig<ISubst, ISubst & Exp>, 
					   ExpSig<ISubst&Exp, ISubst>]


Expect: provided trait is a subtype of what is required
ExpSig<ISubst&Exp, ISubst> <: ExpSig<ISubst, ISubst & Exp>

The first argument in ExpSig seems problematic in the above subtyping check
Since we have no way to change 
ExpSig<ISubst, ... > to ExpSig<ISubst&Exp, ... >
by merging more traits

Playing with structural folds?

If we take a closer look at the dillemma:

type ExpSig<Exp> = NumSig<Exp> & VarSig<Exp>;
type ISubst = mu X. { subst : String -> X -> X };


- Positive
- Positive + Negative 
  ISubst = mu X. { subst : String -> X -> X };
- Only Negative + Analysis on both arguments
  IEq = mu X. { eq : X -> Bool } -- require case analysis on X
- Only Negative + Analysis on first arguments
  IEqAdd
- Positive + Negative + 
  IZipAdd = mu X. { zipadd: X -> X -> X }


type ISubst' Y = mu X. { subst : String -> (Y & X) -> X };

substNum : forall Exp. ExpSig<ISubst'<Exp> & Exp> 
                    -> ExpSig<ISubst'<Exp> & Exp, ISubst'<Exp> >

type IEval = mu X. { eval : Int };

substNum @ IEval :
   ExpSig<ISubst' @ IEval> & Exp> 
-> ExpSig<ISubst' @ IEval> & Exp, ISubst' @ IEval >

evalNum : ExpSig< IEval & Exp> ->  ExpSig< IEval & Exp, IEval >

ISubst' @ IEval = 
   mu X. { subst : String -> (mu Y. { eval : Int } & X) -> X }

IEval = mu X. { eval : Int }
<:
mu X. ({ subst : String -> X -> X } & { eval : Int})



substNum[Exp] (self : ExpSig<ISubst & Exp>) : ExpSig<ISubst & Exp, ISubst> = {
	Lit (val : Int) = fold [ISubst] 
		{ subst (_ : String) (_ : ISubst)  = self.Lit val }
	Add (e1 e2 : ISubst & Exp) = fold [ISubst]
		{ subst (s : String) (v : ISubst) = self.Add 
				((unfold [ISubst] e1).subst s v)
				((unfold [ISubst] e2).subst s v) }
		--- folding : { subst : String -> ISubst -> ISubst }
	Var (s1 : String) = fold [ISubst]
		{ subst (s : String) (v : ISubst) = 
			if s == s1 then v
					   else (self.Var s1) }
}; -- type error!

v has to be ISubst in order to be folded
===>
	((unfold [ISubst] e1).subst
	has to be
	String -> ISubst -> ?

self.Add has to be ISubst & Exp -> ISubst & Exp -> ISubst & Exp
in order to be instantiable
===>
	((unfold [ISubst] e1).subst
	has to be
	String -> ? -> ISubst & Exp


(unfold [ISubst & Exp, ISubst] e1).subst
: String -> ISubst -> ISubst & Exp





{ subst ... } in order to be folded, has to be:
	{ subst : Int -> ISubst -> ISubst}


type checking:
e1 : ISubst & Exp <: ISubst
unfold [ISubst] e1 : 
	{ subst : String -> ISubst -> ISubst & Exp } <-- expected
<:  { subst : String -> ISubst & Exp -> ISubst & Exp } <-- unfolded1
<:  { subst : String -> ISubst & Exp -> ISubst }

	{ subst : String -> ISubst -> ISubst & Exp } <-- expected
<:  { subst : String -> ISubst -> ISubst } <-- unfolded2



e : A [a |-> B]
mu a. A <: B
---------------
fold [B] e : B

Type system design to the rescue?

To achieve the precise typing we discussed in Playing with structural folds? We might want different substitutions in the structural unfolding


e : A+
A+ <: A- <: mu a. B
--------------------- polarized structural unfolding
unfold [A+, A-] e : B [a+ |-> A+, a- |-> A- ]

What will the generalized structural unfolding be like?

For reduction: unfold [A+, A-] (fold [B] v) ----> v

The typing derivation:
v : C [a |-> B]
mu a. C <: B
------------------
fold [B] v : B          B <: A+
------------------------------------
fold [B] v : A+                           A+ <: A- <: mu a. D
-----------------------------------------------------------------------------
unfold [A+, A-] (fold [B] v) : D [a+ |-> A+, a- |-> A- ]

The lemma should therefore be:

given:
mu a. C <: B <: A+ <: A- <: mu a. D

show: C [a |-> B] <: D [a+ |-> A+, a- |-> A- ]

Proof attempt:

by translation:

C [a- |-> {a : C}] <: D [a- |-> {a : D}]

Case 1. 
a is weakly positive in C and D
We can show:
C [a- |-> B] << D [a- |-> A-]
Moreover, as B << A+
We can show:
C [a- |-> B, a+ |-> B] << D [a- |-> A-, a+ |-> A+]


Case 2.
D <: C, C <: D
which implies that
mu a. C == mu a. D

mu a. C <: B <: A+ <: A- <: mu a. D <: mu a. C <: B <: A+ <: A- <: mu a. D
any types are equivalent


We can show:
C [a- |-> B, a+ |-> B] << D [a- |-> A-, a+ |-> A+]
since B, A-, A+ are just equivalent to mu a. C / mu a. D

So, it seems that we can even have this generalization:

e : A+
A+ <: A- <: mu a. B
--------------------- polarized structural unfolding
unfold [A+, A-] e : B [a+ |-> A+, a- |-> A- ]

With this design we can type check the substNum trait:

type ExpSig<Exp> = NumSig<Exp> & VarSig<Exp>;
type ISubst = mu X. { subst : String -> X -> X };

substNum[Exp] (self : ExpSig<ISubst & Exp>) : ExpSig<ISubst & Exp, ISubst> = {
	Lit (val : Int) = fold [ISubst]  
		{ subst (_ : String) (_ : ISubst)  = self.Lit val }
	Add (e1 e2 : ISubst & Exp) = fold [ISubst]
		{ subst (s : String) (v : ISubst) = self.Add 
				((unfold [ISubst & Exp, ISubst] e1).subst s v)
				((unfold [ISubst & Exp, ISubst] e2).subst s v) }
		-- in the unfold annotation
		-- first type for positive unfolding, 
		-- second type for negatve unfolding
	Var (s1 : String) = fold [ISubst]
		{ subst (s : String) (v : ISubst) = 
			if s == s1 then v
					   else (self.Var s1) }
}; -- type check!

The type checking works because:

For the Add constructor:

unfold [ISubst & Exp, ISubst] e1 : { subst : String -> ISubst -> ISubst & Exp } }
                               v : ISubst 
(unfold [ISubst & Exp, ISubst] e1).subst s v : ISubst & Exp

self.Add : ISubst & Exp -> ISubst & Exp -> ISubst & Exp

{ subst ... } : String -> ISubst -> ISubst & Exp

Now, this is a subtype of the expected output type:
	String -> ISubst -> ISubst

fold [ISubst] { subst ... } succeeds!

The type of the Add Constructor is:
	Add :: ISubst & Exp -> ISubst & Exp -> ISubst
satisfying the expected trait signature

Graph View

Backlinks