dependently typed language면 type이 value에 의존하는게 가능한데, 문제는 이 값들을 어떻게 구별하느냐임.


structural 하게 할 수도 있고, nominal하게 할 수도 있음.


-- 간단하게 설명

structural equality는

data Bool = True | False

처럼 constructor들로 쪼개서 같은지 보는거.


nominal equality는

newtype Int' = Int

에서 Int'하고 Int가 다른것처럼 이름가지고 구분하는거.


보통 structural은 value에서, nominal은 type에서 많이 쓰는데 반대도 가능.

--


문제는 함수타입 같은건 constructor로 쪼갤 수가 없으니 structural equality를 검사하는게 불가능함.

(AST단위로 비교하면 모를까. idris는 interative 모드에서 AST출력 해주던데, 타입 검사할때도 반영하는지는 잘 모르겠음)


그래서 agda같은 dependently typed language에서 value에 의존하는 타입를 어떻게 검사하나 봤는데, constructor로 쪼개지면 structural하게 검사하고

함수타입은 nominal하게 검사함.

(idris는 어떻게 하는지 잘 모르겠음)

근데 이게 문법적으로 엄격하게 구분되지는 않더라고.


f x = x

g x = x

라고 하면 f랑 g가 다르게 취급되고


f x = x

g = f

라고 하면 둘이 똑같이 취급됨.


이걸 언제 synonym으로 처리하고 언제 new name으로 처리하는지를 문법적으로 엄격하게 구분이 되면 좋겠다는 생각이 듬.

newname g = f

라고 하면 g하고 f하고 다르게 처리되는 식으로.


그리고 새로운 타입을 정의할때 그 타입의 value들을 nominal하게 비교할지 structural하게 비교할지를 정할 수 있게 한다던가.

등등..


structural하고 nominal하고 공존할 수 없는 개념이 아니라서, 어떻게 해야 자연스럽게 융합될지 생각해볼 필요가 있을 듯.