> While this is true, I'm not sure how constructive types don't face the very same issue.
Not sure if the author claims that constructive types do not face this issue.
On constructive types vs refinement types, there is a recent Reddit discussion on this topic,[1] prompted by Facebook’s use of Dependent Haskell to eliminate bugs.[2]
>Not sure if the author claims that constructive types do not face this issue.
This might be true, but when they were making the case for constructive types they didn't mention it.
>On constructive types vs refinement types, there is a recent Reddit discussion on this topic
The discussions seems to be mostly dependent types vs refinement types, which I'd argue is a false dichotomy. I'd say that dependent types is a what makes refinement types actually powerful in the first place. It's also how most Coq specifications are written.
> This might be true, but when they were making the case for constructive types they didn't mention it.
Agree.
> The discussions seems to be mostly dependent types vs refinement types, which I'd argue is a false dichotomy.
You are right, I think I confused two notions:
1. constructive vs non-constructive reasoning.
2. intrinsic vs extrinsic types (aka Church vs Curry types[ 1]).
In general, intrinsic types are constructive (because Program-is-Proof due to Brouwer–Heyting–Kolmogorov and
Curry–Howard and others).
But extrinsic types could also be constructive, esp. when the external static analyzer has access to the program, such as in refinement reflection [2] (as pointed out in the above Reddit comment thread).
Then I think the author is arguing for constructive proofs, which come naturally with intrinsic types, or at least with extrinsic analyzers accessing program structures; and arguing against non-constructive (extrinsic) types, or anything detached from implementation.
This might be true, but when they were making the case for constructive types they didn't mention it.
>On constructive types vs refinement types, there is a recent Reddit discussion on this topic
The discussions seems to be mostly dependent types vs refinement types, which I'd argue is a false dichotomy. I'd say that dependent types is a what makes refinement types actually powerful in the first place. It's also how most Coq specifications are written.