undefined | Better HN

story

0 pointstel12y ago0 comments

Yeah, less power means greater inference. You can model liquid types in a DT language I believe, but you'll never have the same convenience.

0 comments

vilhelm_s12y ago

"Dependent types" is a quite broad term. The Liquid types people certainly call their work dependent types, even though it has a different flavour than e.g. Coq or Agda.

telOP12y ago

Yes, that's true—I lapsed in terminology. Maybe calling it ITT would be better? There's a lot of ambiguity there, of course. And less marketing.

j / k navigate · click thread line to collapse

0 comments

vilhelm_s12y ago

"Dependent types" is a quite broad term. The Liquid types people certainly call their work dependent types, even though it has a different flavour than e.g. Coq or Agda.

telOP12y ago

Yes, that's true—I lapsed in terminology. Maybe calling it ITT would be better? There's a lot of ambiguity there, of course. And less marketing.

j / k navigate · click thread line to collapse