Occurs-Check bei Fun$$-Typen #279

New Issue

pl · 2023-07-18T13:41:59Z

pl commented

2023-07-18 13:41:59 +00:00

Twice2.jav

class Twice2 {

TPH N id1inst;
TPH R id1;
TPH V id2inst;
TPH Z id2;
TPH AD twice;
Twice2()({
super(());
((this)::TPH Q.id1inst)::TPH N = new Id();
((this)::TPH U.id1)::TPH R = (((this)::TPH S.id1inst)::TPH N.id)::TPH T;
((this)::TPH Y.id2inst)::TPH V = new Id();
((this)::TPH AC.id2)::TPH Z = (((this)::TPH AA.id2inst)::TPH V.id)::TPH AB;
((this)::TPH AK.twice)::TPH AD = (((this)::TPH AE.id1)::TPH R.apply Signature: [TPH AG, TPH AH](((this)::TPH AF.id2)::TPH Z))::TPH AI;
})::TPH AQ
Twice2()({
super(());
})::TPH AN

}class Id {

TPH CE id;
Id()({
super(());
((this)::TPH CJ.id)::TPH CE = ((T x) -> ({
return (x)::T;
})::TPH CF)::TPH CI;
})::TPH CR
Id()({
super(());
})::TPH CN

}

Entscheidende Constraints:

R =. Fun1$$<CME,CMF>
T <. R
T =. CE
AB =. CE
AB <. Z
Z <. CME

Daraus folgt
R = T = AB = Z = CME = Fun1$$<CME,CMF>
Also müsste der Occurs-Check die Unifikation beenden. Aufgrund von Co- und Contravarianz der Argumente und die Ersetzung durch neue Typvaraiblen passiert das nicht.

Twice2.jav class Twice2 { TPH N id1inst; TPH R id1; TPH V id2inst; TPH Z id2; TPH AD twice; Twice2()({ super(()); ((this)::TPH Q.id1inst)::TPH N = new Id(); ((this)::TPH U.id1)::TPH R = (((this)::TPH S.id1inst)::TPH N.id)::TPH T; ((this)::TPH Y.id2inst)::TPH V = new Id(); ((this)::TPH AC.id2)::TPH Z = (((this)::TPH AA.id2inst)::TPH V.id)::TPH AB; ((this)::TPH AK.twice)::TPH AD = (((this)::TPH AE.id1)::TPH R.apply Signature: [TPH AG, TPH AH](((this)::TPH AF.id2)::TPH Z))::TPH AI; })::TPH AQ Twice2()({ super(()); })::TPH AN }class Id<T> { TPH CE id; Id()({ super(()); ((this)::TPH CJ.id)::TPH CE = ((T x) -> ({ return (x)::T; })::TPH CF)::TPH CI; })::TPH CR Id()({ super(()); })::TPH CN } Entscheidende Constraints: R =. Fun1$$<CME,CMF> T <. R T =. CE AB =. CE AB <. Z Z <. CME Daraus folgt R = T = AB = Z = CME = Fun1$$<CME,CMF> Also müsste der Occurs-Check die Unifikation beenden. Aufgrund von Co- und Contravarianz der Argumente und die Ersetzung durch neue Typvaraiblen passiert das nicht.

Sign in to join this conversation.