Threads for igstan

1. 17

   friendlysock 4 years ago | link | on: SQlite's Code Of Conduct

   In the famous words of Henry IV:

   A public-domain, small, time-worn, and battle-tested on-disk relational database is well worth a mass.

   1. 25

      zpojqwfejwfhiunz 4 years ago | link

      Now is the winter of our disk-contents

      1. 2

         igstan 4 years ago | link

         I had a good laugh. Thank you, both!

1. 2

   igstan 8 years ago | link | on: "Mostly functional" programming does not work

   I enjoyed the article. It actually convinced me to be a “fundamentalist” in my current job language, but… writing a really persuading article combating the “ambient monad” struck me as odd given that I have recently witnessed a tweet of the author where he claims:

   I’m happy to leverage the ambient monad

   I think I’ll just assume that he’s performing pro-level trolling on Twitter knowing his playful attitude from the Channel 9 videos.

   1. 3

      mavnn 8 years ago | link

      Given his work on Rx in various (definitely) non-functional languages, there’s a definite smell of epic trolling. On the other hand, I think he ends with a serious point - it would be nice in non-functional languages to be able to mark code as “pure”. .NET started doing this with the “Pure” attribute in code contracts, but it never quite made it to being usable in my mind.

      1. 1

         tel 8 years ago | link

         Why is it trolling to build better tools for real languages while simultaneously wishing for more?

         1. 2

            mavnn 8 years ago | link

            It’s not, and in case I’ve given the wrong impression I have a great deal of respect for Meijer and his work.

            What is trolling though, is to write a detailed rebuttal of why the strategy you’re currently prompting doesn’t work, tweaking the nose of people of the other side of an on going argument by pointing out their solution isn’t very good either and then sneaking in an actual practical suggestion at the end. In fact, I’d go as far as to say it’s a masterpiece of trolling that is far more thought provoking and engaging due to it’s ‘trollish’ nature.

            Trolling how it should be done, not as puerile sexist/racist/plain stupid stuff you normally see.

            1. 1

               tel 8 years ago | link

               Ahh.. I often forget that trolling has a non-idiotic side as well. I understand your point much better now and agree.

1. 4

   igstan 8 years ago | link | on: Idris: Type safe printf

   I would have loved to see an example at the end where the format string comes from user input. I’ll try to find the answer myself as I’m quite baffled right now as how would Idris be able to calculate a type from a string that isn’t known at compile time…

   Except for that, nice video! Thanks for creating it.

   1. 2

      jm 8 years ago | link

      The thing I found unsatisfactory was when there were no arguments, that was not a compile error. But extremely cool.

      1. 5

         bogdan 8 years ago | link

         I haven’t used Idris at all so this is just an assumption on my part. But I think the reason why it didn’t error on the case where there were no arguments is because of currying. printf "%d" by itself just returns a function that takes an Int and returns a String so you can do things like:

         intPrinter :: Int -> String
         intPrinter = printf "%d"
         

         In a complete program, the compiler would complain if you tried to use the intPrinter function as a String value (thus forcing you to provide an argument). Again, this is just an assumption on my part; maybe Brian can correct me if I’m wrong.
      2. 2

         puffnfresh 8 years ago | link

         It would be an error to do the following:

         h : String
         h = printf "Hello ℅s"
         

         But the Idris REPL has no problems printing functions, unlike the Haskell REPL.
   2. 1

      jfredett 8 years ago | link

      I read your question initially and thought, “Clearly that’s simple to solve, you just calculate the function on the fly as you do and then pass it the relevant arguments an–” then I realized you can’t know how many arguments to take without added work. I don’t know Idris, but I suspect the problem can be written:

      main = do
        formatStr <- getStr
        printf formatStr "some" "args" "here" 1 2 3
      

      The question being, ‘What happens when the format string has some number of placeholders not equal to 6’. Certainly we could count and verify the number of needed placeholders, but I suspect this code would either compile just fine and crash on bad input, or hollar that it couldn’t figure out the type of (printf formatStr) and fail to compile (hopefully the latter).

      I suspect to get it to compile you would need to annotate the type as you do in haskell, and then you’d probably need to add a run-time check to make sure things failed nicely.

      1. 2

         puffnfresh 8 years ago | link

         Idris won’t compile the above - proving that the input string has the correct interpolation holes would be pretty tricky, especially in the way this printf is formulated.

         If you want the printf value to be determined at runtime, I’d probably just go the Haskell way but add a validation type. Not a lot of value in proving correct arguments to a value when you don’t know anything about the possible value (conversely, you gain value from having more constraints on the possible input value).