We did this to ourselves

Comments

• ezchili@iusearchlinux.fyi ⁨1⁩ ⁨year⁩ ago

  What

  source

  • tatterdemalion@programming.dev ⁨1⁩ ⁨year⁩ ago

    It’s making fun of dynamic languages because rather than letting the compiler prove theorems about statically typed code, they… don’t.

    source

    • DumbAceDragon@sh.itjust.works ⁨1⁩ ⁨year⁩ ago

      Dynamic languages were invented by runtime error companies to sell more runtime errors.

      source

      • -> View More Comments
    • deegeese@sopuli.xyz ⁨1⁩ ⁨year⁩ ago

      Turns out getting working code is a lot cheaper and more useful than formally proven code.

      source

      • -> View More Comments
    • ShroOmeric@lemmy.world ⁨1⁩ ⁨year⁩ ago

      What

      source
    • xmunk@sh.itjust.works ⁨1⁩ ⁨year⁩ ago

      I may just be an old country lawyer PHP developer… but don’t most dynamic languages also support static type checking and general analysis at this point?

      source

      • -> View More Comments
    • tzrlk@lemmy.world ⁨1⁩ ⁨year⁩ ago

      Though even statically-typed languages can need to check types sometimes; parsing runtime data for instance. I can see how you’d do that with pure statics, but it’d just be shifting the work (e.g. if token == QUOTE: proc.call(read_str(bytes, len))). It’d be cool to see a counter example that isn’t unreadable gibberish, however.

      source
• kronicmage@lemmy.ca ⁨1⁩ ⁨year⁩ ago

  This is referencing Philip Wadler’s 1989 paper “Theorems for Free”, which is fairly well known in the Haskell community: home.ttic.edu/~dreyer/course/papers/wadler.pdf

  source

  • spicyemu@programming.dev ⁨1⁩ ⁨year⁩ ago

    That looks like something I’ve seen somewhere and didn’t understand.

    source
• PotatoesFall@discuss.tchncs.de ⁨1⁩ ⁨year⁩ ago

  I need an explainer on this one

  source

  • steersman2484@sh.itjust.works ⁨1⁩ ⁨year⁩ ago

    if (theorems_for(free))
        make_instance_of(x, String)
    

    source

    • ezchili@iusearchlinux.fyi ⁨1⁩ ⁨year⁩ ago

      What

      source

      • -> View More Comments
• Kolanaki@yiffit.net ⁨1⁩ ⁨year⁩ ago

  🎵 Millions of theorems,

  Theorems for free.

  Millions of theorems,

  Theorems for me, look out! 🎵

  source
• jasondj@ttrpg.network ⁨1⁩ ⁨year⁩ ago

  I’m sorry, I’m only a novice Python guy. Know enough to get two RESTful APIs to talk to each other and do some network automation or rudimentary Ansible plugins.

  What’s wrong with if isinstance(x, str):?

  source

  • Knusper@feddit.de ⁨1⁩ ⁨year⁩ ago

    Apparently, “Theorems for free!” is a paper that talks about an extensive ability to reason about parts of programs, if you follow some rather basic rules.

    However, lots of popular programming languages throw this ability out the window, because they do not want to enforce those basic rules.
    Most languages, for example, allow for rather uncontrolled side effects and to be able to reason as a programmer, you have to make the assumption that no one else abused side effects.

    The instanceof is rather referring to dynamic typing, though, as e.g. employed by Python and JS, which makes it difficult to make any assumptions at all.

    So, in statically typed languages, when you’re implementing a function, you can declare that a given parameter is a number or a string etc. and the compiler will enforce that for you. In dynamically typed languages, you have to assume that anyone calling your function is using it correctly, which is a difficult assumption to make after a refactoring in a larger codebase.

    All in all, such different levels of rigorosity can be fine, but the larger your codebase grows, the more you do want such rules to be enforced, so you can just ignore the rest of the codebase.

    source
• apprehentice@lemmy.enchanted.social ⁨1⁩ ⁨year⁩ ago

  Okay, but what’s a theoren?

  source

  • Pok@lemmy.world ⁨1⁩ ⁨year⁩ ago

    It may or may not be a string.

    source
• kronicmage@lemmy.ca ⁨1⁩ ⁨year⁩ ago

  This is referencing Philip Wadler’s 1989 paper “Theorems for Free”, which is fairly well known in the Haskell community: home.ttic.edu/~dreyer/course/papers/wadler.pdf

  source
• mikidep@lemmy.world ⁨9⁩ ⁨months⁩ ago

  Op here back from the dead. This is in fact not a stab at dynamically typed languages, or at least not only: statically typed languages such as Java also support this kind of construct. In fact, one could develop a technically type safe programming language where an instanceof construct has sound semantics.

  What instanceof breaks is something called polymorphic parametricity, i.e. the fact that generic functions don’t know anything specific about the types they are generic over. This is the fundamental condition for what in the community is dubbed “theorems for free”, that is, naturality of generic functions between generic types.

  source