Encoding CP with distributive recursive types

Composing positive methods

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)


Method Implemetations:

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 }
}

NumSig<IDouble> = {
   Lit : Int -> IDouble
   Add : IDouble -> IDouble -> IDouble
}

-- 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


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
}


e1 : NumSig<IEvalDouble> = 
	(fix [NumSig<IEval>] evalNum) ,, (fix [NumSig<IDouble>] doubleNum)
-- Question: can we instead write:
    (fix NumSig<IEvalDouble> (evalNum ,, doubleNum) )

Type checking the composition:

evalNum : Top -> NumSig<IEval>
doubleNum : NumSig<IDouble> -> NumSig<IDouble>

<: (NumSig<IEvalDouble> -> NumSig<IEval>) 
 & (NumSig<IDouble> -> NumSig<IDouble>) 

<: (NumSig<IEvalDouble> -> NumSig<IEval>) 
 & (NumSig<IDouble> -> NumSig<IDouble>) 
 
<: NumSig<IEvalDouble> -> NumSig<IEvalDouble>





NumSig<IEvalDouble> <: NumSig<IDouble>
   { Lit : Int -> IEvalDouble , 
     Add : IEval & IDouble -> IEvalDouble -> IEvalDouble  }
<: { Lit : Int -> IDouble , Add :IDouble -> IDouble -> IDouble  }

NumSig<IEval> = {
  Lit : Int -> IEval;
  Add : IEval -> IEval -> IEval;
}

NumSig<IDouble> = {
  Lit : Int -> IDouble;
  Add : IDouble -> IDouble -> IDouble;
}

NumSig<IEval> & NumSig<IDouble> = {
  Lit : Int -> IEval & IDouble;
  Add : (IEval -> IEval -> IEval) & (IDouble -> IDouble -> IDouble)
} == {
  Lit : Int -> IEvalDouble;
  Add : IEvalDouble -> IEvalDouble -> IEvalDouble
} <: (strict subtyping) {
  Lit : Int -> IEvalDouble';
  Add : IEvalDouble -> IEvalDouble -> IEvalDouble'
}

Extending Constructors

type NegSig<Exp> = { Neg : Exp -> Exp };

when implementing two methods (double and eval) at the same time, instead of writing interfaces as IEvalDouble', we should make it more precise, IEvalDouble


NegSig<IEvalDouble> = { Neg : IEvalDouble -> IEvalDouble }

evalDoubleNeg (self: NegSig<IEvalDouble>) : NegSig<IEvalDouble> = {
	Neg (e : IEvalDouble) = fold [IEval]
		{ eval = (unfold [IEval] e).eval * -1 }
		   -- Note that this works because 
		   -- x : IEvalDouble = IEval & IDouble <: IEval
		   -- Remark: since here we are dealing with positive subtyping
		   -- it is fine to use "NegSig<IEvalDouble'>"
		   -- due to recursive subtyping
	& fold [IDouble] { double = self.Neg (unfold [IEvalDouble'] e).double }
			-- note here: IEvalDouble' seems necessary, 
			 -- since only unfold [recursive type] is allowed in the syntax
			-- and we would require IEvalDouble <: IEvalDouble'

	-- type checking:
		--                                e : IEvalDouble <: IEvalDouble'
		-- (unfold [IEvalDouble'] e).double : IEvalDouble'
		--                    self.Neg : IEval & IDouble -> IEval & IDouble
		-- here we need the subtyping IEvalDouble' <: IEvalDouble to hold
			-- which does not typically hold for negative types!
			-- expected? binary method composition + self reference ==> problem?
		-- 
		-- self.Neg (unfold [IEvalDouble] e).double : IEval & IDouble
		--                                          <: IDouble
		-- so the fold [IDouble] { double : IDouble } gets the desired type

	-- the overall type of the evalDoubleNeg body:
		-- IEval & IDouble
	-- the overall type of the evalDoubleNeg:
		-- {Neg : IEvalDouble -> IEvalDouble}