4 ms·

As was already mentioned in another reply, what you are describing are refinement types. A refinement type system actually exists for Haskell: it’s called Liqui

As was already mentioned in another reply, what you are describing are refinement types. A refinement type system actually exists for Haskell: it’s called LiquidHaskell,[1] and though I have not used it for anything serious, it seems to work well for certain kinds of problems. The main challenge of refinement types is that arbitrary properties are very difficult to check in general. (If that weren’t the case, software verification would be easy!) I wrote about this at length in my previous blog post,[2] and Hillel Wayne wrote about it earlier this year from another perspective.[3] [1]: https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [2]: https://lexi-lambda.github.io/blog/2020/08/13/types-as-axioms-or-playing-god-with-static-types/ https://lexi-lambda.github.io/blog/2020/08/13/types-as-axiom... [3]: https://www.hillelwayne.com/post/constructive/ https://www.hillelwayne.com/post/constructive/

one-punch 6y ago
> arbitrary properties are very difficult to check in general. To add to this: In theory, it is not just difficult, but impossible. Imagine that the refinement predicate is whether the String/Text encode a (non-)halting Turing machine/Haskell program. Checking it would solve the halting problem. And this predicate is the proof of Rice theorem.[1] (Granted, this may require some sufficiently powerful logic such as first order, not sure if this proof applies to LiquidHaskell.) In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types.
- ImprobableTruth 6y ago
  >In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types. Could you elaborate on that? Unless you're just saying that formalizing reasonably intuitive properties is difficult in general, I don't see what you mean.
ImprobableTruth 6y ago
>The main challenge of refinement types is that arbitrary properties are very difficult to check in general. While this is true, I'm not sure how constructive types don't face the very same issue. Ultimately, you will have to provide evidence for the required properties, with constructive types the proof is just (more or less) implicitly embedded into the datatype, which imo just makes dealing with these properties harder rather than easier. In regards to the post by Hillel Wayne you've posted, I'm not sure what this statement >This means that predicative data is easier to express at the cost of permitting representable invalid data. This is enough of a problem that we prefer constructive data whenever feasible. is supposed to mean exactly. If your predicate makes some data invalid, it's just not representable in the refined type.
- one-punch 6y ago
  > 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] [1]: https://www.reddit.com/r/haskell/comments/jh7575/eliminating_bugs_with_dependent_haskell/ https://www.reddit.com/r/haskell/comments/jh7575/eliminating... [2]: https://www.youtube.com/watch?v=10gSoVZ5yXY https://www.youtube.com/watch?v=10gSoVZ5yXY
  - ImprobableTruth 6y ago
    >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.
    - one-punch 6y ago
      > 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). [1]: https://lispcast.com/church-vs-curry-types/ https://lispcast.com/church-vs-curry-types/ [2]: https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18/refinement-reflection.lhs/ https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18... 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.

one-punch 6y ago

> arbitrary properties are very difficult to check in general. To add to this: In theory, it is not just difficult, but impossible. Imagine that the refinement predicate is whether the String/Text encode a (non-)halting Turing machine/Haskell program. Checking it would solve the halting problem. And this predicate is the proof of Rice theorem.[1] (Granted, this may require some sufficiently powerful logic such as first order, not sure if this proof applies to LiquidHaskell.) In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types.

ImprobableTruth 6y ago
>In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types. Could you elaborate on that? Unless you're just saying that formalizing reasonably intuitive properties is difficult in general, I don't see what you mean.

ImprobableTruth 6y ago

>The main challenge of refinement types is that arbitrary properties are very difficult to check in general. While this is true, I'm not sure how constructive types don't face the very same issue. Ultimately, you will have to provide evidence for the required properties, with constructive types the proof is just (more or less) implicitly embedded into the datatype, which imo just makes dealing with these properties harder rather than easier. In regards to the post by Hillel Wayne you've posted, I'm not sure what this statement >This means that predicative data is easier to express at the cost of permitting representable invalid data. This is enough of a problem that we prefer constructive data whenever feasible. is supposed to mean exactly. If your predicate makes some data invalid, it's just not representable in the refined type.

one-punch 6y ago
> 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] [1]: https://www.reddit.com/r/haskell/comments/jh7575/eliminating_bugs_with_dependent_haskell/ https://www.reddit.com/r/haskell/comments/jh7575/eliminating... [2]: https://www.youtube.com/watch?v=10gSoVZ5yXY https://www.youtube.com/watch?v=10gSoVZ5yXY
- ImprobableTruth 6y ago
  >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.
  - one-punch 6y ago
    > 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). [1]: https://lispcast.com/church-vs-curry-types/ https://lispcast.com/church-vs-curry-types/ [2]: https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18/refinement-reflection.lhs/ https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18... 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.