A mundane use of dependent types
twitter.com
twitter.com
> A mundane use of dependent types... I just tried to add an environment variable to Idris 2, and it wouldn't compile because I forgot to add it to the --help output.
> offers compiler a jelly baby
>That probably sounds like it'd be annoying, but it took about 20 seconds to fix, and it's not as annoying as forgetting the feature is there.
>We always give talks that show off the fancy stuff. Maybe one day I should collect together all these everyday little things and talk about them instead.
>I would need some new jokes to keep it interesting, I suppose.
https://github.com/idris-lang/Idris2/blob/master/src/Idris/E...
Or at least have two modes, "prototyping" vs "production".
I used to program with annotated type languages (Pascal, C++, Java) for a couple of decades. I spent a decade plus with dynamically checked languages, and whenever I try to go back (to Java or C++) or go to something harder (e.g. Haskell) the type checking is very much in the way of initial development. Maybe dependent types are sufficiently expressive that this problem isn't there. However, every time the promise has been made in the past, it's turned out (IMO) that the person advocating is used to working around the weaknesses of strongly typed languages and neither is used to exploiting the strengths of dynamically checked languages nor is used to working around the weaknesses of dynamically checked languages.
They're really useful for rapid prototyping, and also for helping you develop, as you can ask the compiler questions about the hole (like what its type is).
The syntax is just `?name` creating a hole called 'name'.
So you don't have to write the whole program, and you don't need to lie temporarily either! :)
That’s not at all like the experience programming with Idris. Idris is more like working with a powerful assistant that can infer all kinds of stuff about the shape of your function. In some cases, it can even infer the entire function implementation from the type. In cases where it can’t infer that it can give you a bunch of information about what terms are in scope with the appropriate types.
More objectively, a dependent type system (like Idris, Coq, Agda etc.) is a test framework, since it can run arbitrary code.
Instead of writing tests as booleans, with 'true' for pass and 'false' for fail, we write them as types, with the unit type for pass ('()' in Idris) and the empty type for fail ('Void' in Idris), e.g. see this thread https://news.ycombinator.com/item?id=24567404
Of course, we can do the usual monad/effect-system tricks to implement a 'throw TestFailException' API on top of that, if we prefer.
That leaves the caller of my library in control of how they want to handle such cases:
(1) If they silence warnings then everything will probably still work.
(2) If they convert warnings to errors then they can immediately inspect that warning and see how it applies to their use case. They might still just silence the warning, or they might add in some kind of override or shim so that my code works on their system.
> Replying to > @edwinbrady > Is it possible to delay adding it but have it compile with a warning, so you can test it out, but still be fairly confident that it won't actually get to prod?
> Replying to > @Anka213 > You can always add holes, which compile but give a compile time warning and run time error.
I got the point quickly and could expand replies easily when interested.
I open it and at least on desktop I get the author's full thread (3 tweets) which was him just sharing a thought with his followers, and then each tweet has optional context with people and the author making further comments. Then you just dig in or you drop out.
Let me know if I'm wrong, but I think you just expected a full article out of someone who was just simply briefly sharing an experience where a tool that's still fairly unknown in the industry proves its usefulness for everyday usecases. IMO that's valuable on its own.
Sometimes I wish I lived in the alternate universe where every executable binary on my computer had a machine-readable interface description that included every command line argument, every environment variable, every file it needs access to (if not provided as a command line argument), and all file I/O was strongly typed.
Example use case of the latter is that if I have a postscript file and want to convert it to a pdf but don't know the name of the program that does it, I could run a solver that figures out that in a pipeline like this: "cat foo.ps | $converter > foo.pdf", ps2pdf could be substituted for $converter and result in a well-typed command line. This could be integrated into tab completion.
Another problem is that sometimes there are "obvious" things that you'd like to write where the program itself is small but the proof of correctness isn't as easy. But I'd imagine that in a world of ubiquitous dependent types the software engineering might adapt to that. Either by encouraging you to write things that are easy to prove, or by developing best practices of when it's acceptable to skip a proof.
https://gcc.godbolt.org/z/c9KqYb
Unfortunately, this version requires a custom StringLiteral class and some other awkwardness because constexpr is still very limited. (I tried Rust const generics too but they're even worse.) This should improve in the future.
Sure it's nice that the language itself has a built-in way to verify a complex invariant and not having to write a unit test.
But what it does illustrate is something I've meant to write a bout for a while: having this kind of convenience let you be lazy about design.
In some (C++) projects I've worked on, adding a new configuration item would automatically documents it because the class to create a configuration item requires you to provide a doc string argument. So it could be even less forgotten.
Or, conversely, this kind of correctness by construction allows you to focus on parts of the program that could suffer from non-trivial bugs
How does having this in the language permit laziness in design? You still have to think about the properties in order to describe them, whether it's going into a type system or a test suite.
Does the laziness occur once the property is placed into the type system because you can now rely on the compiler to assist you? Wouldn't the same argument apply to having a test suite that detected similar failures to maintain these properties?
Hum... No. It's not a test.
A test is some code that tries to detect the presence of errors with specific execution data and environment. This is verification, that is code that tries to detect the absence of errors over any possible execution data and environment.
The distinction is extremely relevant, mostly because a little bit of validation can replace entire screens of tests, and because tests tend to become stale, while validations tend to be generic enough to survive refactoring and even changes in requirements.
But well, I entirely agree with this:
> But what it does illustrate is something I've meant to write a bout for a while: having this kind of convenience let you be lazy about design.
It's very nice to hack some minimum proof of concept of the most relevant problems, and be able to refactor it into some high quality code just by setting the checks for quality and blindly following their results. I imagine that's also what the "TDD for everything" people like so much about their processes.
Like, yeah, enforcing that env variables are accessed in a structured way is kind of a solved problem. I don't think dependent typing adds that much.