하스켈에서 가장 핵심적인 부분은 type system/type inference 일 텐데
관련 연구 및 언어들이 등장한 시기는 아래와 같음
Simply typed lambda calculus : 1940
Hindley-Milner 타입 추론 알고리즘 : 1969
System F (Hindley-Milner 타입 시스템 일반화) : 1972
ML : 1973
Hindley-Milner 타입 추론 알고리즘의 completeness 증명 : 1982
Standard ML : 1983
Miranda : 1985
Haskell : 1990
OCaml : 1996
보면 알겠지만 하스켈에서 사용된 이론은 lambda calculus를 빼도 거의 20년 전부터 나온거고 그때 당시 기준으로도 최신 이론이라 말하기는 좀 미묘함.
Hindley-Milner type inference 를 제일 먼저 사용한 언어도 Robin Milner가 직접 만든 ML이고 하스켈보다 한참 먼저 나옴.
그러니까 하스켈이 연구용이 아니라 개발용으로 만들었단게 구라가 아니다. 연구라고 해도 구현에 대한 연구가 주임.
반면 진짜 연구용 언어인 cubical agda는 매우 따끈따끈 한데
Martin-Löf type theory : 1972
Coq : 1989
Agda 1.0 : 1999
Agda 2 : 2007
univalence axiom : 대략 2009
cubical type theory : 2016
cubical agda : 2019
나온지 2년 됐음..
참고로 cubical agda 말고도 cubical type theory를 구현한 언어는 꽤 있음
님 전공 뭐임?
컴공
컴공은 컴공인데 세부전공
PL
해당 댓글은 삭제되었습니다.
linear type도 나온지는 한참 된 개념이고, 당장 러스트에서 쓰는 affine type도 linear type 비슷한 거니까
힌들리 밀너는 아는데 cubical은 아예 첨 들어보네. 뭔가 장점이 있음?
프로그래밍에 필요한건 아니고, 증명언어 타입시스템임
Homotopy Type Theory라는 굉장히 혁신적인 증명언어용 타입 시스템이 있는데, 이 HoTT를 공리 없이 구현하려고 나온게 cubical type theory임
호옹...몬가 어렵따..
낚시인줄 알았는데 찐이네
이런 거 좋당
증명언어로써 coq이랑 agda랑 차이있음?
타입 시스템은 거의 같은데 활용 방식은 상당히 차이남
applicative functor인가? 그거 2008년 되어서야 학계에 나온거라고 누가 그러던데
맞아 그쪽에도 하스켈 공이 크긴 한데 하스켈 본연의 기능이 아니라 그냥 그런걸 사용해서 프로그래밍 하는 관습이 하스켈에서 유행했을 뿐이라서.. 살짝 다름
applicative functor로 프로그래밍 하는건 2008년에 나온게 맞는것 같은데, (lax) monoidal functor 언제 생겼는지는 잘 모르겠다.. 아마 조금 더 이를것 같음
이게 컴공이지
커 ㅁ 사같은데