공부목적으로 language 하나만들면서 type inference 넣어보려고 공부 막 시작했는데 질문좀.
1. 컴파일타임에 추론가능한 모든것들에 대해서 (예를들면 a = b + c // a:int, b:int, c:int) 구현할때 Coq, Agda같은 proof-assistant (써본적없음) 걸로 구현하는게 어떻게생각하는지?
장점으로는 증명,테스팅에 용이할것같은데 단점으로는 랭귀지 하나 더추가해서 관리해야한다는점? (단점아닐수도), proof-assistant와 컴파일러 코드간의 interface구축해야하는 further work가 생기는점? (컴파일러가 타입추론을 proof-assistant에게 넘겨야하니까). 그래서 질문은 장단점이뭔지, proof-assistant로 구현한 사례(레퍼런스)가 있는지, 조언 등
2. OCaml이 힌들리밀너 이론으로 type inference를 구현했다고 들었는데 (자세히 찾아보진않음) 역사적으로 힌들리밀너 타입인퍼런스 뒤에 나온 이론 및 구현중에 힌들리밀너 타입인퍼런스 정도의 퍼포먼스 및 대중성을 보인 연구들이 있는지?
3. 아무조언
감사합니다
1번은 프로그래밍 언어를 증명보조기로 형식화 하는건데, 연구용 미니 언어로는 많이 함. 산업용으로는 비용이 너무 커서 그런걸 하는 경우는 드물지만 종종 있음. compcert (Coq으로 구현한 C 컴파일러) 같은 것들. 실용적 장점은 검증된 언어 구현체를 얻을 수 있다는 점.
2. HM 타입시스템이 아니라 HM 타입추론 알고리즘 말하는거지? HM 타입 시스템을 확장하고 추론알고리즘을 거기에 맞춰서 수정하는 그런 연구는 많이 있음. HM이랑 뿌리부터 다른 추론 알고리즘은 별로 못들어봄.
1. compcert 찾아봤는데 motivation이 기존 상용 컴파일러 (gcc 등)가 (1) 버그있는 머신코드(소스코드에서는 버그가없지만)를 생성하거나 (2) 소스코드상의 behavior를 subsume하지못하는 머신코드를 생성하는, 이런 2가지의 범주들에 대해서 correctness를 추가한 컴파일러 만든것같네요? 제 목표는 컴파일러가 코드를 똑바로 생성한다기보다는 type system같이 formal verification하기 좋은 것들만 컴포넌트로 구분해서 마이크로아키텍처처럼 분리해보고싶었던 아이디어였는데 거리가 좀 있는듯 하네요. 별로 좋은 아이디어가아닌지..ㅠ? 2. 저는 HM 타입추론을 얘기한거였는데 HM 타입시스템이 기저이론이였군요. 둘다 살펴봐야겠네요 감사합니다
걍 잘 아는 언어로 짜는게 편함.