[HN Gopher] A mundane use of dependent types
___________________________________________________________________
A mundane use of dependent types
Author : Smaug123
Score : 93 points
Date : 2021-02-28 14:46 UTC (1 days ago)
(HTM) web link (twitter.com)
(TXT) w3m dump (twitter.com)
| Spivak wrote:
| 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.
| guerrilla wrote:
| I can't wait until they're ubiquitous. I think I read somewhere
| Rust was considering them. That'd be great.
| alpaca128 wrote:
| Rust does support dependent types via traits, just not as
| explicit feature and also not in the most intuitive way.
| comex wrote:
| 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.
| alpaca128 wrote:
| 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.
| creata wrote:
| Can you link to one of these talks? I'm absolutely
| certain that Rust does not have dependent types.
| [deleted]
| johnsoft wrote:
| I would love to see OP's code ported to Rust.
| nerdponx wrote:
| What are the downsides? Longer compile times? Soundness and/or
| completeness problems?
| ufo wrote:
| 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.
| comex wrote:
| This 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
|
| 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 wrote:
| Conversely (I think), if you have dependent types you don't
| require constexpr.
| butt_hugger wrote:
| We have links to tweets on the front page?
| Smaug123 wrote:
| Yes? 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&que...
| Three days ago we had
| https://news.ycombinator.com/item?id=26280808 which is _very_
| highly upvoted.
| alecco wrote:
| 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.
| johnfn wrote:
| 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.
| johnfn wrote:
| I 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.
| rowanG077 wrote:
| How 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.
| pierrebai wrote:
| 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.
| sourceless wrote:
| > 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 wrote:
| > 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?
| marcosdumay wrote:
| > 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.
| laserharvest wrote:
| > [Having and using dependent types] let[s] you be lazy about
| design.
|
| Now I've heard it all.
| Smaug123 wrote:
| 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_
| rsstack wrote:
| The 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 wrote:
| Speaking of "rest of", this is the file in question:
|
| https://github.com/idris-
| lang/Idris2/blob/master/src/Idris/E...
| elihu wrote:
| 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.
| tempodox wrote:
| Twitter is a terrible format for stuff like this. I wish HN had
| a filter that automatically kills all tweet submissions.
| mixedCase wrote:
| Strange, 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 wrote:
| 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.
| mixedCase wrote:
| Sounds 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 wrote:
| moreover, my company blocks social networks, so I can't
| access any of these threads unless I unroll them
| tomp wrote:
| I really hate compiler errors that could be warnings.
|
| Or at least have two modes, "prototyping" vs "production".
| miloignis wrote:
| This was addressed in the thread:
| 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.
| laserharvest wrote:
| https://twitter.com/edwinbrady/status/1366325538898538499
| remexre wrote:
| 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).
| bendiksolheim wrote:
| 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.
| hyperpape wrote:
| For 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 wrote:
| Unit 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.
| eek04_ wrote:
| 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.
| ArchieMaclean wrote:
| 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! :)
| chongli wrote:
| _it 's all "satisfy the compiler"_
|
| 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.
| Spivak wrote:
| 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.
| chriswarbo wrote:
| 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.
| hansvm wrote:
| 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.
___________________________________________________________________
(page generated 2021-03-01 23:02 UTC)