https://en.m.wikipedia.org/wiki/Curry%27s_paradox

https://stackoverflow.com/questions/2583337/strictly-positive-in-agda

idris agda 처음 써보고 굉장히 당혹스러웠던 문제인데, dependently typed language에서 termination 문제는 진짜 맨날 튀어나옴

간단히 해설을 하자면,
data Q -- Q의 정의는 아무래도 좋음
data P = MkP (P -> Q)
위와 같은 data type을 생각해보자.
P의 생성자 MkP의 타입은 MkP :: (P -> Q) -> P 임.

중요한건 여기서 P만 가지고도 재귀도 없이 종료 안하는 프로그램을 망들 수 있음.

ptoq :: P -> Q
ptoq p@(MkP x) = x p

p :: P
p = MkP ptoq

q :: Q
q = ptoq p

Q의 정의를 주지도 않았는데 Q를 만들었다. 그러니까 Q에 아무 타입이나 넣을 수 있고, 한마디로 증명용으로 못써먹게 됨.
그리고 q = ptoq p 를 평가해보면 ptoq p 가 되는걸 알수 있음. 한마디로 종료를 안함.

이걸 해결하려면 애초에 P같은 데이터 타입을 금지해야 함. 구체적으로 어떤 것들을 금지해야 하냐면
MkP :: (P -> Q) -> P 를
MkP :: F P -> P 꼴로 볼 수 있는데, 여기서 함자 F 가 P에 대해 strictly positive 해야함.

일단 positive/negative 라는건 함자의 공변/반변성을 말하는건데 (C#이나 Scala에 있는 in out 도 같은거임)
a, (a, b), r -> a,  (a -> r) -> r 등은 a에 대해 positive 고
a -> r 같은건 negative 임.
그냥 arrow 왼쪽에 올때마다 (-)가 곱해진다 보면 됨.

strictly positive 는 조금 더 강한 조건인데, 타입이 화살표의 왼쪽에 오는걸 완전히 금지해버린다.
(a -> r) -> r 같은건 positive 지만 strictly positive는 아님.

위의 MkP :: (P -> Q) -> P 의 경우 P -> Q 가 negative한게 문제임.
어쨋든 curry's paradox를 해결하려면 strictly positive 하지 않은 타입들을 전부 금지해야 한다.

근데 문제는, 저런 타입이 의외로 만들고 싶을 때가 있음. 위의 stackoverflow 링크처럼 HOAS (Higher Order Abstract Syntax)를 만들고 싶을 때, 하스켈같이 타입이 허벌인 언어는 간단히 되지만 agda에서는 콤파일이 안됨.


이런건 보면 진짜 뭐든 득실이 있긴 함. 물론 그래도 디펜던트 타입 쓰고 싶긴 한데