7 ms·

Idris points the way to the future of programming. A few examples that I find very intriguing: 1. type safe printf: https://github.com/mukeshtiwari/Idris/blob

• lodi 9y ago
  If anyone is having trouble understanding the raw code linked above, the official book[1] introduces all three of those concepts gently and intuitively. I highly recommend it! [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...
  • Buttons840 9y ago
    The book is written by the creator of the Idris language. I highly recommend it to those interested in type level programming as well.
• jlturner 9y ago
  Most functional languages have a type safe printf / sprintf (i.e. OCaml, F#, Haskell) which is similar to the effect you get in Idris: the types required to apply the function are statically analyzed from the format string. Edit (links): OCaml: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.html https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.ht... F#: https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual/core.printf-module-%5Bfsharp%5D https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual... Haskell: https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-Printf.html https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-P...
  • lkitching 9y ago
    The Haskell version of printf does not statically analyse the format string and will raise an exception if the provided arguments are invalid e.g. Prelude Text.Printf> printf "%d\n" "invalid" *** Exception: printf: bad formatting char 'd' The behaviour of F#'s printfn is hard-coded in the compiler and could not be written in F# iteself.
  • dllthomas 9y ago
    > the types required to apply the function are statically analyzed from the format string. Not so, in that Haskell package: Prelude Text.Printf> printf "%d\n" 1 1 Prelude Text.Printf> printf "%d\n" *** Exception: printf: argument list ended prematurely Prelude Text.Printf> printf "%d\n" 0.5 *** Exception: printf: bad formatting char 'd' Prelude Text.Printf> printf "%d\n" 1 2 1 *** Exception: printf: formatting string ended prematurely It could certainly be done with TH/QQ. I'm not sure, offhand, if there is already a package to that effect.
    • hesselink 9y ago
      There are several packages on hackage offering a type safe printf. Some use TH, some use variadic functions (defined with a type class) or other advanced type level features.
      • dllthomas 9y ago
        Variadic functions are used in the package under discussion, and don't get you compile time checking of the format string.
  • cannam 9y ago
    Aren't the Ocaml and F# examples relying on some dedicated compiler support for the format string type, though? The Idris example is interesting because its printf implementation can actually be written in Idris.
    • lower 9y ago
• danidiaz 9y ago
  A haskell version of 1) is talked about here: https://www.reddit.com/r/haskell/comments/55bvt4/typesafe_printf_with_typeintype/ https://www.reddit.com/r/haskell/comments/55bvt4/typesafe_pr... It uses the "singletons" library (no relation to the singleton design pattern) that emulates some features of dependent types.
• hellbanner 9y ago
  Does anyone remember the language that wanted to be future of programming, making everything (API calls, lists on screen etc) inherit from 1 base class, and it used SQL-like searching for filtering on collections? It had a browser based demo.
  • m-j-fox 9y ago
    No but tell me if you remember.
    • wesp321 9y ago
      Fortress?
      • m-j-fox 9y ago
        Depressing thing to Google. Seems like an interesting project that couldn't keep it's funding in volatile times. It might have been Swift or F# if developed at a better company.
        • zem 9y ago
          they did the best job of operator associativity and precedence i've ever seen. still hoping some other languages pick up on it. http://lambda-the-ultimate.org/node/2943#comment-43411 http://lambda-the-ultimate.org/node/2943#comment-43411
          • m-j-fox 9y ago
            Whitespace-implied parenthesis. 1+2 * 3 == 9 Sick! I wish Haskell notices this.
    • hellbanner 9y ago
      It's Eve
  • mmalone 9y ago
• platz 9y ago
  and then you need to log in a VIP user or a debug user without auth but cant produce a proof so now it wont compile at all. not a problem i you own the code but in client/server a third party could be the client or server so will have to be very careful about placing proof obligations on code you dont own.
• hota_mazi 9y ago
  Type safe printf has been around for more than a decade, going all the way back to at least Groovy.
  • m-j-fox 9y ago
    I know clang will not let you make a mistake, but it must be some kluge since the C language clearly doesn't anticipate that.
  • dllthomas 9y ago
    I used it in OCaml well before there was a Groovy. But what's interesting here is that you get it without compiler special casing and without macros, as a natural consequence of how the type system works - in a way that generalizes to other problems.
    • colorint 9y ago
      >without macros Type systems are macro systems, it's just not obvious because type languages are very different from expression languages. The main "innovation" of Idris is hammering harder on this front. And in any case, the fact that most type languages are logic languages gives people with a formalist bent a warm feeling in their stomachs.
      • dllthomas 9y ago
        There's a valid perspective from which type systems are particularly-constrained macro systems. That doesn't mean there aren't contexts where it's useful and/or interesting to distinguish. But if you wish, pretend I had written "traditionally conceived general purpose macros" :)
  • mej10 9y ago
    It is weird to me that so many people are getting caught up on the fact that type safe printf has been around forever. If someone has looked into Idris they almost certainly know that it isn't a new concept. I linked it because its implementation is amazing comparatively and it is just one clean example of what is possible.
