Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Names are not type safety

lexi-lambda.github.io

Post reply on HN
Print view View original

31–40 of 130 posts

Re: Names are not type safety

#31

Post by sankha93 »

_28jh wrote: post #25

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 ty…

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/

Re: Names are not type safety

#32

Post by lexi-lambda »

_28jh wrote: post #25

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 ty…

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/

[2]: https://lexi-lambda.github.io/blog/2020/08/13/types-as-axiom...

[3]: https://www.hillelwayne.com/post/constructive/

Re: Names are not type safety

#33

Post by [deleted] »

imoverclocked wrote: post #17
alexmingoia wrote: post #8

Earlier quoted context omitted.

Yeah, I don’t find those points very convincing. Obviously if you export other ways to construct the type, it doesn’t work... It’s like saying “if you forget to sanitize input it won’t get sanitized.” Okay?

The entire point of a good type system is to reduce the need for extra cognitive diligence around your data/code. The more corner cases you have to be careful around, the less helpful the type system is.

[deleted]

Re: Names are not type safety

#34

Post by nine_k »

seanwilson wrote: post #27
_28jh wrote: post #25

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 ty…

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).

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.

Re: Names are not type safety

#36

Post by seanwilson »

nine_k wrote: post #34
seanwilson wrote: post #27

Earlier quoted context omitted.

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).

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…

> 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.

Re: Names are not type safety

#37

Post by embwbam »

chongli wrote: post #30
codebje wrote: post #10

Earlier quoted context omitted.

In Haskell, you would use an algebraic data type that can only hold legal values. You would typically only use a newtype when you're just giving a new name to the same type. Having a Magnitude newtype over Int doesn't change the range of permissible values but does prevent using a Length where a Magnitude was expected, for example. In all typed languages you'll eventually see a function with multiple arguments of the…

How do you write a data type which can only hold legal email addresses? Or URLs? ZIP codes? Or even dates and times? Expressing all of the requirements of these real-world data formats, within a type system such as Haskell's, seems like an extremely daunting task to me. I have programmed in Haskell a fair bit in the past and I have no idea where I'd begin with those.

Practically, I disagree with the GP. A newtype is fine in these cases. You don't have to say you know what to do with negative Lengths if you have a smart constructor that won't let you create one.

Re: Names are not type safety

#38

Post by brundolf »

_28jh wrote: post #25

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 ty…

This is similar to the philosophy behind Clojure's "spec" system: 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

Re: Names are not type safety

#39

Post by lmm »

lexi-lambda wrote: post #18
lmm wrote: post #12

I disagree, and I think this kind of fundamentalism hurts the adoption of type safety. It's like saying that a non-machine-checkable mathematical proof is not a proof - something few working mathematicians would agree with. In a well-formed program it is impossible to have a OneToFive that has not passed through toOneToFive. That's type safety by any reasonable definition. It's not as much type safety as you'd gain t…

Read the article more carefully. I wrote in multiple places that the use of newtypes does provide real safety. > If you are fond of newtypes, this whole argument may seem a bit troubling. It may seem like I’m implying newtypes are scarcely better than comments, albeit comments that happen to be meaningful to the typechecker. Fortunately, the situation is not quite that grim—newtypes can provide a sort of safety, just…

> Read the article more carefully.

This is unnecessarily rude. Maybe you should have written the article more carefully, or read my comment more carefully.

> newtypes are useful, but only when used in certain ways and in a weaker sense than constructive data modeling

Constructive data modelling can be an easier way to provide certain kinds of guarantees in some circumstances, perhaps. But the claim that newtype-based approaches are not type safety remains false.

Re: Names are not type safety

#40

Post by nimih »

eyelidlessness wrote: post #16
lmm wrote: post #12

I disagree, and I think this kind of fundamentalism hurts the adoption of type safety. It's like saying that a non-machine-checkable mathematical proof is not a proof - something few working mathematicians would agree with. In a well-formed program it is impossible to have a OneToFive that has not passed through toOneToFive. That's type safety by any reasonable definition. It's not as much type safety as you'd gain t…

> In a well-formed program it is impossible to have a OneToFive that has not passed through toOneToFive. I think this is the key. In any (type) system, there’s an opportunity to chicanery the compiler. The degree to which you have to treat users of that system like children depends on how likely you think they are to behave badly. If a “well-formed program” is something you can reasonably expect in your environment,…

The whole conceit of fancy type systems is that it's generally useful to move as many things as possible from the realm of "humans must verify" to "computers can automatically verify on behalf of humans". Relying on data representations which are richer or more constrained than newtypes, and treating with suspicion promises the computer can't automatically verify, isn't "treating your users like children," it's acknowledging that you and your users are, eventually and probably frequently, going to forget important assumptions and make mistakes.
Post reply on HN