Code is also meant to be read and reasoned about by humans, not just by the compiler.
I think a version of this applies to static types as well. Even under normal circumstances, I've noticed at times my own thoughts getting lazy when refactoring statically-typed code. I don't "load" as much of the program into my brain as I would otherwise; I just change the part I want to change and then fairly thoughtlessly fix all the type errors. I don't think this is a good thing. The OP takes this to an absolute extreme.
Static types are there to document and to catch bugs early; they cannot be used as a complete verification that your code is correct, much less a generative tool for writing logic where "you're not entirely sure how" it works.
How good a thing it is depends on how right you are when you do it. If your language is statically typed, but not very well, then it's a bad thing. But it's not just abstractly a bad thing because you are a lazy person who didn't choose to do useless cognitive work, it's a bad thing because you may be wrong. To give a specific example, if your type system forcibly adjoins NULL to all pointer types, you can't afford to take your hands off the wheel when dealing with pointer types and neglect that case. You must think about it when using pointer types.
On the other hand, if you take your hands off the wheel for a moment, but you perform only type system manipulations that you have good and correct reasons to believe won't affect the behavior of the underlying code... then what's wrong with that?
I'm guessing you've used the former type of language more than the latter? Me too. I think you've turned the justifiable fear you feel in that sort of language into a heuristic, which makes it easy to then forget the underlying problems. But there's no particular virtue to having to understand more of the program to do a manipulation than having to understand less. Proof: If that was always true, then that recurses on itself until you shouldn't ever make a change until you understand the whole program completely in your head at once (if not the whole system it is running on). Even if that's true, it doesn't matter; we humans don't have the cognitive capacity for that, we must window our understandings.
It isn't just the micro task of refactoring one particular function; it's completely common for me to undertake a type-driven refactoring of code where just the type-driven aspects are plenty to fill my cognitive window. Especially since I'm usually in a looser language and I really have to watch those darned forcibly-adjoined NULLs. If I'm somehow "obligated" to understand more, the result isn't that I'm going to have that understanding, the result is that my hand will be tied and I won't be able to do that refactoring because it'll blow out my cognitive budget.
I'm not arguing with that. I'm only saying that we shouldn't assume "the types are enough", so long as we have more "cognitive window" available. Here's why:
add :: Integer -> Integer -> Integer
add x y = x + y
add :: Integer -> Integer -> Integer
add x y = x - y
All I'm saying is we shouldn't needlessly ignore the actual logic in favor of "letting the compiler write it for us". That's what the OP is expressly advocating for.
>
I’m not going to say that blindly filling in type holes always works, but I’d say maybe 95% of the time? It’s truly amazing just how far you can get by writing down the right type and making sure you use every variable.
The reason why this works is known as theorems for free, which roughly states that we can infer lots of facts about a type signature (assuming it’s correct.) One of those facts we can infer is often the the only possible implementation. It’s cool as fuck, but you don’t need to understand the paper to use this idea in practice.
One question you might have is “what the heck does it mean for a type to be correct?” Good question! It means your type should be as polymorphic as possible.
On one hand there is a bunch of minus signs in Maxwells equations and there is nothing except historical nomenclature and experiments that can tell you where they go. Nothing in the type system can know if dB/dt is curl(E) or -curl(E). (Note that dE/dt has the opposite sign.) And if you implement say a finite difference stencil you have a bunch of numerical coefficients like (1/24, -27/24, 27/24, -1/24) that are not straightforward to derive. If you go to NSFD these coefficients will actually come out of the numerical optimization run by another code. The compiler will never be able to type check that.
On the other hand it can be quite useful to have the compiler type check variable for correct SI units, so you don't accidentally add curl(E) to B without multiplying by the time step dt. But that is already quite possible with the type system in C++ that is derived by purists as bad and weak. Maybe it could even add checks that stuff in the new time step has to have a change proportional to dt added to it and prevent me from accessing stuff that is not properly time centered. But then again I have not seen anybody write code like that in Haskell that did anything useful.
Having guardrails is nice, but you can not write the entire program in types. And if you try all you get is the same complexity in a unreadable syntax.
The vast majority of the time, we're really working with types like
User -> Permissions -> PermissionType -> Maybe BillingHistory
To the extent that you can't actually depend on your code to not do things like magic permissions into existence... well... this is precisely why that's always a bad idea. Don't write code that does that.
For my Haskell response: In Haskell, when you know how to read the type system, you don't have to use a heuristic to guess whether you should slow down.. the type itself is telling you that you need to be more careful. As a reasonably skilled Haskell programmer using type-directed reasoning, you can immediately read off from "Int -> Int -> Int" that you have a more complicated function than "a -> a -> a". The latter is so "simple" there's only two reasonable implementations, whereas that's only the beginning of what your Int function may do. However, when you have "Applicative f => f (a -> b) -> f a -> f b", you actually can know what that is not doing. The polymorphism tells you you don't have to sit there and study it. It can't magic an "a" into existence, or suddenly decide to use "division" on the resulting "b", because it can't. It doesn't know how. You don't need to worry about it doing those things anymore, because it can't.
For my harmonization of the two: In principle, imperative code can almost always magic values into existence, use globals, etc. One of the reasons I can stand writing in looser langauges like Go is that I just don't do those things. In general, when I write code, if you've got a "Permission" and "PermissionCheckable", I do my best to keep it so there's only one sensible way to combine the two. So, when I'm refactoring my code, even in looser strictly-typed languages, I can still pretty much get away with the type-directed approach. (Backstopped by the unit tests I have anyhow.) It is certainly true that you can write, or be forced to deal with, code that is conceptually mismashed where this is more dangerous, but I'd suggest as you get experienced over the years that you learn to stop doing that.
You might be surprised to learn that this is not only possible but something research is definitely working towards.
In a language like Agda, for example, when there is enough type information available the compiler can fill in the holes for you with the obviously correct implementation.
The idea behind program synthesis drives this even further. Using type level specifications we can automatically derive the programs that meet those specifications. This is useful because the language of types is much more concise than the language of terms. For sufficiently difficult problems it's much easier for humans to reason about complexity in higher-level specifications. Let the computer generate the code!
It's still early on for this kind of technology but projects like Synquid[0] are making good headway.
Dependent-type theory also forms the basis of interactive theorem proving in Coq and Lean[1]. We use something like holes as the basis of proofs. Haskell's typed holes are quite a bit more loose but to me it feels very similar to working with such a system. I propose to Haskell there there exists an expression that satisfies a particular type and then I use the typed holes to fill in my obligations to provide a proof. The hole is my goal and the available objects in scope are my terms. It is a very effective tool for solving hard problems.
[0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-...
[1] https://leanprover.github.io/
update: Links
Yet the humans must still fully consider the higher-level specification. I know that what you describe isn't a compiler per se, but from the perspective of programmer experience it seems analogous. You're not enabling the programmer to "not think", just to think on a more abstracted level. I think the gist of my point still stands; maybe not the final paragraph.
> This is useful because the language of types is much more concise than the language of terms.
actually holds with sufficiently complex types. For example, would the fully-specified type for quicksort actually be shorter than quicksort?
I don't know that there is any reason to believe so. The best we may be able to hope for is that we'll have less work to do for formal verification, since instead of writing both the proofs and the code, we may be able to only write the proofs and have the code for free. However, given that writing the proofs is, at least currently, much, much harder than writing just the code, I'm not sure this type of development would make more than a dent in the software engineering world.
What is the probability that an expert software engineer could write a correct implementation of this algorithm, I wonder? As their colleague will we be able to review that code and notice if it contains an error? What are the sufficient parameters for an acceptable solution: should it run with 8 threads and 2 state variables?
I don't think we'll see these tools and practices become wide spread but I do see the cost of using them is coming down. I also see the number of cases where systems that aren't safety critical are never the less causing harm to property and people. It's possible that at this intersection we'll see the adoption grow: bringing down the cost of writing software that handles higher degrees of liability could be a useful tool to have.
If so, then I think the answer so far is: even though few senior SEs could write correct implementations of that algorithm, there are definitely many more than the number of people who can write non-trivial software with complex dependent types in a decent amount of time.
Of course, you can write code in Idris or Agda and be productive, but not if you want to do stuff like actually proving that your sort function produces a sorted permutation of original list and other similar somewhat rich tight bounds.
The more you want to express in your types, the more complex your program becomes. A very nice example is how you would implement matrix multiplication in regular ways (with matrices of numbers) versus how much more work you need to add if you want to track physical quantities (with proper support for different physical quantities for each value in the matrix). It's easy to say {{1, 2}, {3, 4}} can be multiplied by {{5, 6}, {7, 8}}, but much harder to say if {{1m, 2kg}, {3N, 4Pa}} can be multiplied by {{5m, 6N}, {7Pa, 4kg}}.
My point here is not that dependent type theory is going to take over the industry and we should all learn to write proofs!
It's more that we can if we want to. Writing a proof with tactics in Lean feels a lot like programming with typed holes in Haskell (it's harder but the experience is similar). With training a motivated programmer can write proofs that verify their designs which provide a strong guarantee of correctness.
Whether types are more expressive than programs... I think they are? That seems to be the whole point of Synquid: you can express complex constraints and proofs in your types that enable it to derive the program for you. Is that easier than simply writing the program?
I think one should consider that writing the correct program is harder. And where getting it right matters a lot I hope that synthesis will one day allow us to derive those programs from their specifications (or at least the parts that matter the most). It would save a lot of the burden of proving that the program we wrote implements the specifications.
Haskell's compiler will generate all the logic for serialization and deserialization, leaving me to only implement the actual business logic.
I think you're thinking of a very shallow kind of auto-generation of code, which doesn't include any kind of behavior beyond calling your API.
The GP though was talking about generating the behavior based on the type specification, which is also doable in principle. For example, you could provide a complex type specification for a sorting function, and have the compiler infer the implementation.
For example, you could declare a function which takes a list of `Ord a` and returns a list of `Ord a` such that the second list is a permutation of the first list and each element in the second list is <= to the next element (you of course need dependent types for this). With this type signature, the system could generate the code for a function which achieves this purpose.
However, I do not believe that it will be easier to write that type signature (especially if you want to add properties like stability or time and space constraints) than it would be to write the actual sorting function yourself and sticking with `Ord a => [a] -> [a]`. I also don't think we will see anything like this in the near future that doesn't rely on a large set of pre-defined functions that the system simply fills in.
dependently typed languages also seem woefully unprepared for real systems programming. they are probably good in the small but are so difficult in the large that the costs outweigh the benefits.
In the reusable abstraction space, what you're talking about just doesn't happen. There aren't bugs that need to be hunted down by careful inspection in these things because the methods described in the article are sufficient to catch them. They'll fail to type check or have obvious flaws of the sort -Wall catches.
In the business logic domain, there is a lot more room for errors that can't be caught by those approaches. But code in that domain also can't be written like this in the first place, so it's kind of a strange criticism to say "the code I can't write like this contains bugs that are hard to track down when I try to write it like this."
I can sense one additional objection coming: "If this isn't for business logic, what value is it? I write business programs."
To that, I would answer that most programs are stuffed full of redundant non-business logic, and you don't even realize how bad it is. It took roughly 30 years of c-like languages for people to be fully on-board with the idea that 3-clause for loops are error-prone boilerplate separate from the business logic and worth abstracting out.
If you use Haskell enough you'll realize a lot of your code in most languages is there to fiddle with implementation details instead of working over the actual problem space. A lot of Haskell code takes the form of super-generic abstraction plumbing bits that serve to isolate a common pattern and make sure the edge cases are covered.
Those bits of code are the ones usually called "impossible to understand", which are fully described by their types, and which can be implemented with this approach.
Once I let go of needing to understand how a piece of code turns into CPU instructions, I found that this code is actually the easiest to understand!
This is coming from something who tried that approach and had a bug in production.
And thinking with types helps you to do that. Satisfying the type checker doesn't guarantee a program is functionally correct but it does reject a large number of obviously incorrect programs from being considered. And with holes it can guide use towards the likely correct program.
From TFA:
> I’m not going to say that blindly filling in type holes always works, but I’d say maybe 95% of the time?
It's a tool. If you don't know how to implement something a good first approximation is understanding it's shape and filling in the holes. I think this is the spirit of what the article is demonstrating.
Writing the program so that it's clear is the next step. The final example, `zoop` is renamed to `foldr` once we realize what we're working with. This is how I often work with Haskell in practice: I know the types and shapes of values I need to produce and I work with the compiler to write an expression that fits the type. Then I rewrite for clarity and intent.
Most Haskell code I read in the wild is borderline incomprehensible because of things like poor naming choices. Typically I can rewrite the code to be clearer, but it's a lot of effort.
I think Haskell would benefit from some style guidelines that emphasize that your code ought to be understandable by others. That would at least counteract the natural tendency to believe that terseness is a virtue or a goal.
You can write incomprehensible C too. It's just that most people have stopped doing that.
> just because the types check out doesn't mean it's free from bugs
That's certainly true in the general case. In fact, the author gives a type-checked-but-wrong example of "we need an Int, so just return zero."
But in some specific cases, as the author writes, "One of those facts we can infer [from a type signature] is often the the only possible implementation." The article demonstrates that "possible" includes "also makes use of all the values available (or else the signature would be simpler)."
The trick is to make sure that as soon as you've written this garbage, you go back, split things up into proper methods with descriptive names. Even things like introducing intermediate variables goes a really long way towards improving readability.
To me, this is a starting point, not the finish line.
I am familiar with free monads/extensible effects, so I know the idioms at play in that 1-argument function. We're taking an extensible effect, "peeling" State off it (this is an idiom of EEs) and returning the rest of the effects within StateT. I can now this is a way to interop between the State effect in the effect stack & the StateT monad transformer. I don't give 2 shits about the implementation - I can use this to solve my problems just fine.
EDIT: HAHA - I just realized that this function is called "hoist" which is exactly the name I would've given it based on common Haskell idioms. I didn't even read the name - just the type. That's the essence of Haskell :)
That's fine because you can enter zen state and refactor it using compiler hints ;)