3 ms·

> A light-weight form of dependent types are refined types, which are essentially dependent function types that have contracts on their parameters and return ty

by ufo 12y ago

> A light-weight form of dependent types are refined types, which are essentially dependent function types that have contracts on their parameters and return types I had never seen it written that way. What can full dependent types do that you can't do with refinement types?

tomp 12y ago
I'm not sure, as I'm not really knowledgeable in programming with full dependent types (as in Agda, Idris, or Coq). However, I can point you to this discussion on Reddit [1]; essentially, one user (kamatsu) is saying that refinement types are not dependent types: > More or less, if you have sigma and/or pi types, then you have dependent types. If you don't, you don't. Also, he claims that a crucial difference is that dependent types are proofs, while type-checking refined types requires proof search. Then, another user (neelk) points out an article [2] which claims (I haven't read it) that dependent types can be encoded using singleton types, which can be written using refined types. [1] http://www.reddit.com/r/programming/comments/26se9k/refined_types_a_better_type_system_for_more/chu013j http://www.reddit.com/r/programming/comments/26se9k/refined_... [2] http://www.iro.umontreal.ca/~monnier/comp-deptypes.pdf http://www.iro.umontreal.ca/~monnier/comp-deptypes.pdf