9 ms·

I’ve come to believe that a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value. The only real implementatio

• valenterry 2y ago
  Sadly this is true and I 100% agree. After reading and working through type-level programmin in Idris, this is the conclusion I came to.
  • pmarreck 2y ago
    What made it seem too restrictive to you? Or what were your experiences trying to apply it to real-world scenarios?
    • valenterry 2y ago
      I'm not sure what you mean. I don't find Idris restrictive (except for the lack of union types with subtyping). Rather I find any mainstream language very restrictive - or is that what you meant?
      • pmarreck 2y ago
        ah, I think I misunderstood. Still getting through the Idris book :)
• pydry 2y ago
  I think there's a sharp rule of diminishing returns the stronger you make type systems. Type safety comes at a cost and that cost has to come with an associated payoff. This is why ultra strong type systems end up being little more than academic toys - the payoff when you dial type safety up to an extreme doesn't match the associated cost. Types and tests should meet somewhere in the middle because the same law of diminishing returns affects tests in reverse. They tend to be good at what the other is bad at and if you rely too heavily on one at the expense of the other they will start fraying around the edges.
  • Quekid5 2y ago
    In Idris you get to choose how strict you want to make your types. E.g. you can choose to use "Vect n a" if you want a vector a's where the size is tracked by the type system. Or you can use e.g. "List a" if you want a list of a's where the size is not tracked by the type system. Of course the problem comes when you have to interface some code which expects a "Vect n a" and you have a "List a", but that's solvable by simply checking the size (dynamically) and deciding what to do if your "List a" isn't of size exactly n. (Fail, or whatever.). Going from "Vect n a" to a "List a" is trivial, of course. ... but really, that's where most of the friction is: Boundaries between APIs where the types don't quite line up. (Which is often the case for other languages, tbf. We tend to just notice less at compile time since most languages are so bad at expressing constraints.)
  • unstruktured 2y ago
    What, to you, is an ultra strong type system? Both OCaml and Haskell are used in plenty of non academic contexts. Do you mean something like Coq or F*?
    • BiteCode_dev 2y ago
      "plenty" is relative. You don't see many GAFAM products created in either, and that's because of the trade off OP talks about.
      • randomdata 2y ago
        I don't see many GAFAM products created in any functional language, even those with primitive type systems. Are you sure it is the type system that is scaring people away?
    • pydry 2y ago
      I was thinking of Haskell and F#. Neither one is completely unused outside of academic contexts but it is rare. Rust is an example where a stronger type system has an associated payoff and it's being used all over.
  • 2y ago
• pmarreck 2y ago
  Idris is fascinating. I actually took the book about it on vacation with me. Software reliability is becoming increasingly important as we tie all these systems together because it multiplies the number of possible unanticipated failure modes. Regarding the ultimate utility of languages initially considered "academic," the languages Lisp, Haskell, Prolog, Scala, Erlang and OCaml would like to have a word ;)
  • nottorp 2y ago
    But most of those don't have a real type system though? And definitely not a strict one.
    • nyssos 2y ago
      Scala, OCaml, and Haskell all have very powerful type systems. OCaml and Haskell even have good ones.
• andsoitis 2y ago
  > arbitrary rules a programmer knows about the bounds of a value Ada's generalized type contracts using subtype predicates work pretty well for this: https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Developer/chapters/05_Type_System.html#generalized-type-contracts-subtype-predicates https://learn.adacore.com/courses/Ada_For_The_CPP_Java_Devel... You can use it for something as simple as expressing ranges, or to represent types with arbitrary constraints, including types with discontinuities.
  • kqr 2y ago
    But these are only promised to be checked at runtime, even though the compiler can sometimes hint at things earlier.
    • docandrew 2y ago
      With SPARK mode you can check them at compile-time with provers and elide the runtime checks. You can do _very_ sophisticated type predicates this way.
• ParetoOptimal 2y ago
  Haskell has real world examples, for instance: https://docs.servant.dev/en/stable/tutorial/ApiType.html https://docs.servant.dev/en/stable/tutorial/ApiType.html
