Problems of the Mugda paper

[xieyuheng]

(1) Equivalent without type is wrong, because the meaning of equivalent is only determined for specific type.

(2) Ap has target & args instead of target & arg.

(3) Using Var & Ap as Value instead of defining a Neutral type.

[xieyuheng]

(4) No TypedNeutral, no typed directed readback, thus can not handle eta rules.

[xieyuheng]

(5) The meaning of Values.Ap is overloaded.

The paper uses (A):

• Data
• Ctor

Maybe we should use (B):

• Datatype
• DatatypeCtor -- Data of the paper
• Data
• DataCtor -- Ctor of the paper

[xieyuheng]

Pros and Cons about (5):

(A) is gooder:

• In (A), Exp is close to Value.

(B) is gooder:

• In (B), doAp will be clear.