It probably could do with some examples, and better docs, but it seems like they use this to update old chunks, which is a great use of lenses.
But yeah, you'd have to weigh that up against how ugly it turns out to be in Java. It's not just because of the verbosity, it's the lack of being able to abstract over type-level functions that makes it quite icky to implement these abstractions in Java.
Yup, lots of people are under the impression that you need to prove everything when it comes to DTs. That's not true - you can indeed push these checks to runtime, and just have the compiler make ensure you do it.
Don't get me wrong - CT is a super handy thing to learn, and it pops up a ton when thinking about any software, including type checkers and compilers, but the OP was specifically asking about type theory and programming language implementation. Yes, you can express lots of category theory in terms of type theory (the dream is to implement all of it in terms of TT so that we can mechanise it), but it won't be the best use of your time if you want to build a type system.
I believe it's more just how to use a dependently typed language (my copy is still in the mail). Like the Little Schemer, it's written in the Socratic style. I think the idea is that you can do it all in your head if you want, with a piece of paper covering up the column with the answers.
Note that many of those problems are being actively worked on in research, and progress is being made, albeit slowly. That said, we can still get some of the benefits of dependent types, even without all the problems being solved right now! Just gotta be aware that it's not all roses yet.
Typescript actually does have some forms of type dependency (eg. conditional types), but these things have been added in a sort of ad-hoc way, and it's unclear how sound they actually are, and they are quite limited. The book here uses a language, pie, that is designed in a much more principled way, with greater expressiveness. The book probably won't be directly applicable to TS work, but I'm sure you would benefit from getting a more rounded understanding of what is possible with type systems.
I hear that Practical Foundations of Programming Languages by Robert Harper[0] is highly recommended. I have Types and Programming Languages, but found it a little dry to be honest. I do use it as a reference manual in my work though.
They've been historically hard to implement in a way that is both efficient, sound, integrates with effectful code, promotes code reuse (like in Haskell), and has good developer UX (good error messages and IDE support). I believe we are getting to a point where it is feasible, hence I'm messing around with it myself [0], but it can be challenging to navigate the terrain of papers and theory as a language designer. While DTs themselves are quite simple, the integration with other features users expect is tricky, and producing a production-grade compiler is definitly not as straightforward as making a regular Hindley-Milner style language.
Yeah, I agree. And when Rust removed poorly designed things, they were often replaced with alternatives that solved the problem better, so it was never felt like a pain.
Yeah! I also liked how escape hatches weren't looked down upon as much. They're kind of important if you want to be developing production software! It's cool to remove stuff if things are poorly designed (which Elm's native code API was), but it'd be great if something better was put in its place! Reason seems to be handling this in a decent way - Purescript as well. So there are other options at least.
The difference in Rust's case is that whenever anything was removed it was replaced with something that was better designed. It provided escape hatches available to allow for workarounds (ie. unsafe, and a nice FFI), and to allow C libraries to bridge the gap while the ecosystem was still developing.
Most other English-speaking people in the world deal with different accents reasonably often in media and their lives, the American accent most of all. I think it's more that it's easy for American's to live in a bubble, because the country is so large - it's sometimes odd to see American media putting subtitles on strongly accented but otherwise perfectly intelligible english speakers, for instance.
There is work being done to bring an algebraic effects system to OCaml, but it's slow going. I think because the people pushing it have a bunch of other things on their plates too. But it would be super nice to have!
> No, I mean that neither Elm nor Standard ML has nor needs typeclasses. No language needs typeclasses.
Standard ML has less need for type classes because it has a much more expressive module system, but it still can be extremely tedious to pass around module definitions all the time, which is why they added equality types when the language was originally designed. This is considered an ugly hack though, even by its own creators [0].
Definitely agree that folks should aim for better than type classes, especially due to complications around global instance coherence. One nice solution is modular implicits/instance arguments [1][2]. Tricky thing is to do it without adding too much complexity to the language.
I do wish that there would just be some acknowledgment that it's a hard, but real problem to solve for Elm's point in the design space, rather than just pretending it isn't there. It's ok just to say that you're not spending design capital on it at the moment due to more pressing issues!
Yeah, IIRC many years ago I added it in a document as a pattern for C APIs (I can't remember where though). Either other people were doing the same thing, or were influenced by that. Anyway, you should use `*const libc::void` these days! Sorry for the confusion.
Oh lovely, will have to give this a read at some stage!
I'd also be really interested in versioning, and upgrading a cluster over time, without bringing the whole thing down (like with Cloud Haskell). Would be super handy to be able to verify that your migration works first, before actually going ahead with it. I'd also love it if the types could be used in some way to make this kind of thing easier to reason about.
Are you also aware of the work advancing in Akka Typed? After a number of iterations they made some modifications that made things simpler - not sure how it compares with your work though: https://doc.akka.io/docs/akka/2.5/typed/actors.html#relation...
Dialyzer works on success typing, which only tells you when it's certain there's a bug, but will stay silent if it's unsure. Even at the highest settings I couldn't get the same lovely iteration loop that you get in an ML-style language (like Haskell, Elm, Rust, etc) that I've come to expect, where you feel like you are having a conversation with the tool.
At the time I was attempting to use it, it was also super slow, and libraries were not keeping their typespecs up-to-date. Also a big one: no parametric polymorphism results in `any`s galore. :/
Most systems aren't really at the scale where the BEAM really excels. I'd still contend that they would be far better off with a good type system to make it easy to refactor and iterate as requirements change.
Apparently Typed Akka is finally starting to arrive at a good design, after a number of iterations over the years, but seems like there is still lots of interesting research to be done in distributed type systems.
> In Elixir, you notice the dynamic typing mostly when you're defining callbacks that take MFA-style function specs, e.g. def handle_click(m, f, a)
I really noticed it in the `Enum` module - so many `any`s, on simple things like `map`. Kind of ridiculous. And protocols are not type directed, so you don't get the huge win of return type polymorphism. Kind of kills lots of useful patterns :/
Algebraic effect systems can also do this. See Koka, Eff, Multicore OCaml, Frank, Purescript-run, freer-effects, freer-simple etc. These generally allow you to handle effects in different ways. Not sure if F#'s type system is powerful enough to build this as a library though.
As Haskell begins to get more and more dependently typed features this could definitely be an exciting possibility (I think there are folks already working on this).
Lots of folks seem to be getting drawn to actix-web, which features quite a bit up the top of these benchmarks. I've not used it, but it works on stable, is fully async, and has been met with many good reviews!
I kind of found Dialyzer disappointing from starting a project from scratch. It would miss many obvious mistakes that I expected would be caught. Very much was not a fan of this key design decision of success typing! That said, the theoretical research behind it I can respect.
Ah, thanks for the extra info. I'm too young to have dealt with this stuff myself, so first-hand experience is always really interesting! What I have had to deal with is schemaless JSON HTTP APIs - definitely know what a pain that is! GraphQL is a whole bunch nicer from what I hear (but will be interesting to see what folks say in several years time).