• turboponyy 2y ago
  I empathize with this point of view - if not in any other way then in principle. However, as a counterpoint, I'd suggest that encoding all known invariants as types may be prohibitively cumbersome and time-consuming - to the point where writing the program becomes more of an exercise in proofs rather than producing something useful. Often the invariants of a program are implied or can be easily inferred by the reader, which can actually make the program easier to understand for both the reader and the writer by leaving some things unsaid. Of course, whether a program is easier to understand when its invariants are written down vs. when they are left to be inferred by the reader is probably a matter of circumstance, so different tools for different jobs and all that. I've recently been writing a small program in Go - my first foray into the language - and I thoroughly enjoy how it gets out of my way. The lack of rigor is freeing if you don't stop to think about it too much.
  • ryangs 2y ago
    The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.
    • mason55 2y ago
      Yeah - in theory they are the same thing. You can have a dependent type that's an array with a length of 5 or you can create a type called ArrayLengthFive, and in both cases the type checker ensures that you don't accidentally use an unbounded array. But the difference is that with a dependent type, you get more guarantees (e.g. my ArrayLengthFive type could actually allow for arrays of length 20!). And the type checker forces you to prove the bounds (there could be a bug in my code when I create an ArrayLengthFive). And the dependent type allows other parts of the system to use the type info, whereas ArrayLengthFive is just an opaque type. I do think there is room for both ways of working. In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself. But there are certainly other cases where it is useful to encode the data constraints into the type so that you can do more operations downstream.
