Comment by icen | Hacker News Reader

Comment by icen | Hacker News Reader

Parent Full thread

(Not OP.)

When moving from dynamically/untyped/unityped languages to those with types, you are liberated from having to check the shape of inputs. If you're given something that claims to be a list of strings, it absolutely is a list of strings, and you can proceed without thinking about it's list-ness or string-ness any further.

When moving from a typed language to a dependently typed language, you are liberated from having to check the state of inputs. You don't have to worry that your file handle is closed, or ensure that you update the state of the object correctly to satisfy some protocol (if you don't, you will be picked up on it!). If you are writing a parser, you don't need to check that the parser returned the form that you just called - you know upfront.

There are other niceties: the type of the function is always a very rough exposition of what the function should do. With dependent types, it becomes considerably clearer. Consider these two functions, which could have very similar implementations (in some Idris-like syntax):

    f : Int -> Int -> Bool
    data T : Int -> Int -> Type where
         Tz : T 0 x
         Ts : T a b -> T (a + 1) (b + 1)
    g : (x : Int) -> (y : Int) -> Maybe (T x y)

Given just the structure, it should be a bit clearer as to what's going the functions intend to do.

But wouldn't the actual code tell you exactly what the function does? Why is it beneficial to have a similar version of the same in a more or less different language expressed separately?

The flipside of your description of moving from un typed to typed to dependent typed languages is the amount of specification you need to think about and add to your code. This is awesome for component interfaces, but it can often get in the way of internal code. For example, if I try to redactor a long function and extract a few bits, those bits may only be called with very specific argument values, despite what the types I have on hand (or am willing to define) might say. Languages without some dynamic escape hatches can force you to create code that is too general, or define extremely specific types, for situations that really don't call for it.

It also makes very generic or dynamic code much harder to write, or requiring ever more complex constructions. For example, most mainstream typed languages can't express something as simple as 'a function that returns either an A or a B' without resort g to dynamic typing and casting. And even in Haskell, a lot of code is more loosely typed than might be expected. For example, even though measurement units are often touted as a feature of typed languages, there are no complex mathematics libraries that use measurement units, simply because it is so much effort to correctly type everything, for relatively little gain.

Yes, the actual code will always tell you exactly what it does.

There is always a necessary distinction between specification and implementation: if there weren't, one of them would have no value. We often suggest that the intent of a piece of code should be specified in comments, and this is in that category. This way, the compiler can read your comment and figure out if it needs updating! Languages without dependent types work this way too - but you have to try very hard indeed to be eloquent in type signatures, and being able to talk about values lets you say a bit more.

Coming onto your second point: if the function is only valid for some set of values of the given type, why is it 'not really called for' to create specialised types for it? If you call it with something else and it runs, it will be a bug. Newtypes or wrappers are common patterns.

I think that most mainstream typed languages have common constructs to offer that 'A or a B' value you want: this is solved via inheritance, `Either`, `Result`, or `std::variant`.

Types don't generally specify intent as well as comments do. They still can only tell you what the code does, not really why. They do clarify some assumptions the implementation makes, essentially defining pre- and post-conditions, which you'd normally write in comments if you didn't have types. But at some point, it does get much easier to say 'performs a stable sort' then to define the dependent types to express that the list is sorted and that the order of equal elements doesn't change.

My point about newtypes and wrappers is that they are almost pure overhead for helper functions. There is a reason why we don't define precise types for each of our intermediate calculations in general, and this doesn't change when we move those computations to a separate function.

Finally, inheritance is not a real solution for returning A or B, with inheritance I can only return a C that both A and B derive from, and this C often doesn't exist and can't be added post-hoc. What you normally do is go for Object or void*, which is much closer to dynamic typing than inheritance. And most mainstream typed languages don't have Either or Result. C++ with std::variant is the only exception, I forgot that it was added. BTW, I should be more explicit - the way I see it, the mainstream typed languages are Java, C#, C, C++, and maybe Go.

Reply on news.ycombinator.com