4 ms·

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

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 6y ago
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 6y ago
  Speaking 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 ago
I really hate compiler errors that could be warnings. Or at least have two modes, "prototyping" vs "production".
- laserharvest 6y ago
  https://twitter.com/edwinbrady/status/1366325538898538499 https://twitter.com/edwinbrady/status/1366325538898538499
- remexre 6y ago
  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 6y ago
  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 6y ago
    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 6y ago
      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.
      - Spivak 6y ago
        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.
      - eek04_ 6y ago
        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.
- miloignis 6y ago
  This 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 ago
Twitter is a terrible format for stuff like this. I wish HN had a filter that automatically kills all tweet submissions.
- mixedCase 6y ago
  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 6y ago
    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 6y ago
      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 6y ago
  moreover, my company blocks social networks, so I can't access any of these threads unless I unroll them
elihu 6y ago
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.
- tomjakubowski 6y ago
  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.

rsstack 6y ago

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 6y ago
Speaking 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 ago

I really hate compiler errors that could be warnings. Or at least have two modes, "prototyping" vs "production".

laserharvest 6y ago
https://twitter.com/edwinbrady/status/1366325538898538499 https://twitter.com/edwinbrady/status/1366325538898538499
remexre 6y ago
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 6y ago
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 6y ago
  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 6y ago
    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.
    - Spivak 6y ago
      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.
    - eek04_ 6y ago
      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.
miloignis 6y ago
This 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 ago

Twitter is a terrible format for stuff like this. I wish HN had a filter that automatically kills all tweet submissions.

mixedCase 6y ago
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 6y ago
  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 6y ago
    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 6y ago
moreover, my company blocks social networks, so I can't access any of these threads unless I unroll them

elihu 6y ago

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.

tomjakubowski 6y ago
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.