• didibus 9y ago
  I'm sure there's a branch of programming where that would be amazing, but in my experience, I've never had major bugs due to my client and server implementing their protocol wrong. In fact, I question most of the value of formal verifications for non critical software. Most of the problematic bugs that make it through in my experience are either a complex combination of multuple parts of the system interacting together in a way that doesn't end up behaving the way it was intended, or programmers implementing the wrong thing on edge cases.
  • haskellandchill 9y ago
    I have 8 years of industry experience and feel the exact opposite. When programming in Ruby I am forced to not fully express the concepts in my head. We do TDD but our tests are humorously thin; typically covering none, one, many. Idris proofs are tricky but more automated and powerful than writing tests. And I can still write tests in Idris. To go beyond "protocols", UI form data to server response back to UI display in a web app is a source of major bugs. So many things are broken. Recently I had to add a spurious lap infant to book a flight due to JavaScript template being broken when rendering 0 children.
    • codygman 9y ago
      spurious lap infant?
      • haskellandchill 9y ago
        True story: https://i.redd.it/lc84fv1lrv2z.png https://i.redd.it/lc84fv1lrv2z.png
    • vijucat 9y ago
      What happens if you try to book 9007199254740993 spurious lap infants? Just curious. I'd love to QuickCheck the diapers out of this method.
  • Karrot_Kream 9y ago
    I've encountered so many bugs because of mismatches between server and client APIs, it's not even funny. Even then it remains a persistent problem, as evidence with changing Thrift schemas forward.
• lobster_johnson 9y ago
  Re typesafe printf, I assume the compiler can produce efficient code, since the pattern matching occurs at compile time? Also, if you have an arbitrary string that isn't a constant that can be analyzed statically — for example, a string read from a config file — how do you prove to the compiler that it's a valid format-code string?
  • jfoutz 9y ago
    the compiler knows the failure modes. if the file doesn't exist, the printf isn't reachable. if the file isn't at least X bytes long, the printf isnt' reachable if bytes 10-20 can't be parsed as a number the printf isn't reachable. it's just showing if you get through these 50 checks, by the time you get to printf the bytes will have been converted to what you need, or the program will have already errored out.
  • eutectic 9y ago
    Any string is a valid format string.
    • lobster_johnson 9y ago
      I mean the combination of format string + values. Anyway, is that really true? "%-1s" should probably give you an error, for example.
• jw- 9y ago
  > Think about being able to specify protocols in the type system and ensuring that your client and server meet the specifications. The example in that link is about user authentication. Imagine having a proof that the program can only get into a "LoggedIn" state by going through the authentication protocol. Sounds like you are describing Session Types! (http://groups.inf.ed.ac.uk/abcd/ http://groups.inf.ed.ac.uk/abcd/) (http://summerschool2016.behavioural-types.eu/programme/DardhaIntroBST.pdf http://summerschool2016.behavioural-types.eu/programme/Dardh...)