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

61–70 of 130 posts

Re: Names are not type safety

#61

Post by mcv »

I don't know much about Haskell, but I was struck by this:

> "Suppose we want a type for “an integer between 1 and 5, inclusive.” The natural constructive modeling would be an enumeration with five cases"

Does that really make sense? Using an enum for a limited integer type? I realise most languages don't actually support true limited integer types, but if I recall correctly from my introductory programming classes 28 years ago, Modula2 does allow you to specify a number type with a range of acceptable values. I don't think I've seen that in any other language, but it sounds like an incredibly useful feature if you want type safety.

Re: Names are not type safety

#62

Post by ImprobableTruth »

lexi-lambda wrote: post #32
_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, softwa…

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

Re: Names are not type safety

#63

Post by aliceryhl »

The Rust standard library has many examples of exactly this, except with unsafe to assert that the unreachable cases can't happen. A classic example is the String type, which is just a newtype around Vec. Other examples include CStr, NonZeroUsize and PathBuf.

Arguably even File is an example of this. Internally, it's just an integer for the file descriptor.

Re: Names are not type safety

#64

Post by the_mitsuhiko »

aliceryhl wrote: post #63

The Rust standard library has many examples of exactly this, except with unsafe to assert that the unreachable cases can't happen. A classic example is the String type, which is just a newtype around Vec . Other examples include CStr, NonZeroUsize and PathBuf. Arguably even File is an example of this. Internally, it's just an integer for the file descriptor.

> has many examples of exactly this

Exactly what? I'm not sure what you're referring to here exactly.

Generally newtypes in Rust are not used excessively and largely for sensible safety assertions. I don't see people making `EmailAddress(String)` newtypes.

Re: Names are not type safety

#65

Post by ChrisSD »

the_mitsuhiko wrote: post #64
aliceryhl wrote: post #63

The Rust standard library has many examples of exactly this, except with unsafe to assert that the unreachable cases can't happen. A classic example is the String type, which is just a newtype around Vec . Other examples include CStr, NonZeroUsize and PathBuf. Arguably even File is an example of this. Internally, it's just an integer for the file descriptor.

> has many examples of exactly this Exactly what? I'm not sure what you're referring to here exactly. Generally newtypes in Rust are not used excessively and largely for sensible safety assertions. I don't see people making `EmailAddress(String)` newtypes.

Why not? That would seem useful if other code depends on having a validated email address.

Re: Names are not type safety

#66

Post by one-punch »

lexi-lambda wrote: post #32
_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, softwa…

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

Re: Names are not type safety

#68

Post by one-punch »

ImprobableTruth wrote: post #62
lexi-lambda wrote: post #32

Earlier quoted context omitted.

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, softwa…

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

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

[2]: https://www.youtube.com/watch?v=10gSoVZ5yXY

Re: Names are not type safety

#69

Post by the_mitsuhiko »

ChrisSD wrote: post #65
the_mitsuhiko wrote: post #64

Earlier quoted context omitted.

> has many examples of exactly this Exactly what? I'm not sure what you're referring to here exactly. Generally newtypes in Rust are not used excessively and largely for sensible safety assertions. I don't see people making `EmailAddress(String)` newtypes.

Why not? That would seem useful if other code depends on having a validated email address.

I point you to the article.

Re: Names are not type safety

#70

Post by loup-vaillant »

quietbritishjim wrote: post #54
CyberRabbi wrote: post #46

Earlier quoted context omitted.

Hmm asking to read something more carefully is not rude if the commenter is refuting a point that was never made in the article.

It would suffice to say "that point was not made on the article".

That's unnecessarily cautious. Unfounded criticism rightly deserves a slap on the hand, and "Read the article more carefully" is a very light one.
Post reply on HN