Threads for j2kun

  1. 2

    Not langdev. Think I’m rather burned out. I heckin’ hate type checking so much. Anyone want to write a pragmatic and functional type checker for me, including generics, and let me get on with life to the actually interesting part of the project?

    Maybe I’ll play with my OS project instead. It’ll never be useful and involves exactly zero theoretical math, which sounds exactly like what I need.

    1. 1

      Naive question: why is writing a type checking algorithm so difficult?

      1. 2

        It’s not. In theory. But nobody tells you how to do it. The only tutorials, examples, books etc come in one of three forms:

        • Too concrete (no generics, no subtyping, basically just integers and bools and maybe strings)
        • Too abstract (“here is how you implement simply typed lambda calculus, ok up to you to go from here”)
        • Demonic math

        I’m really sick of trying to deal with any/all of them, synthesize them into something small but sane and functional, and generally banging my head against a wall over and over.

        1. 1

          As a casual consumer of adjacent literature this rings true to me. Especially the demonic math. I feel somehow deficient that I can’t decipher the mad scribblings that I see in a lambda cube article. I get the impression that this would be very clear and really just self evident if I had the proper education, except I don’t know what that education is, where to get it (without paying 5 or 6 figures) or how long it would take to get. What’s more, some arrogant part of me feels like I should be able to create some amazing programming language because really I’m so smart (you know except the whole not knowing how thing).

          Your language also has a linear component too, right? I imagine that only compounds the wonderfully under specified nature of the whole ordeal.

          1. 2

            You might be interested in my book, A Programmer’s Introduction to Mathematics (pimbook.org, ebook is free), which doesn’t focus specifically on type checking systems, but does cover math, notation, and proofs more generally. That said, I do sense that languages folks (type systems, functional programming, etc.) go a bit haywire on the notation as compared to a typical mathematician.

            1. 2

              …except I don’t know what that education is, where to get it (without paying 5 or 6 figures) or how long it would take to get…

              It’s doable. You just start reading and talking to people about it. There are plenty of people on the r/ProgrammingLanguages discord server that will happily tell you way more than you ever wanted to know about any of it, and a couple guides that are widely cited such as http://siek.blogspot.com/2012/07/crash-course-on-notation-in-programming.html and https://blog.acolyer.org/2018/01/26/a-practitioners-guide-to-reading-programming-languages-papers/. As for “how long it would take to get”, well, same as learning to program itself I expect. You can get functionally familiar with it in a few months, and getting good enough to really understand all the nuances will take a lifetime. But unless you’re doing fancy research you probably don’t need all the nuances, just the ability to follow others’ nuances.

              Of course, I haven’t done this. As you said, “some arrogant part of me feels like I should be able to create…” I keep thinking I know enough already and trying to take short cuts.

              Your language also has a linear component too, right?

              If you’re referring to my effect-system-ish ideas, I’m not even that far yet, and I don’t want it to be that complicated. All I really want out of it is to be able to annotate functions with useful constraints (“does not panic”, “does not allocate”, etc) and have the compiler able to check/enforce them for me. That seems like it should be pretty straightforward, since I don’t really intend much composition or metaprogramming or such. Then either that will be good enough for what I want, or I will need to learn more and elaborate it. Either way, not my main concern right now.

      1. 1

        This is the kind of religious attention to rigor that undergraduates benefit from, but that researchers couldn’t care less about. It’s the analogous “well actually” guy for mathematics. Part of graduate school training is to teach you to distinguish between important and unimportant issues, and I think the empty graph is a clearly unimportant issue. And even the authors admit this at the end, so I can only infer the article is something of a joke.

        1. 1

          Sometimes rigor can unveil a important point hidden in a seemingly unimportant stuff. It’s just a LOT less likely to do so. If you have the free time though might as well peek.