I don't think there's a reasonable argument against refinement types being a kind of dependent type. Arguments against this usually just come down to implementation details and people not wanting to associate themselves with us nerdy DTT people
Conversation
My experience is that the disagreement goes the other way -- people who talk about dependent types tend not to want to include Typed Racket, eg.
The other consideration is the saying "Liquid Haskell has dependent types" can confuse people into expecting something different.
2
10
I think that's a confusion about what dependent types are. We need to say "arbitrary dependent types" when that's what we mean IMO
2
1
I think 's suggestion of saying first-class types when you mean full dependent types would be really helpful here!
For instance, if you're only allowed to depend on, say, integers, then only type-level integers and arithmetic becomes first class.
3
1
8
Indeed, this is why I started using that phrase. It seems reasonable for "dependent type" to mean lots of things.
1
4
Yeah I've been using it too after seeing you use it in a talk. It's also a bit less of a mouthful and less scary than 'full-spectrum dependent types'!
1
1
I think I did get some push-back when talking to a lisp minded person though, seeing as there are restrictions on where types can go (eg. universe levels etc), but I'm not sure I care all that much?
There's restrictions on where anything can go, in that things have to type check... so I'm not especially bothered about that complaint. I think "first class types" helpfully communicates what's actually going on.
2