Kim-Gayoung / RPCExample_Java

https://github.com/kwanghoon/rpcexample
0 stars 1 forks source link

ForAll에 대한 제약사항을 추가할 때 #17

Open Kim-Gayoung opened 5 years ago

Kim-Gayoung commented 5 years ago

@kwanghoon unify에 ForAll에 대한 조건을 추가해야되서 관련 질문에 대해 comment를 보냅니다.

https://github.com/Kim-Gayoung/RPCExample_Java/blob/23720dee28b7abf713122f2f8ca7b88a8b4025eb/src/com/example/extrpc/Infer.java#L458

ForAll에 대한 제약사항을 unify 해줄 경우, 다양한 타입들이 올 수가 있는데, Bound Type Variable에 대한 제약사항은 제거를 하고 추가를 해야된다고 생각을 합니다.

예를 들어, forall a1. a1 = a2 와 같은 경우에는 a1과 a2가 제약사항이 추가되서는 안되고, forall a1, a2. (a1-s->a2)-c->a3 = a4-c->a5인 경우에는 a3와 a5에 대한 제약사항만 추가되는 것이 맞다고 생각합니다.

ForAll이 가진 Type이 VarType의 경우, 제약조건을 확인하여 bound type variable에 대한 식을 제거를 하면되는데 ForAll이 가진 Type이 FunType의 경우, 부분적으로 ForAll을 모두 붙여 보내는 방법을 생각해 보았는데, 혹시 제약조건을 제거할 적절한 알고리즘 있을까요??

kwanghoon commented 5 years ago

@Kim-Gayoung 내 생각에는

forall a.ty 와 같은 형태의 타입은 오직 type environment에서만 나타나야 하고 제약식을 생성하거나 제약식을 푸는 과정에서는 a를 어떤 고유 타입 변수로 대체한 ty{ a0 / a}만 다루게 될 것이다.

따라서 unify에서 forall a.ty 형태의 타입을 고려할 필요가 없을 것으로 판단한다.

이 경우를 빼고 unify를 코딩한 다음 혹시 내가 생각하는 바와 다른 경우가 발생하면 다시 논의해보자.

kwanghoon commented 5 years ago

@Kim-Gayoung Any progress?