12 ms·
Names are not type safety
- seanwilson 6y ago> Newtypes are useful when carefully applied, but their safety is not intrinsic, no more than the safety of a traffic cone is somehow contained within the plastic it’s made of. What matters is being placed in the right context—without that, newtypes are just a labeling scheme, a way of giving something a name. What's a better alternative though? I like this approach for tagging e.g. user input that has been checked to be free of HTML/JS injection hacks to stop you from outputting user input that hasn't been checked first (Angular does something like this with TypeScript I think). Obviously you could tag something as safe that isn't by mistake but at least the places in your code this decision is made is explicit and you can't forget to do it. I'm not seeing a practical alternative that would be significantly better. If you want to be able to capture any property you can think of in the type system (like bounded integers or bounded lists), you're inevitably going to need dependent types and they're about as far from practical as you can get (where either you or the computer will then have to write difficult maths proofs before you know your code is correct).
- tbroadley 6y agoApplying the author's "parse, don't validate" concept, I think you'd parse the user input into a "safe HTML" type with a definition that excluded the language features that enabled those attacks. It might not be worth writing such code for a single project, but I could get behind a library that did that.
- p1necone 6y agoThis is an approach I've used in C#/Java - you have 'UnvalidatedFoo' and 'ValidatedFoo' types, UnvalidatedFoo has a public constructor, ValidatedFoo has a private constructor. The only way to acquire a ValidatedFoo is to pass an UnvalidatedFoo into ValidateFoo(). The outer layer of the code deals in UnvalidatedFoos, but past that point you must have a ValidatedFoo to continue.
- dodobirdlord 6y agoAn extremely good example I've found for this is canonicalization in all forms. Frequently there are scenarios where there are many ways to represent something, but only one official Right Way. https://en.wikipedia.org/wiki/Canonicalization#Usage_cases https://en.wikipedia.org/wiki/Canonicalization#Usage_cases
- nyanpasu64 6y agoDoes "parse, don't validate" apply regardless if the resulting type is a newtype or constrained by construction?
- tbroadley 6y agoI'm not sure I see how "parse, don't validate" would apply when using a newtype—would you mind explaining further? I think the main point of this article is that newtypes aren't an application of "parse, don't validate". If you validate that user input doesn't contain XSS, then wrap it in a `SafeHtml` newtype, that's validation, not parsing. The article outlines ways that you could wrap the user input but forget to validate. By contrast, suppose you have a type like `type SafeHtml = TextNode Text | DivNode SafeHtml | ...`. You parse the user input into a value of this type. If the parse fails, it's because the user input contained something unsafe. The article contends that it's harder to accidentally wrap an unsafe string, since you have to parse a safe HTML string to get a value of type `SafeHtml`. (Although I'm not sure I buy that last point. With both methods you'd want to keep the `SafeHtml` type's constructors in a module and not export them. Otherwise you could wrap arbitrary text in the newtype or in the `TextNode` constructor. Both seem equally possible to me.)
- nyanpasu64 6y agoReturning an Option<newtype> is closer to "parsing" than returning a bool.
- alexmingoia 6y agoThe way to ensure type safety of new types is smart constructors: https://wiki.haskell.org/Smart_constructors https://wiki.haskell.org/Smart_constructors You have a constructor function which does the input check, and it lives in a module that only exports the smart constructor, not the type constructor. It doesn’t matter if another module deconstructs the type, since the input was already checked. For example: newtype Username = Username Text mkUsername :: Text -> Either Text Username mkUsername t = if t == “” then Left “Username cannot be blank” else Right (Username t) If you don’t export the constructor for Username, and only export mkUsername, it doesn’t matter if someone deconstructs the Text from Username, because it must already be validated.
- shawnz 6y agoThe article gives some examples why smart constructors don't fully solve the problem in the section "Newtypes as tokens"
- alexmingoia 6y agoYeah, 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?
- imoverclocked 6y agoThe 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 6y ago[deleted]
- remexre 6y agoI've gotten bit by the Generic one in real code before... I'm sure if I used Haskell for RESTful web stuff more, I'd eventually get bit by something similar for Aeson too.
- shawnz 6y agoMaybe you can solve it like this: internally represent the document as DOM objects. Have element nodes contain a list of children which can be either raw strings (representing text nodes), or other element node objects. The render function of element nodes would know to escape the contents of text nodes before concatenating them with their rendered element node siblings. It would be type safe since it knows all the types of children it can contain. It's like SQL parameterized queries: delay the concatenation until the last possible moment to reduce the area where errors can occur. But I think maybe that just moves the opportunity for error to the render function, so I don't know if that is really an improvement on "smart constructors".
- codebje 6y agoIn 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 same type and have to check the documentation (or worse, implementation) to know what each is for. Having a zero cost type alias to make it clear is an improvement and IMO is a form of type safety. Having a data type that can hold illegal values is a bad idea. Using an Int for Length implies you know what to do with negative lengths, for example. A newtype won't help there.
- alexmingoia 6y agoAre you suggesting using Proxy to create a type that masks an Int? How would you deal with text that can only contain certain characters for example?
- codebje 6y agoIn the Length case I'm more suggesting to use an unsigned integer type than any more complex type system trickery to specifically limit the range. There are type systems that let you declare a new type to be a sub-range of an existing type, but Haskell's is not one of them.
- alexmingoia 6y agoDependent types don't provide any safety over smart constructors for parsing, which is the most common use case for types with restricted values. Validating user input, parsing emails or URLs, etc. all must deal with an invalid case at runtime, and dependent types are of no use there.
- remexre 6y agoWhat dependent types would protect you against would be the parser itself returning data. I think it'd be quite difficult to do this for the case of an email or URL, but for cases like "length values must be non-negative," a parser/validator with a type like parseLength :: JSON -> Either Error (Sigma (l : Length). lengthToDouble l >= 0.0) is reasonable, and I'm sure somewhere in the literature there's an indexed monad or something for building parsers/validators out of these, that keeps track of the properties while combining parsers like these.
- skybrian 6y agoIt seems to me that there is no practical alternative. The impractical alternative is to extend the language so that its type system implements the feature you want. (For example, adding bounded integers.) I don't see how that helps, though, because there could be bugs in your language extension, and it has to be maintained. It's just going about it the hard way. It would be sort of like avoiding "unsafe" in Rust by extending the compiler instead.
- p1necone 6y agoThere's a lot to be gained by isolating the place where the validation needs to be done, and the source of the bugs could be to one place though. Would you rather have one bit of code that checks 1<=X<=5, or 100 call sites all doing the same thing slightly differently?
- skybrian 6y agoThere ways to do that without type system level hacking.
- lexi-lambda 6y ago> What's a better alternative though? I’m not really suggesting there needs to be an alternative. Using newtypes to achieve safety via encapsulation is fine, good even, and I say as such at several points in the article.[1] The point is twofold: 1. A lot of uses of newtypes in the wild are “safety theater” and provide zero actual safety benefit. 2. The uses of newtypes that do add safety provide it in a weaker sense than correct-by-construction data modeling. The point is not that newtypes are always useless. In fact they are often by far the most practical tool for the job. The blog post just advocates being conscious and considerate of the limitations of the techniques. [1]: https://news.ycombinator.com/item?id=24964494 https://news.ycombinator.com/item?id=24964494
- PhineasRex 6y agoSo in the example where you're constructing HTML, you would never use strings to represent your HTML. So your template might look something like ``` P(Text(someUserText), I(someItalicized)) ``` This is essentially how React.js works; you don't need to tag strings as safe or unsafe because strings are never treated as HTML, only constructed HTML values (via JSX) are treated as HTML.
- imoverclocked 6y agoThis is an excellent article that clearly outlines a conversation I had with a co-worker last week; Type systems are usually only as helpful as the developer allows them to be.
- lmm 6y agoI 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 through explicitly modelling the internals, but that's a difference of degree, not kind. Sure, using `Generic` or any number of other things lets you break your rules - but so does using `unsafeCoerce` on the constructive version. I'd argue that newtypes provide a better cost/benefit than essentially any other language feature. The author purports to embrace the idea that the type system is a tool to be used pragmatically, but that's exactly what using a newtype does: you enforce that appropriate checks are applied to any use of any given type, but what's "appropriate" is an internal concern for that module. Whereas expecting to be able to construct every domain datatype rigorously from first principles is simply not realistic in a lot of business cases; that constructive model may well be opaque or simply not exist for the domain you're working in. (Yes, this may well mean the domain you're working in is fundamentally incoherent - but if that incoherence is present in the real process that you're modelling, then your model has a responsibility to faithfully reproduce it). This kind of newtype use can be done compositionally - one module can be reasoned about without needing to understand the internals of the modules you're depending on - which is the essence of practical, effective programming tools. A technique that only works in a "closed world" will always be severely limited in its applications.
- eyelidlessness 6y ago> 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, you can also reasonably assume you also received a nominal type because it was validated. If it’s not, the expectation is that someone is lying to the compiler... and then you treat someone like they’re misbehaving. Even if they’re not.
- sillysaurusx 6y ago(The following comment may not have anything to do with Haskell’s use of the word “name,” but I’ve wondered about this for a long time.) Forcing someone to write iFoo instead of foo isn’t type safety, but it’s a certain kind of safety that I haven’t seen clearly spelled out. Actually I recall Joel on Software mentioning it once. I don’t like it, but it’s always seemed interesting. Another example is in lisp: *current-input-port* to indicate that a variable is dynamic, you can end it with an asterisk. But this is only a convention. I’ve always felt that LET should automatically do dynamic binding for any name that ends with . But then of course that runs into surprising corner cases when the user wants to e.g. write foo-+ foo-/ foo- foo— You could argue that names aren’t type safety, but I would disagree that they aren’t any kind of safety. A good naming convention is one of the safest ways to program in an otherwise hostile domain. But that raises the question: what kind of safety is it? I’m not sure it even has a name, other than Hungarian notation, which is both imprecise and not sufficiently general for the concept. EDIT: Ah, the post was “Making Wrong Code Look Wrong” by Joel on Software: https://www.joelonsoftware.com/2005/05/11/making-wrong-code-look-wrong/ https://www.joelonsoftware.com/2005/05/11/making-wrong-code-... (with discussion from 11mo ago: https://news.ycombinator.com/item?id=21482993 https://news.ycombinator.com/item?id=21482993) The idea really should have a name.
- pwm 6y ago> Forcing someone to write iFoo instead of foo isn’t type safety, but it’s a certain kind of safety The term I'd use (at least from the top of my head) is hygiene. The article uses the word safety in a restrictive sense, ie. preventing errors. Forcing iFoo instead of foo, to me, is more about hygiene where one could still potentially make an (accidental or deliberate) error but that would go against said hygiene. Maybe another way to put it is that safety prevent misuse while hygiene guides correct use. Or another is that with safety the letter and spirit of the law are one and the same while with hygiene it's not. Haskell's `newtype` is an amazing tool for (proactive) hygiene and, as the article says, a limited tool for safety. By proactive hygiene I mean that if you have: bmi :: Float -> Float -> Float Looking at it you don't know what those params are. They are all just `Float`s. There's not vocabulary to them. Meanwhile here: newtype Height = MkHeight Float newtype Weight = MkWeight Float bmi :: -> Height -> Weight -> Float It is both clear what they are as well as the compiler will prevent you from passing `Weight` as the 1st param. Now it's not safety as you can still wrap the wrong `Float` as `Height` but that would go against the hygiene.
- howenterprisey 6y agoFurther reading, featuring the vocabulary words "Apps Hungarian" and "Systems Hungarian", and opening with a lovely anecdote about baking: https://www.joelonsoftware.com/2005/05/11/making-wrong-code-look-wrong/ https://www.joelonsoftware.com/2005/05/11/making-wrong-code-...
- identity0 6y agoI'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 agoI 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 agoI've been reading about that, can't seem to wrap my head around the difference between refinement and dependent types.
- kbr 6y agoI 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 agoSounds 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).
- jasonhansel 6y agoOne note: instead of using module boundaries to limit how a value can be used, you can use existential types instead. This is essentially equivalent to how encapsulation works in OOP languages.
- quickthrower2 6y agoThe idea of needing a 1-5 compile-time constrained value is rare in any application I have worked with, because either you'd use an enum, or the "5" isn't really known at compile time. (I thought about this when doing some basic Idris lesson.). It makes me wonder what the constrained type might be that I do need? A non-negative floating point number would be a common one I think, e.g. for a coordinate. I've not been keeping up with Haskell but can you guarantee this at compile time? I guess it would be hard to do so, because every assignment to this from a normal floating point would need to be checked, requiring you "prove" that the number is non-negative at compile time, so back to Idris I guess? E.g. x:Positive, x+5 -> this is now a normal float, or I need to prove x+5:Positive. I have only haskelled a little bit, but I would think most of the newtypes are mostly to trace the meaning of something. E.g. Latitude, Longitude, X, Y, WeightKg, and so on. These would be hard to constrain (and to what..?) they are just floating points.
- runeks 6y ago> The idea of needing a 1-5 compile-time constrained value is rare in any application I have worked with, because either you'd use an enum, or the "5" isn't really known at compile time. The OneToFive-type is used to illustrate a point, not because it’s practically useful. > A non-negative floating point number would be a common one I think, e.g. for a coordinate. I've not been keeping up with Haskell but can you guarantee this at compile time? No. It’s not possible. But, as you point out, this is not a problem since values like these are rarely known at compile-time. And, more importantly, if you can’t trust a programmer to write the correct constant, how can you trust the same programmer to write the correct type for this constant (“non-negative float”)? Except by using a quasi-quoter (which amounts to parsing a string into a float at compile-time)
- runeks 6y agoIt should be noted that the -- to use the terminology of the article -- extrinsically safe example module Data.List.NonEmpty.Newtype can be converted into an intrinsically safe one by changing the definition of the NonEmpty type from newtype NonEmpty a = NonEmpty [a] to: newtype NonEmpty a = NonEmpty (a, [a]) (and changing the associated functions accordingly -- which can now be implemented without the use of error). EDIT: Upon further thought, I'm not sure the above distinction makes sense. The implementation of e.g. Data.List.NonEmpty.Newtype.head would still involve the use of "error" through the use of Data.List.head: head :: NonEmpty a -> a head (NonEmpty (x, [])) = x head (NonEmpty (_, lst)) = Data.List.head lst
- ImprobableTruth 6y agoWhy would you use Data.List.head rather than just matching on lst?
- runeks 6y agoI realized the example doesn't make sense for head, since head should always just return the first item of the tuple. I still think it would make sense to define e.g. last using Data.List.last: last :: NonEmpty a -> a last (NonEmpty (a, [])) = a last (NonEmpty (_, lst)) = Data.List.last lst which is safe even though Data.List.last contains error.
- ImprobableTruth 6y agoYou can avoid the error of Data.List.last by 'inlining' it (just like you could in your first example) last :: NonEmpty a -> a last (NonEmpty (a, [])) = a last (NonEmpty (a, x:[])) = x last (NonEmpty (a, x:xs)) = last (NonEmpty (a, xs))
- runeks 6y agoI see your point. But I’d argue that you avoid it in both cases, since without inlining the error-call is unreachable anyway.
- mcv 6y agoI 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.
- piaste 6y agoRange types in the Pascal family, unless I'm mistaken, are not checked for legitimate values at compile time - they just crash at runtime if you try to create one with an invalid value. Syntactic sugar for an assert statement in the constructor. It's usually quick and straightforward to replicate the feature in a modern language with generics and first-class functions. When people refer to 'type safety', they almost always mean compile-time safety. Not just ensuring that a value of 6 cannot exists, but ensuring that none of your code is trying to create one. The unwieldy enumeration allows that.
- aliceryhl 6y agoThe 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<u8>. 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.
- the_mitsuhiko 6y ago> 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.
- ChrisSD 6y agoWhy not? That would seem useful if other code depends on having a validated email address.
- the_mitsuhiko 6y agoI point you to the article.
- ChrisSD 6y agoThe article doesn't exactly make a case against it. It even explicitly says it's useful! It just says making a newtype isn't as strong a guarantee as a proper type. Newtypes do work to assert certain checks have already been done and need not be repeated.
- runeks 6y ago> Exactly what? I'm not sure what you're referring to here exactly. "Newtypes as tokens"
- aliceryhl 6y agoOf newtypes. I gave several examples of them. The String type _is_ a newtype that outlaws some of the possible values of the underlying type, namely non-utf8 byte sequences. I wasn't talking about people using Rust, but about the standard library. That said, I have personally used newtypes a reasonable amount, mostly for making sure I don't mess up different kinds of database ids.
- brainzap 6y agoAnd types are not names.
- benibela 6y agoIn Pascal you can easily create such a type OneToFive = 1..5 It should inherit all the normal arithmetic, but does not allow values outside the range However, these kind of types are causing a lot of problems. You do arithmetic on them, get a value outside of the range, and then it throws an exception. And an unhandled exception crashes the program, which is often worse than an invalid value. And it is slow when it has to check if the value is in the range after every arithmetic operation, so you can disable the range checking to make it faster. But then you get values outside the range without an error The language also assumes everything can be initialized to zero. It just calls "memset" on a allocated memory, so it can be initialized quickly. So you often get values that are zero whatever the range is And you cannot even check for that, because the compiler knows what values are valid. So if you want to check if the variable has a valid value and write (value >= 1 and value <= 5), the compiler knows it is supposed to be always true, and optimizes it away.
- 0xFluegel 6y ago> And an unhandled exception crashes the program, which is often worse than an invalid value. Please elaborate. Why is working with garbage better than not working at all? Would it not also rather make it easier to find these out-of-range cases with fuzzing?
- benibela 6y agoIt is better in GUI applications. You have 1% of code dealing with user data, and 99% of code doing other things For example, a text editor. If it crashes, you lose all your text since the last save, which is very bad. But the editor also does other things like playing animations when you click somewhere, a lowering button, or a show a rotating hourglass as mouse cursor. If it would show a wrong animation, that is completely irrelevant. Or it has syntax highlighting with a range type for possible user-defined colors. If it shows the wrong color, that is no big deal. But if you have a new version of the editor, adding more colors, and you use those colors in the user's setting, you cannot downgrade to an older version, because it would crash when it does not know the new colors. I just had an actual problem with such an exception when calling GetFileAttributes. It returns INVALID_FILE_ATTRIBUTES (unsigned 0xFFFFFFFF) on failure. But I was calling a wrapper around it, which casts it to a signed value and then return -1. Storing the return value in an unsigned variable and then comparing it to 0xFFFFFFFF gave me a range check error. But compiled with range checking disabled, it works perfectly fine.
- sparsely 6y agoI believe that Ada, or perhaps a specific subset with some extensions, achieves most of these goals. You can definitely restrict types to be a range or enumeration of e.g. ints, and they have some facility for contract based function interfaces.
- MaxBarraclough 6y agoYes, this is a feature of standard Ada. https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Named_subtype https://en.wikibooks.org/wiki/Ada_Programming/Type_System#Na...
- jerome-jh 6y agoI do not see the problem with newtype, but rather with fromOneToFive and toList. As soon as you use them, you are left with an Int and a List. So why complain safety is lost when it has been intentionally lost? If the compiler does not provide safe ways of working of newtype's, the programmer indeed has to provide them in the form of methods, basically just as shown in the article.
- devit 6y agoThe real issue is the lack of dependent types in Haskell (and unfortunately Rust and all languages with a vast ecosystem). With dependent types, you can just include a type-level proof that x <= 5 in the integer wrapper type, which then allows to statically check that the default case in the match is impossible. A newtype including such a dependently-typed proof is the correct solution to this problem, since it can be generalized to any range, unlike the enum with 5 variants.
- rowanG077 6y agoIt's possible to do this in haskell but it's quite clunky.
- im3w1l 6y agoThis really makes me wish I was programming in Haskell, makes me feel than anything else is cowboy madness.
- chriswarbo 6y agoThinking about safety and security can benefit from a threat model: what sort of things do we expect to happen, and are we trying to prevent? I think of safe handling of user input as "first order safety". Server-side code handling arbitrary input from the network should use an adversarial model: assume that users will exploit any weakness we expose, no matter how convoluted. Program/library architecture and design is more like "higher order safety": we're not directly preventing attacks, we're preventing code-which-allows-attacks. I don't follow an adversarial approach here: I'm not trying to stop a rogue developer from inserting backdoors into a project, I'm trying to catch and prevent mistakes from being made. If there's a correct-by-construction way to approach certain problems then I'll gladly use it (e.g. one of my current projects uses NonEmptyString, NonEmptySet and NonEmptyList, which use a (head, tail) pair to guarantee non-emptiness). If that's not practical, but there is a way to encapsulate problematic code using newtypes and modularity, then I'll take that (e.g. this project has a NoSpace newtype for strings without whitespace). If it's not practical to encapsulate problematic code, then I'd still rather make it obvious when something dodgy is happening, e.g. even if a 'StatusCode' is isomorphic to a String, the minor cost of wrapping it up in a newtype is worth it to prevent obvious mistakes like appending semantically distinct values. It's all about bang-for-buck. I also agree that type synonyms usually aren't worth it. The extra cost of introducing a newtype isn't much, and it buys us a lot more in terms of ruling out problems, making conversions more explicit, better error messages, etc.
- ronlobo 6y agoVery interesting read, thanks for putting that together. I am wondering how these ideas relate to "value objects", a term formed many years ago via domain driven design.