9 ms·
A mundane use of dependent types
- Smaug123 6y agoFull 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
- rsstack 6y agoThe rest of his thread: >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.
- ricree 6y agoSpeaking of "rest of", this is the file in question: https://github.com/idris-lang/Idris2/blob/master/src/Idris/Env.idr#L47 https://github.com/idris-lang/Idris2/blob/master/src/Idris/E...
- tomp 6y agoI really hate compiler errors that could be warnings. Or at least have two modes, "prototyping" vs "production".
- laserharvest 6y agohttps://twitter.com/edwinbrady/status/1366325538898538499 https://twitter.com/edwinbrady/status/1366325538898538499
- remexre 6y agoWell, 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).
- bendiksolheim 6y agoI 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.
- hyperpape 6y agoFor production that makes sense, but "I'd like to run my unit tests before I spend effort fixing this thing" is a valid use case.
- chongli 6y agoUnit testing is greatly de-emphasized when you have dependent types. So many of the things you'd catch with unit tests you can turn into type errors.
- Spivak 6y agoYou 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.
- eek04_ 6y agoI 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.
- miloignis 6y agoThis was addressed in the thread: https://twitter.com/Anka213/status/1366219698317053954 https://twitter.com/Anka213/status/1366219698317053954 > 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.
- tempodox 6y agoTwitter is a terrible format for stuff like this. I wish HN had a filter that automatically kills all tweet submissions.
- mixedCase 6y agoStrange, I see no problems here. Specially for something that was just a simple thought, not an essay. I got the point quickly and could expand replies easily when interested.
- ufo 6y agoHow 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.
- mixedCase 6y agoSounds perfectly reasonable to me as it is. 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.
- merdadicapra 6y agomoreover, my company blocks social networks, so I can't access any of these threads unless I unroll them
- elihu 6y agoThis 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.
- tomjakubowski 6y agoAround 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.
- alecco 6y agoIDEs 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.
- butt_hugger 6y agoWe have links to tweets on the front page?
- Smaug123 6y agoYes? Right now there are two such links on the front page. It's pretty common in general: https://hn.algolia.com/?dateRange=all&page=0&prefix=true&query=https%3A%2F%2Ftwitter.com&sort=byDate&type=story https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que... Three days ago we had https://news.ycombinator.com/item?id=26280808 https://news.ycombinator.com/item?id=26280808 which is very highly upvoted.
- Spivak 6y agoI’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.
- guerrilla 6y agoI can't wait until they're ubiquitous. I think I read somewhere Rust was considering them. That'd be great.
- alpaca128 6y agoRust does support dependent types via traits, just not as explicit feature and also not in the most intuitive way.
- comex 6y agoNo, 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.
- alpaca128 6y agoThere 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.
- deleted 6y ago[deleted]
- johnsoft 6y agoI would love to see OP's code ported to Rust.
- 6y ago
- pierrebai 6y agoBut 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.
- sourceless 6y ago> having this kind of convenience let you be lazy about design Or, conversely, this kind of correctness by construction allows you to focus on parts of the program that could suffer from non-trivial bugs
- Jtsummers 6y ago> 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?
- laserharvest 6y ago> [Having and using dependent types] let[s] you be lazy about design. Now I’ve heard it all.
- marcosdumay 6y ago> AKA a unit test 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.
- johnfn 6y agoAs 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.
- rowanG077 6y agoHow can you specify in typescripts a field must be used? I'm currently writing typescripts for a web app and this would come in hamdy for me.
- simlevesque 6y agoAny field present must be used. Optional fields end with ?
- rowanG077 6y agoI have never seen any typescript where any field present must be used. Can you make an example?
- johnfn 6y agoI got some downvotes on this post but it's a genuine question and I'm not trying to troll. Not sure what's going on here.
- comex 6y agoThis doesn't require full dependent types because the values being examined are constants. Here's a version in C++20: https://gcc.godbolt.org/z/c9KqYb 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.
- laserharvest 6y agoConversely (I think), if you have dependent types you don’t require constexpr.