짧은 이해로 해커뉴스를 읽어보니 디펜던트 타입과 유사한게 리파인 타입이란게 있고 이것이 더의미있을수 있다고도 하네요. https://github.com/tomprimozic/type-systems/tree/master/refined_types
넓은의미에서 리파인드또한 디펜던트타입시스템의 일종이라 볼수 있음. 문법에 문제에 가까울수 있다. 리파인드는 디펜던트 타입이 다루고자 하는 문제에 대한 다른 접근으로 주로 SMT Solver, Automated Theorem Prover와 같은것을 언어? 컴파일러? 단에 도입하여 디펜던트타입랭귀지가 바닥부터 타입정의를 잘해야 하는 부분을 자동으로 매꿔준다
- 톱다운
- everything is proved, by hand, by the user, who has to build up the whole program from basic blocks
- e.g. idris, coq, agda, dependent haskell
type List a n =
| Nil : List 'a 0
| Const : a -> List a n -> List a (n + 1)
- 버텀업
- Start with a program and add some assertions about the values (and possibly functions, but this can then get more complicated) in the program. The idea is that many of these can ideally be proven by automated SMT solvers, which support some “theories” (e.g. natural numbers, real numbers, bitfields (i.e. machine integers and floating point numbers), algebraic datatypes) and can prove some statements in these theories.
- e.g.
- Liquid Haskell >>> https://ucsd-progsys.github.io/liquidhaskell-blog/
- Danfny >>> https://rise4fun.com/Dafny/tutorial/guide
- F* >>> https://fstar-lang.org/tutorial/
- Z3 >>> https://github.com/Z3Prover/z3
type List a = <... whatever ...>
property length : List a -> Nat