I'm not sure whether this is a joke?
Conversation
It’s definitely not advice! But maybe not a joke? Monads, or more generally delimited continuations, have the interesting property of being able to accumulate type information by virtue of each continuation being an overloaded function of the previous state to the next state.
2
3
But that’s true of any generic combinators you’d use to build up routes, whether or not it’s monadic. So yeah, it must be a joke :-p
1
As an aside, this is why I’m still a believer in “success typings”. You can’t model everything with types, so you shouldn’t be tempted to try. It’s kinda fun to watch you solve these puzzles though, because I suspect you will eventually rage quit contemporary type systems :)
2
4
I dunno, I had mixed feelings about using Dialyzer’s implementation of success typing. It was kind of annoying in practice to have it silently ignore ambiguously typed stuff. Not sire if that is more a problem with the tool ir success typing in general.
1
The success typing paper is pretty cool, but the idea doesn’t seem to really fit with a type-driven workflow (ie. for design and refactoring support).
1
Fair enough. My actual view is somewhat more nuanced. I don’t believe that erased types are workable either, which I bet is a big part of the problem in Erlang. I also want reflection, contract enforcement, and other runtime services.
1
2
Erasure should be possible, but so should reification, so you can get zero-cost when compiled, or usable at runtime for parsing and value generation. The language has to be codesigned with its type system (and VM too!)
2
1
Yeah. Support for both erasure _and_ runtime type dispatch is something of interest to me in relation to dependent types.
1
1
I will also clarify that I do think that using any type system for the forseeable future (perhaps forever?) requires one to accept that they are imperfect and require the programmer to make certain sacrifices to satisfy the tool.
1
And I understand that there are smart people who aren't willing to make that trade-off, and don't hold that against them. Type system designers/implementers will always be behind the curve of what developers want to do.
My hope is that in pursuing better UX around dependent types we can at least make type systems more extensible and customisable for library and application developers. But it DTs don't solve all the problems, and create other problems as well.