• harporoeder 2y ago
  With dependent types you still end up having to do dynamic checking of invariants for a substantial portion of real world code to construct the value with the properties you want. Anything coming from disk or network or a database etc. In practice I feel that it is far easier to just do manual dynamic checking with the constructor hidden from other modules such as `constructEmail :: string -> Email' which uses normal value level code, a common Haskell pattern. Obviously a little less flexible for the common dependent type examples of such as appending two vectors of a specific length.
  • duped 2y ago
    You should be parsing/validating any value coming from disk or the network
    • wvenable 2y ago
      You never know when the file will just suddenly be all zeros.
• jerf 2y ago
  The benefits of such an approach would be substantial. However, nobody has gotten the costs down below "eye watering", or similar other metaphors. It's not that it can't be done, it's that it is not yet known if it can be done in a way that comes out positive on the cost/benefits engineering analysis. I am open to the possibility that it can, but at the same time, I'd say if I draw the trendline of progress in this area out, it's not really all that encouraging. If you want to see why it has remained only academic, spend some time with Idris and take notes on how many problems you encounter are fundamental to the paradigm versus problems that can be solved with a larger involvement of effort. You'll want to pick a task that fits into its library ecosystem already, and not something like "hey, I'll write a fully generic HTTP server that can be proved correct" on your first try. I seriously suggest this, it's very educational. But part of that education will probably be to tone down your expectations of this being a miracle cure any time soon. I don't say this to celebrate the situation; it's a bummer. But if the situation is ever going to be solved, it's going to be solved by people viewing it clearly. (One of the major problems I see is that when you get to this level of specification, you end up with everything being too rigid. It is true that a lot of programming problems arise from things being made too sloppy and permitting a lot of states and actions that shouldn't exist. But some of that slop is also what makes our real-world systems compose together at all, without the original creator having to anticipate every possible usage. The "richer" the specifications get, the more rigid they get, and the more the creator of the code has to anticipate every possible future usage, which is not a reasonable ask. While I'd like to have the option to lock down many things more tightly, especially certain high-priority things like crypto or user permissions, it is far from obvious to me that the optimum ideal across the entire programming world is to maximize the specification level to this degree. And those high-priority use cases tend to jump to mind, but we also tend to overestimate their size in the real world. If we are going to see this style of programming succeed, we need to figure out how to balance the rigidity of tight specification with the ability to still flexibly use code in unanticipated manners later, in a context where the original specifications may not be quite right, and I think it's pretty unclear how to do that. Tightening down much past Haskell seems pretty challenging, and even Haskell is a bridge or three too far for a lot of people.)
  • AnimalMuppet 2y ago
• vbezhenar 2y ago
  I'm surprised that most popular languages don't even do simple type constraints. Like x: 1..100 y: "yes" | "no" I feel that there are lots of low hanging fruits when it comes to typing which would improve both program readability and correctness.
  • phaedrus 2y ago
    Ada code resembles this.
  • paulddraper 2y ago
    TypeScript does the latter. The former is difficult to track through arithmetic operations.
    • randomdata 2y ago
      Typescript also does the former, albeit with less friendly syntax. X: 1 | 2 | 3 // …
      • betenoire 2y ago
        Kinda but not really. It actually handles type inference on string concatenation, but doesn't understand math. type N = 1 | 2 const x1:N = 1 const x2:N = 1 const sum:N = x1 + x2 Typescript (the version running on my box) considers this an error.
        • randomdata 2y ago
          There is nothing to suggest that 1..100 understands math.
          • betenoire 2y ago
            I think the whole point of a type fully understanding the constraints of your data suggests it would ideally. Typescript is able to do this with strings when using templates. type Suit = "C" | "D" | "H" | "S"; type Rank = "A" | "2" | "3" | "4"; type Card = `${Suit}${Rank}`; const club = "D"; const ace = "A"; const aceOfClubs: Card = `${club}${ace}`; Even though I have not declared the club or ace as a Suit or Rank, it still infers the Card correctly in the last line. This is a stronger form of typing than what you are settling for where 1..100 doesn't know its own range. This is the difference I'm referring to.
• taeric 2y ago
  I regret to say that every type level Gordian knot that I have ever been exposed to came from attempts to do this. I think a lot of the problem is that many of the constraints and acceptable values for data are not determined until well after first deployment. The "knot" comes in when you are explicitly changing data and code to add a feature that you didn't anticipate at the start. This is a lot like schemaless databases. The flexibility of not having to fully specify the full schema does not mean that you don't benefit from specifying parts of it? Indeed, if you are indexing things, you have to specify those parts. But it is hard to argue with a straight face that schemaless tools don't have some strong benefits.
  • thesuperbigfrog 2y ago
    >> This is a lot like schemaless databases. The flexibility of not having to fully specify the full schema does not mean that you don't benefit from specifying parts of it? Indeed, if you are indexing things, you have to specify those parts. But it is hard to argue with a straight face that schemaless tools don't have some strong benefits. This is very similar to what Rich Hickey argued in "Simplicity Matters": https://youtu.be/rI8tNMsozo0?si=xTkpsLYTYh0jA5lB https://youtu.be/rI8tNMsozo0?si=xTkpsLYTYh0jA5lB Basically when you use a hash / JavaScript-style object rather than a fixed struct definition for your data (which amounts to a schema- less database in aggregate) Easy addition of new properties Co-existence of different versions of objects (newer objects will typically have more properties) Introspection of properties and validation rules / reflection
    • wwweston 2y ago
      Sometimes I’ve wondered if versioned types might be a help in bringing coexistence to a typed setup, and if this is part of where the benefits of a service oriented architecture come from. But given how versioning snarls can play out in dependency management I expect this idea has some tradeoffs in the best case.
      • taeric 2y ago
        I'm curious what you have in mind that doesn't boil down to "duck typing?"
• prmph 2y ago
  To check these types would then require possibly infinite time, and the checking may never halt, per the halting problem. Useful types are a compromise between expressiveness and practicality.
  • rictic 2y ago
    It's true that there are valid programs which don't type check in the same way that for any mathematical system there are truths which can't be proven. In practice though, almost any program you'd want to write can be type checked, in the same way that few proofs get tied into Gödelian knots.
    • prmph 2y ago
      True, but there is a difference between "can be type checked" and "can be type checked in a reasonable amount of time". I get reminded of this everything I have to work with a certain large Typescript code-base of mine that makes heavy use of union and template literal types. The Typescript Language Server has a hard time with these types. Frequently, everything slows to a crawl in VSCode, and it take 10 minutes of more for intellisense to update after every type change, ouch. Although in this case, I suspect it is Typescript's implementation of union types that is to blame (since other languages seem to handle complex union types with ease), this experience still shows that type checking can become quite expensive.
• galkk 2y ago
  Requirements change, things evolve. Having bounds in the type system is too restrictive. Even history of "required", rather simple restriction on the value, is showing that putting that logic into type system is too much of a burden. https://capnproto.org/faq.html#how-do-i-make-a-field-required-like-in-protocol-buffers https://capnproto.org/faq.html#how-do-i-make-a-field-require...
  • skybrian 2y ago
    This is true when you can’t upgrade all the data and all the data generators. But there are smaller systems where you can actually upgrade everything you have and set some new requirements for everything coming in.
  • yencabulator 2y ago
    The other alternative is what protobuf did to solve the same pain: In proto3, all optionals have a default value. They're effectively required where the default value doesn't need to be encoded in the message. The exact different between the two approaches is subtle. Technically you can fancier things with the framework exposing the optional values as set/not set, but in practice a lot of code is a lot simpler with default values. https://protobuf.dev/programming-guides/proto3/#default https://protobuf.dev/programming-guides/proto3/#default
  • stouset 2y ago
    If the requirements change, you can update the definition in the type system once. And then you immediately know the locations where this new bound is violated.
• kelseyfrog 2y ago
  I wish it were possible, but I have a sneaking suspicion that types like PrimeNuber or TotalProgram, are beyond the realm of possibility.
  • moomin 2y ago
    PrimeNumber is definitely possible in pretty much any dependent type language. Indeed, it would be pretty impossible to get any work done in Lean without it. TotalProgram: possible in some, not in others, I think.
    • kelseyfrog 2y ago
      > PrimeNumber is definitely possible in pretty much any dependent type language. That's awesome! Thank you. I didn't know type systems were capable of expressing that level of sophistication. Would HaltingProgram and NonHaltingProgram be expressible? I hope it's clear what I'm trying to convey, but the technical wording escapes me today.
      • mrkeen 2y ago
        see the 'total' keyword in Idris https://docs.idris-lang.org/en/latest/proofs/patterns.html https://docs.idris-lang.org/en/latest/proofs/patterns.html
      • xmgplays 2y ago
        HaltingProgram and MaybeHalting is expressible(or vice versa), if you want to cover all programs in one of two types. If you want specifically HaltingProgram and NotHaltingProgram then you need a third category of MayOrMayNotHaltingProgram.
      • moomin 2y ago
        There is a fascinating result about types that they have a one to one correspondence with proofs. Dependent type systems leverage that to the hilt.
• klysm 2y ago
  I agree with the philosophy at a high level, but opening up the power of what you can do at compile time is a very deep and nuanced trade off space. I think there’s a more general way to state what you’re getting after as well: we should be able to express arbitrary constraints that are enforced by the compiler. These constraints don’t really have to be about values themselves but could also be about how they are consumed e.g. linear types. Unfortunately, the more powerful the type system, the harder it is to make inferences. Generality comes at a cost.
• rictic 2y ago
  I'm optimistic that improved proof search using modern AI can make working with dependent type systems much more productive and practical. A future programmer may be spending more time formally describing the invariants of the system.
• carapace 2y ago
  > a type should be capable of reflecting any arbitrary rules a programmer knows about the bounds of a value That's a programming language. In other words, now your type system needs a type system.
  • mrkeen 2y ago
    Sure. If you're Haskell, you call them kinds. In Idris, they're just types.
    • carapace 2y ago
      Yes but that misses the point. The pragmatic (not to say economic) motivation for type systems in the first place is to eliminate bugs in software. If you make them more complicated it makes it harder (more expensive, cost is always brought up as a barrier to correctness) to use them.
• anamax 2y ago
  That sounds like you're using "type" to mean "representation", albeit with a lot of detail. I may be odd, but my programming problems are rarely due to the number of bananas or how bananas are represented, but whether I'm working with the correct bananas.