---
> "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that
Actually languages can help a lot.
This isn't just about "silly mistakes". Compilers are _theorem provers_. Quite literally there's an equivalence between type theory and mathematical logic. I hope you're not saying that math logic doesn't help in modeling real world semantics.
So yes, via modelling types in an expressive language you can at least have proof that the changes you make are consistent with the world view you had before those changes.
Of course people accustomed to less expressive languages like Java won't believe this until they see it. But you should really look into Haskell to see the difference. And dependent typing brings this to the next level.
This is more effective than trying to remember to always check the head function in every single place you ever try to get the first element of a list.
Yes, you can still write a compiling but wrong program. But it will likely be pretty close to what you actually want it to do, and it's easier to notice the behavior is not what you expected in one place, enforce that behavior via types, and see where you went wrong through compiler errors.
Programming usually happens in the context of a business, and the technology used has implications in a cost/benefit analysis.
Being able to express invariants at the type level is cheaper for a business at scale.
If you consider this huge overhead in development cost, maybe time is better spent in less intrusive ways of improving software reliability.
My impression is that advanced type systems interest people because they're cool moreso than because they're practical tools for reducing errors.
The kind of discussion I see on this post generally reinforces my impression.
FWIW, I'm not suggesting moving everything possible into types. I'm suggesting types are better than not having them, just like tests are better than not having them.
I don't know, maybe there is a good way of structuring the software to avoid this effect (I'm not extremely invested in type systems), but maybe it's just a lot of additional pain on top -- too much perceived pain for people who can barely make their software "seems to work".
And if I then look at the actual data transformations behind all this code: It would be a 2 day exercise in Clojure to re-build this from scratch.
firstly, the most available `head` function crashes on half the constructors.
more fundamentally, just try using any file or network io method. you just won't have a clue how it can fail, because it isn't even documented.
there's many methods where the best you can do is work out what exception is being used to wrap a C errno and read the appropriate Linux man page.
at least C documents it's functions that can return errors, and usually encodes them in the type. in Haskell, it's just, "if you're dumb enough to use IO (and what alternative have you got), anything can crash all the time. deal with it".
Haskell is great right up to that point, but that's a critical point.
(I've tried to find ways to deal with this, but the most people seen to refer too something else when discussing how horrible exceptions are, so I wonder if I'm insane)
I suggest you come to https://www.reddit.com/r/haskell/ if you'd like more discussion about it. We often have threads wishing for partial functions to be removed from base!
it won't let me know how or if the function you wrote will throw an exception, or what kind of exception it will throw, unless it's documented in the type.
but my objection is that many times, the possibly of failure is only present in my generic, language/api agnostic knowledge that a file might not be readable or a ship might drop an anchor on a cable. having thought about it, I then have to read the source code to understand what exception might get thrown, so I can prevent my program from crashing.
(i would prefer it to continue as best as it can in the case that some api is unavailable, which is obviously a usecase dependent decision)
At least some of these sorts of bugs (depending on how you define "fail") are captured even in Haskell today by things like Maybe. In fact, if Haskell was total (like Idris) you wouldn't even be able to write a function that searches a list for an element with this type:
find :: (a -> Bool) -> [a] -> a
Dependent types go further and let you guarantee things like "zip only compiles for two lists of exactly the same length" which can be helpful in some circumstances (specifically in Haskell we use things like zip [0..] too often to want to change the function literally called zip, but you could imagine another name, perhaps zipExact as in the Safe library).
I suspect you probably already know this and meant a different kind of failure, such as mathematically invalid (which you could probably encode via a sufficiently powerful type system), or a simple misunderstanding of the requirements (which you—as the misunderstander—obviously can't).
in principle, only if you can prove you don't use the result. there's nothing wrong with not calculating a value that doesn't exist.
Now you have n, m, and xs : List Int n, ys : List Char m, and you want to do zip xs ys but m doesn’t “unify” with n so the type is wrong. So you have to do an equality check at runtime which gives you a proof of equality or inequality. In the equal case you have a value of type “n == m” and then you can use a language feature to rewrite the type of xs (or ys) according to this equality.
This was written on a phone kind of hastily but maybe it makes some sense.
zip : Vect n a -> Vect n b -> Vect n (a, b)
Don't dependent types happen at run-time?
Dependent types in Idris occur at compile time and are erased as part of compilation. At runtime, those Vects do not carry around any length information.
It seems like you would have to solve the halting problem for them to work at compile time.
Idris addresses this by having a totality checker. Every function in Idris is marked as either total (known to halt, barring any bugs in the totality checker) or partial (possibly not halting). Only total functions are allowed in types. For example, the function append:
append : Vect m a -> Vect n a -> Vect (m + n) a
So how does the totality checker work? Wouldn't that purport to solve the halting problem? No, the totality checker in Idris isn't magic, it's conservative about what it considers to be total. In order for it to declare a function total, it must identify at least one argument that progresses towards a base case at every step. It can do this even with mutually recursive functions.
In practice, if you write an interactive program in Idris, you can make every function total except for main, which presumably contains an infinite loop that checks for input forever.
It's more accurate to say that Idris can guess an implementation of the function, but it's not the only possible implementation with that type. There's nothing in the type to stop the function from reversing one or both of the lists before the zipping stage, for example. More generally, it could randomize the order of elements in one or both of the supplied lists.
It's interactive, though, and it's extremely fun to use. It gives you the feeling that you're solving a puzzle, and like a good puzzle game, it can do the obvious bits for you.
It is a serious shortcoming that even when you pay the complexity cost of dependent types, you still can't specify the intent in this case. I mean, the semantics of "zip" can't be specified with a type. You can define a "sorted list" or "ordered list" type, but you cannot enforce maintainance of the natural, arbitrary order of list elements. In this sense dependent types are both too complex to reason about and simultaneously not powerful enough to fully specify the function.
rzipWith :: (forall a. f a -> g a -> h a) -> Rec f as -> Rec g as -> Rec h as
zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith f as bs = recToVec (rzipWith f' as' bs') where
as' = vecToRec (fmap Const as)
bs' = vecToRec (fmap Const bs)
f' (Const a) (Const b) = Const (f a b)
vecToRec :: Vec n (f a) -> Rec f (Replicate n a)
recToVec :: Rec (Const a) as -> Vec (Length as) a
Right, for instance I wouldn't be surprised if "the least amount of work" here amounted to reversing both lists as you zip.
You're completely correct in the first half of that but the languages really can help there. Dependent types can be a lot more expressive and capture finer details of your semantics than what you're probably used to.
I simple example is the `pop` function of a List. In Python, you could put strings in a list element. With Java, you can enforce the type of element that goes in a list. In a language with dependent types, you can ensure at compile-time that `pop` can only be called on a non-empty list and returns a list of `length - 1`.
I'd say the difference between Haskell and C are orders of magnitude, not just a difference between 50% (probably a lot lower) and 90% (which would require you to specify the entire contract, at some point you may end up reimplementing business logic inside the type signature at which point you could have bugs there too and you haven't won that much. You still need to use it right). In dependently types languages, it's not unheard of with type signatures longer than the implementation itself.
There is of course no silver bullet, but expressive type systems can protect you against unintended behavior and significantly reduces the number of unit tests you'd need to write.
BTW, buffer overflows etc are a bit orthogonal to this, as that's related to memory safety, not type safety.
app : Vect n a -> Vect m a -> Vect (n + m) a
app Nil ys = ys
app (x :: xs) ys = x :: app xs ys
With dependent types some of the logic will be coded in types, and we would need to check those.
Doesn’t mean it might not be useful.
The simplest example is very common banking and e-commerce logic which is basically a series of checks in the form:
if <some piece of data retrieved at runtime at that particular moment> is consistent with <multiple other pieces whose number and relevance depends on that data retrieved at runtime from potentially multiple sources>.
This isn't true. It's possible to write a symbolic differentiation system using, primarily, Scala's type system. In an elegant fashion.
Similarly, Julia represents math better than, say python or Java. A vector type should not need to know about inner products of vectors, because the math definition of a vector space does not.
This will have large effects on how easy it is to decompose your code into neat little pieces.
I'm not sure that's even it. It's "I don't really understand the requirements until I try to implement them and therefore my first 6 attempts are hopelessly wrong".
The reason dynamic languages are so popular I think is because they make it so fast to iterate through the first 6 attempts whereas statically typed languages make that 50% slower and that generates a huge feeling of helplessness and frustration that you keep doing all this work to satisfy the compiler and then its thrown away.
Of course one can argue that all these people are stupid and should just understand the requirements in the first place, but it's a separate point: that is reality - people find it hard to understand requirements.
But it is one reason I like more "incremental" languages like Groovy since I can iterate really fast in dynamic mode and then tighten up all the screws afterwards by converting it to statically typed code.
But it probably could be true for a lot of languages, but for Haskell, the set is much smaller
Dependent type can let you achieve some degree of semantic correctness above that. Either by refined types or proof. But it's not generally applied because there are a lot of things we just couldn't prove yet.
Dependent types aim to address exactly "How do I capture this extremely complicated real world semantics in code?". Except now you have the option to capture some or all of those semantics in types instead of terms.
Probably a tangent but I feel like this is only partly true. DSLs are specifically built to do that for example. The languages can meet us half-way so to speak.
> How do I capture this extremely complicated real world semantics in code?
This is why I keep using Python after having dabbled in other more interesting languages: the probability of writing correct code for me and the team I support is fairly high.
Out of all of those, I've pretty much stayed with Python as it keeps letting me get my job done with minimal code and maximum readability. I've been almost as efficient in Julia and have gradually picked up Powershell's quirks and find them all good for scripting tasks where you don't create too many pages of code.
Would I migrate with a large codebase? It depends on the industry of course, but if it is common line of business applications I'd be hard pressed to find something else. I was really hoping Kotlin could help here with it's REPL/Scratchpad and being on the JVM, but I didn't end up being too impressed (it might take more time).
I don't want to contribute to a static versus dynamic never ending argument. I guess I will say that Haskell, the JVM, and .NET just seem to have to much ceremony around them. I'm sure it's very powerful, but there is a lot to learn that distracts from just writing code.
Indeed it is "correct" in the sense that it has a very high likelihood (maybe 90% ?) of doing what the programmer intended (Unlike say C or C++ where the probability drops to about 50% for beginners)
However, that is a poor definition of "correct". While it's true that a lot of huge consequences have occurred due to stupid errors like buffer overflows (unintended bug), there are equally disastrous bugs caused by intent - i.e. the programmer had no idea the code could fail.
The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that