WIP This is the Encoding CP + negative methods refined with CP-style of elaboration:
Elaborating compositional interfaces and sorts. Firstly, the compositional interface ExpSig:
type ExpSig<Exp>= {
Lit : Int -> Exp;
Add : Exp -> Exp -> Exp;
};
is translated to an equivalent type using only type parameters:
type ExpSig Exp OExp=
{ Lit : Int -> Trait[Exp,OExp] } &
{ Add : Exp -> Exp -> Trait[Exp,OExp] };
The sort Exp is represented by two type parameters
Background
In Encoding CP with distributive recursive types - refined we already defined the following:
type NumSig Exp OExp = {
Lit : Int -> Trait[Exp,OExp];
Add : Exp -> Exp -> Trait[Exp,OExp]
};
type IEval = mu X. { eval : Int };
type IDouble = mu X. { double : X };
type IEvalDouble = IEval & IDouble;
evalNum = trait [self: Top] implements NumSig IEval IEval = open self in
{ Lit = ... } ,,
{ Add = ... }
doubleNum Exp = trait [self: NumSig<IDouble & Exp>]
implements (NumSig (IDouble & Exp) IDouble) =
open self in
{ Lit = fold [IDouble] (self.Lit ... ) } ,,
{ Add (e1 e2 : IEvalDouble) = fold [IDouble] (self.Add ... ) }
e1 = new evalNum ,, doubleNum @ IEval : Trait[NumSig<IEvalDouble>]
Task 1 - extending new constructors
type VarSig<Exp> = { Var : String -> Exp };
-- assume variables evaluate to 1
-- depends on the Add constructor
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 together
-- we rely on the fact that IEvalDouble' == IEvalDouble
-- Alternatively, we may write:
-- Var (s : String) = fold [IEval] { eval = ... } ,,
-- fold [IDouble] { double = ... }
e2 = new evalNum ,, doubleNum @ IEval ,, evalDoubleNum @ Top : Trait[NumSig<IEvalDouble> & VarSig<IEvalDouble>]
Task 2 - extend the subst binary method - old style
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
is not a subtype of
String -> ISubst -> ISubst
fold [ISubst] { subst ... } fails!
--- We are in a dilemma:
-- 1) Either we parameterize the `self` reference with
-- extra methods (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?
--
--
Change the self signature
Or, we can further refine the signature of the substNum trait?
substNum[Exp] (self : ExpSig<ISubst, 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) }
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>
what is the trait for
substNum2<Exp> :: Trait[ExpSig<IEval, ISubst & Exp>,
ExpSig<ISubst&Exp, ISubst>]] ?
so that substNum @ IEval ,, substNum2 <: Trait[IEvalSubst] ?
Playing with structural folds?
dillema revealed:
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] 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) }
}; -- 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
{ 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
Two Exp parameters
substNum[Exp] (self : ExpSig<ISubst, 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) }
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
self.Add : ISubst & OExp -> ISubst & OExp -> ISubst & Exp
{ subst ... } : String -> ISubst -> ISubst & Exp
<: String -> ISubst -> ISubst
fold [ISubst] { subst ... } : ISubst --- OK!