> 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.
>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.
Well, the point isn't to have errors for a lack of documentation, the point is that dependent types offer a lot of expressiveness in modelling what it means for programs to be valid in your domain, both so the compiler can tell the programmer about subtleties they may have missed, and the programmer knows what details of the implementation are intentional features (e.g. every case this function handles has a corresponding entry in a table of documentation).
I really dislike the concept of compiler warnings. It's either an error, in which case it needs to be handled right away, or it's completely fine. Warnings are overlooked in the long run.
You don’t deserve the downvotes. You need far far fewer unit tests when you have a good type system backing simply because the compiler allows you to meaningfully constrain your inputs.
I really want to love types. But type errors so so get in the way of getting to something testable - it's all "satisfy the compiler" which either requires writing out close to my whole program or writing a lot of temporary lies.
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.
Idris has 'holes', where you tell the compiler that you haven't written this part yet, and it will compile while ignoring the hole.
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.
Sibling comments are talking about "good types need fewer tests, yada yada" which is somewhat subjective (although I happen to agree with it).
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.
I'll use a warning if it might be an error but I don't have enough information to be certain (most commonly when I'm trying to infer essential information about a compilation target and have a reasonable but fallible fallback for esoteric targets).
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.
How many people will notice that there is important info hiding under replies? Twitter's UI excels at hiding that information, and at presenting it in a weird order.
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.
This isn't really a comment about dependent types, but one of the things I hate about environment variables is that you can't query a binary to ask what environment variables it supports.
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.
Around 95% of the getenv() calls I have seen in my life use a string constant. So there's some hope for a static analysis tool for that much, at least when it comes to native/compiled binaries.
IDEs could improve significantly with Dependent Types. They could make you input at once in all the affected places. And it could be even automated for simple things.
I’m so happy that mainstream tooling is getting dependent type support. They’re just so damn expressive. Nothing feels like the safety of eliminating lots of runtime checks and error handling because the compiler makes it impossible to do the wrong thing.
No, it does not. It has some support for types which depend on constant values (i.e. values known at compile time), but not types that depend on runtime values, which is the real power of dependent types.
There are literally talks on YouTube about using dependent types in Rust. In fact that is how I stumbled over the topic in the first place. So yes, it does. Just not in a convenient way, as I already mentioned.
In my experience the key challenge is the steep learning curve. You need to understand advanced type theory to really understand what the error messages mean.
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.
But this was not magical: the code has to have a specific check coded in that verify that one thing added here is also added there... AKA a unit test?
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.
> 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.
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?
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.
As someone who doesn't understand what dependent types are, this seems opaque to me (and is probably equally opaque to anyone else who doesn't understand). You can do this trivially with e.g. a structure-like type. E.g. in TypeScript it'd just be `type EnvironmentVariables = { otherFlags: stuff; newFlag: whatever; }` - and then you'd just have to use `EnvironmentVariables` in both the --help and in wherever you specify your environment variables.
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.
49 comments
[ 2.1 ms ] story [ 91.1 ms ] thread> 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.
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?
Now I’ve heard it all.
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.
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.