Full text of Edwin Brady's tweet:
> 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
> 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...
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.
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.
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.