6 ms·

I've been thinking for a while about something like an "assertion based type system." Rather than types being variants of other types, types can be described as

I've been thinking for a while about something like an "assertion based type system." Rather than types being variants of other types, types can be described as other types + restrictions. Functions take variables with types but also come with a list of assertions. For example, it is sometimes useful in graphics to differentiate, in the type system, a 3D vector and a normalized vector (e.g. separate Vec3 and Norm3 types) but there is nothing you can do to actually put this into the type system. In some assertion based system, you would write something like: `type Norm3 = Vec3 v given(len(v) == 1)`. You could cast a Vec3 to a Norm3 which would run the assertion at run time, or you could write a function like `normalize` which always returns a Norm3 (maybe even it comes with its own assertion that len(v) != 0). Then you can safely pass your Norm3s to functions that expect normalized vectors. It's always recommended to make bad states unrepresentable, but it's weird how no language has ever given you a system like this.

kbr 6y ago
I think you might be describing refinement type systems [1]? [1] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type
- kylereeve 6y ago
  I've been reading about that, can't seem to wrap my head around the difference between refinement and dependent types.
  - kbr 6y ago
    I think dependent types are stronger than refinement types because they can encode types that don't necessarily have to be decidable. Refinement types are used for creating subsets of a type, while dependent types can be used for creating arbitrary types based on values. As a result, dependent types are more powerful, but they might be too much if all you need are some constraints on an existing type.
seanwilson 6y ago
Sounds like you're describing dependent types. You've now got the problem that showing your program is correct involves writing maths proofs that show your properties hold in all cases (which is an undecidable problem).
- nine_k 6y ago
  But maybe analyzing all cases is not needed if we know (or postulate) something about the predicates? E.g. we can prove (or just assume since the case is simple) that construction of Norm3 is defined for any triple except (0, 0, 0), and that it is preserved under rotation and under reflection, but guaranteed to be broken under addition. I suspect that if we factor out such basics, the amount of proof for a reasonable function may become manageable.
  - seanwilson 6y ago
    > or just assume since the case is simple That's like what the blog post is about where you're tagging values you assume have a certain property. > I suspect that if we factor out such basics, the amount of proof for a reasonable function may become manageable. It's not obvious how you contain the complexity though and you don't need a lot before it becomes well beyond practical for even experienced programmers. The moment you have to write an algebraic proof where variables are multiplied together you're in the realm of nonlinear arithmetic which is undecidable for example, and writing proofs is hard. Mainstream languages contain the proof complexity by limiting what you can express e.g. it's trivial for the computer to prove "String = String" and "Dictionary = HashTable" as part of type checking.
deleted 6y ago
[deleted]
sankha93 6y ago
What you are looking for are refinement type systems. LiquidHaskell [0] is the most well known refinement type system out there, to specify and verify these kind of assertions. [0]: https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/
lexi-lambda 6y ago
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.
brundolf 6y ago
This is similar to the philosophy behind Clojure's "spec" system: https://clojure.org/about/spec https://clojure.org/about/spec It's mainly concerned with runtime-checking, but the idea is to establish a standard that can be leveraged in multiple ways, from tests to (I believe) some degree of static analysis

kbr 6y ago

I think you might be describing refinement type systems [1]? [1] https://en.wikipedia.org/wiki/Refinement_type https://en.wikipedia.org/wiki/Refinement_type

kylereeve 6y ago
I've been reading about that, can't seem to wrap my head around the difference between refinement and dependent types.
- kbr 6y ago
  I think dependent types are stronger than refinement types because they can encode types that don't necessarily have to be decidable. Refinement types are used for creating subsets of a type, while dependent types can be used for creating arbitrary types based on values. As a result, dependent types are more powerful, but they might be too much if all you need are some constraints on an existing type.

seanwilson 6y ago

Sounds like you're describing dependent types. You've now got the problem that showing your program is correct involves writing maths proofs that show your properties hold in all cases (which is an undecidable problem).

nine_k 6y ago
But maybe analyzing all cases is not needed if we know (or postulate) something about the predicates? E.g. we can prove (or just assume since the case is simple) that construction of Norm3 is defined for any triple except (0, 0, 0), and that it is preserved under rotation and under reflection, but guaranteed to be broken under addition. I suspect that if we factor out such basics, the amount of proof for a reasonable function may become manageable.
- seanwilson 6y ago
  > or just assume since the case is simple That's like what the blog post is about where you're tagging values you assume have a certain property. > I suspect that if we factor out such basics, the amount of proof for a reasonable function may become manageable. It's not obvious how you contain the complexity though and you don't need a lot before it becomes well beyond practical for even experienced programmers. The moment you have to write an algebraic proof where variables are multiplied together you're in the realm of nonlinear arithmetic which is undecidable for example, and writing proofs is hard. Mainstream languages contain the proof complexity by limiting what you can express e.g. it's trivial for the computer to prove "String = String" and "Dictionary = HashTable" as part of type checking.

deleted 6y ago

[deleted]

sankha93 6y ago

What you are looking for are refinement type systems. LiquidHaskell [0] is the most well known refinement type system out there, to specify and verify these kind of assertions. [0]: https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/

lexi-lambda 6y ago

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.

brundolf 6y ago

This is similar to the philosophy behind Clojure's "spec" system: https://clojure.org/about/spec https://clojure.org/about/spec It's mainly concerned with runtime-checking, but the idea is to establish a standard that can be leveraged in multiple ways, from tests to (I believe) some degree of static analysis