디펜던트 타입 언어를 만들고 싶습니다

[기괴공학도(mecheng98)]

뭘 공부해야 하나요?

- dc official App

[lp(24.3)]

굳이 의존형을 사용하는 이유가 있나요?

[기괴공학도(mecheng98)]

증명 보조 기능을 넣고 싶어서요. - dc App

[기괴공학도(mecheng98)]

단순 타입 람다 셈법 도우미 LambdaWizard를 만들어 보고 더 대단한 걸 만들어보고 싶어졌어요. Github에 치면 나와요. - dc App

[lp(24.3)]

현존하는 거의 모든 dependent type system은 Per Martin-Löf의 타입 이론에 직간접적으로 기반하는 걸로 알고 있습니다. 이론적 배경이라면 여기서 시작하는 것이 도움이 되지 않을까 싶네요. (
https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory)

[lp(24.3)]

그런데 흥미 본위의 프로젝트라면야 뭘 하든 마음대로지만, 실용적 목적이 있다면 그 목적이 무엇인지를 구체적으로 설정하는 것만으로도 대부분의 경우 의존형이 필요 없다는 결론이 나오지 않을까... 라는 것이 제 사견입니다.

[lp(24.3)]

일단 가장 중요한 질문은 이거겠죠. 프로그래밍 언어인가? 정리 증명기인가?

[기괴공학도(mecheng98)]

저는 그냥 취미충이라서 컴퓨터 잘 모르고요, 인터프리터까지만 만들고 싶어요. - dc App

[기괴공학도(mecheng98)]

둘 중 하나라면 증명 보조 기능을 고를게요. 소스파일을 실행파일로 만드는 데는 관심이 없고 인터프리터까지만 만드려고요. - dc App

[기괴공학도(mecheng98)]

그리고 디펜던트 타입이 없어도 되는다는 의견에 동의합니다. 저는 Pragma 없이 Haskell을 사용해서요. - dc App

[lp(24.3)]

인터프리터란 증명이 valid한지 검증하는 타입체커를 말씀하시는 거죠? Computational interpretation이 있는 언어를 evaluate하는 게 아니라?

[기괴공학도(mecheng98)]

둘 다 해보고 싶은 게 제 욕심입니다. 안 될까요? - dc App

[lp(24.3)]

아니요, 상술했듯 취미 목적이라면 안 될 것은 전혀 없지요. 다만 양쪽으로 동시에 실용적이기 어렵다는 점은 감안하고 시작하는 것이 좋을 것 같다... 정도의 의견이었습니다.

[lp(24.3)]

반드시 의존형일 필요는 없으나 프로그래밍과 정리 증명을 동시에 수행하고 싶다... 라면, 제가 아는 한에서는
https://dl.acm.org/citation.cfm?id=2331097
이 텍스트가 가장 조건에 부합하는 것 같습니다.

[기괴공학도(mecheng98)]

맞습니다. 둘 다에 특화될 필요가 없다고 댓글 달려고 했어요. 책 추천해주셔서 감사합니다. ^^ - dc App

[기괴공학도(mecheng98)]

전 평생 취미로 이쪽 분야를 공부하려고요 ㅎㅎ 운동도 게임도 재미없어서요 - dc App

[lp(24.3)]

별 관계 없는 이야기지만 게임이라 해도 한마디로 하기 어려울 만큼 종류가 다양하지요. TIS-100 같은 게임은 의외로 좋아하실 수도?

[기괴공학도(mecheng98)]

처음 들어본 게임인데 완전 어려운 것 같군요. 저랑 비슷한 친구가 있는데 그 친구가 휴가 나오면 같이 해봐야겠군요. - dc App