<story><title>Names are not type safety</title><url>http://lexi-lambda.github.io/blog/2020/11/01/names-are-not-type-safety/</url></story><parent_chain><item><author>_28jh</author><text>I&amp;#x27;ve been thinking for a while about something like an &amp;quot;assertion based type system.&amp;quot; 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&amp;#x27;s always recommended to make bad states unrepresentable, but it&amp;#x27;s weird how no language has ever given you a system like this.</text></item></parent_chain><comment><author>lexi-lambda</author><text>As was already mentioned in another reply, what you are describing are &lt;i&gt;refinement types&lt;/i&gt;. 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.&lt;p&gt;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]&lt;p&gt;[1]: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;ucsd-progsys.github.io&amp;#x2F;liquidhaskell-blog&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;ucsd-progsys.github.io&amp;#x2F;liquidhaskell-blog&amp;#x2F;&lt;/a&gt;&lt;p&gt;[2]: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;lexi-lambda.github.io&amp;#x2F;blog&amp;#x2F;2020&amp;#x2F;08&amp;#x2F;13&amp;#x2F;types-as-axioms-or-playing-god-with-static-types&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;lexi-lambda.github.io&amp;#x2F;blog&amp;#x2F;2020&amp;#x2F;08&amp;#x2F;13&amp;#x2F;types-as-axiom...&lt;/a&gt;&lt;p&gt;[3]: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.hillelwayne.com&amp;#x2F;post&amp;#x2F;constructive&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.hillelwayne.com&amp;#x2F;post&amp;#x2F;constructive&amp;#x2F;&lt;/a&gt;</text></comment>
<story><title>Names are not type safety</title><url>http://lexi-lambda.github.io/blog/2020/11/01/names-are-not-type-safety/</url></story><parent_chain><item><author>_28jh</author><text>I&amp;#x27;ve been thinking for a while about something like an &amp;quot;assertion based type system.&amp;quot; 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&amp;#x27;s always recommended to make bad states unrepresentable, but it&amp;#x27;s weird how no language has ever given you a system like this.</text></item></parent_chain><comment><author>seanwilson</author><text>Sounds like you&amp;#x27;re describing dependent types. You&amp;#x27;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).</text></comment>