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.

>> 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

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

The first two properties can be handled by adding optional fields to your struct. The third can be done at compile time rather than runtime if you define a strict class hierarchy. I think really the problem is that many languages make struct definition needlessly verbose so it feels convenient to just use a map. The price of using schemaless includes runtime performance as well as the compiler being unable to warn you about easy (for a compiler) to detect and report data mismatch errors. I have spent a lot of time using lua the way I think many people use clojure. It is quite seductive and does feel very productive at first, but eventually I find that for a sufficiently complex program, I want the compiler to validate my data usage for me.

Protobufs are an interesting hybrid. They assume a common, linear history of schema versions, where all data generators had access to an arbitrary version in that history. The schemas define field ids and types, but not which combinations of fields can show up.

If you can upgrade all the data then you don’t need to worry about versioning,

Or you can do it like HTTP headers and hope for the best.

Protobufs are also a fun place to look for how much debate people will get into regarding required versus optional fields. Your post is taking an implicit "everything is optional" view. But, it does allow you to be stricter.

Common Lisp Object System also touched on all of these ideas years ago.

Everything has been `optional` for about a decade.

> The option to set a field to required is absent in proto3 and strongly discouraged in proto2.

https://protobuf.dev/overview/#syntax

Ah, I dropped off protobuf a while back. I definitely remember a lot of uproar about it, at the time.

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.

I'm curious what you have in mind that doesn't boil down to "duck typing?"

Not the most elegant mechanism, but it should be accessible to imagine an implementation via inheritance hierarchies even for a static manifestly typed language. Class "Person4.1" inherits from class "Person4" inherits from class "Person2" inherits from "Person". Probably there's a better way (and one could argue that a design where knowing the version of the class/object matters isn't a well-encapsulated design, which could have something to do with why duck typing often works out better than expected in OO systems).

I think my question is what would you be doing here that doesn't boil down to "has these properties/methods, I'll accept"?

I think this is a lot easier if you exclude the "methods" in my quote there. Since those almost certainly have the same general contract that would spread across things.

You might be interested in the Unison language then.

> 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.

Let me put on my straightest face.

Schemaless tools have no benefits.*

As soon as you start _doing_ anything with your data, it has a schema. You may not have declared it to your data store, to a specific piece of code, etc, but your application logic almost definitely makes assumptions about the shape of the data--what fields are and aren't present, the types of values in those fields, and what those values mean.

Every piece of your system must either accept undefined behaviour in the face of data which doesn't fit this implicit schema (there are very few non-trivial problems where you can define a meaningful, valid output for all possible inputs), or essentially treat the schemaless parts as hostile and assert its assumptions before every action.

The only thing you've done by going "schemaless" is distributing your schema across your systems and pushed the schema validation out to each thing interacting with the schemaless components instead of centralizing it.

* Yes, literally storing raw, unstructured data. But as soon as you need to _do_ anything with the data besides regurgitate it you're back to it having some sort of schema.

So you have mainly straw-manned on the word "schemaless" to make an argument. This is akin to attacking dynamic typing by pointing out that most things can be type inferred by the code.

That is, you are not wrong in that most data stored is structured in some way; but you are ignoring a ton of the benefit of the schemaless world. As I pointed out, there are benefits to specifying schema. In parts, you /have/ to do so. Specifically if you want your DB to do any work on the data. Indexing/filtering and the like.

Now, you do hit largely on the benefits of the "schemaless" world. And that is that it is not undefined how it will store whatever schema you throw at it. You will have restrictions on keys, but otherwise it will store whatever you throw at it.

At large, this means you can skip out on a lot of the formality of specifying all schema shapes during development and can take a much more flexible approach in your code than you are forced to if the data layer can't work with you.

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-require...

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.

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

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.

I wish it were possible, but I have a sneaking suspicion that types like PrimeNuber or TotalProgram, are beyond the realm of possibility.

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.

> 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.

see the 'total' keyword in Idris

https://docs.idris-lang.org/en/latest/proofs/patterns.html

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.

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.

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.

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.

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.

> 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.

There is also the in-between Rust approach. Start with the user input as a byte array. Pass it to a validation function, which returns it encapsulated within a new type.

    #[derive(Clone, Hash, Ord, Eq...)]
    struct Email(Box<str>);

    // validate UTF-8 + 
    fn validate(raw: &[u8]) -> Result<Email, EmailValidationError>;

What is annoying is the boilerplate required. You usually want your new type to behave like a (read-only) version of the original type, and you want some error type with various level of details.

You can macro your way out of most of the boilerplate, with the downside that it quickly becomes a domain specific language.

AKA the "parse, don't validate" approach [1].

1: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...

The salient excerpt is: "A parser is just a function that consumes less-structured input and produces more-structured output". In opposition to a validation function that merely raises an error.

    - validate(raw) -> void
    - parse(raw) -> Email | Error

Of course the type signature is what seals the deal at the end of the day. But I am going to follow this naming convention from now on.

Parsing a string into an email, of course, is already fraught with peril. Is it valid HTML? Or did you mean the email address? Is it a well formed email, or a validated address that you have received correspondence with? How long ago was it validated? Fun spin on the, "It's an older code, sir, but it checks out."

I've seen attempts at solving each of those issues using types. I am not even positive they aren't solvable.

Validation is an event, with it's own discrete type separate from the address itself. This is no different than a physical address.

    123 Somewhere Lane
    Somewhereville, NY 12345

is a correctly formatted address but is almost certainly not one that physically exists.

Validation that it exists isn't solvable in the type system because, as I mentioned, it is an event. It is only true for the moment it was verified, and that may change at any point in the future, including immediately after verification.

I think I get your point. I would add reconciliation to validation. In that sometimes you cannot validate something without doing it, and are instead storing a possibly out of band reconciliation of result.

I'm curious, though, in how this argument does not apply to many other properties people try and encode into the types? It is one thing if you are only building envelopes and payloads. And, I agree that that gets you a long way. But start building operations on top of the data, and things get a lot more tedious.

It would help to see examples that were not toy problems. Every example I have seen on this is not exactly leaving a good impression.

There are things that can embed a bit of temporal logic into types, such as a linear type that can statically guarantee a file handler has been closed exactly once, or error.

For the most part, what I think people really want are branded types. F# has a nice example of unit, where a float can be branded Fahrenheit or Celsius or Kelvin, and functions can take one of those types as parameters.

You then have some function that can parse user input into a float and brand it one of those types. The compiler doesn't make any guarantees about the user input, only that the resulting branded value cannot be used where a different one is expected. Other good examples are degrees and radians, or imperial and metric, etc.

Depending on what you are doing, knowing at a type level that some number can never be negative (weight in pounds) can save you a lot of hassle. If one part of the system doesn't brand a value, and it feeds into another part of the system that is branded, you're stuck with extraneous runtime checks all over the place or a lot of manual unit tests. Instead, the compiler can point out exactly, and in every instance, where you assumed you had a validated value but instead did not.

Some of these are why I would add reconciliation to the idea. Linear types, specifically. You can encode that you only send a message once. But, without doing reconciliation with the destination, you can not be sure that it was received.

I'm torn, as the examples from small programs make a ton of sense and I largely like them. I just cannot escape that every attempt I've seen at doing these in large programs is often fairly painful. I cannot claim they are more error prone than the ones that skip out on it. I can say they are far more scarce. Such that the main error condition appears to be to stall out on delivery.

But then ironically, the problem with relying on programming language type systems is that they don't scale (beyond the boundaries of a single process). As soon as you are crossing a wire you have to go back to runtime validations.

Throwing out type safety simply because you have unverified input is a little silly. It's trivial in most statically typed languages to safely turn input into a concrete type (or an error if it is invalid) at the edge and meanwhile maintain type safety throughout the rest of the code.

There's where good documentation and training pays off.

Some invariants that are too complex to express purely in code, requiring numerous separate low level bookkeeping functions throughout the system, can be concisely expressed as a high level idea in natural language (wether as comments or at an external technical document).

Make sure that your developers are exposed to those documents, throw in a few tests for the most obvious cases to ensure that newcomers are learning the invariants by heart, and if they're competent you should not have problems but in the most obscure cases (that could appear anyway even if you try to formalize everything in code).

Typed constraints don't scale either.

I eagerly await your implementation of a type describing my tax return. And to implement a compiler for the new programming language you'll inevitably have to construct, we're gonna need two types, one expressing all valid source programs, and the other all valid programs for the target platform.

Oh, can we also get updates to that for next year's taxes, new platforms, and other such future business needs? Of course the current requirements have to still remain supported.

There is no world where the added time here for the developers is with the trade off, and if you look through my history, you will see that I largely reject “dev time trade off” as a notion a company should ever seriously entertain as a significant burden.

> 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_Devel...

You can use it for something as simple as expressing ranges, or to represent types with arbitrary constraints, including types with discontinuities.

But these are only promised to be checked at runtime, even though the compiler can sometimes hint at things earlier.

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.

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.

You should be parsing/validating any value coming from disk or the network

You never know when the file will just suddenly be all zeros.

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.

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.

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.

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.)

Slightly more optimistically: As we go along, small pieces go from "too expensive to actually use" to "usable on real projects, but nobody does yet", and then to "doesn't everybody do that?"

This is the story of improvements in type systems over the last 70 years. But the progress is very slow. So this is only slightly more optimistic...

This is where I'd really be interested in seeing an AI system help. Don't write an AI system that helps me shovel out vast quantities of code, and then solves the problem of the resulting incomprehensible mass of code being impossible to work with by making it even easier to shovel out yet more masses of code to deal with the even larger masses of AI-generated code. It does not take a genius to see that this ends up with even the AIs being staggered by the piles of code in the world until all intelligences, natural and otherwise, are completely bogged down. (Exponential complexity growth defeats everyone in this physical universe, even hypothetically optimal AIs running on pure computronium.) Write me an AI that can help me drive something closer to Idris and bridge the gap between that overly-rigid world I'm complaining about and the more human/real-world goals I'm really trying to accomplish, have the AI and the programmer come to a meeting-of-the-minds and produce something with exactly the right rigidity in it, and help me reuse the results of other's work.

I mean... we're going to end up with the first one. But a man can dream. And while I will cynically say we're going to end up with the first one, it is at least possible that we will then recognize there's a problem and pursue this second approach. But not until the first approach bites us, hard.

I think the world of datalog and dynamic logic programming (or perhaps Answer Set Programming with Constraints) may be very useful in scenario 2, and people are still pursuing that without waiting for scenario 1 to happen first.

Yeah, scenario 1 will also probably still happen.

Hell, even with agreeing to a very rigid world view, that'd be a dream. Imagine an AI proof assistant that does two things:

1. writes more proofs, focusing on the area I point at

2. makes small, atomic, incremental, suggestions to make it easier to prove something; once those pass proofs+tests, go back to #1

But hey, that would likely require some sort of artificial mental models and iterative reasoning, and not just slapping more compute+data together into a word generator...

Haskell has real world examples, for instance:

https://docs.servant.dev/en/stable/tutorial/ApiType.html

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.

Ada code resembles this.

How would you ensure that the values of the types doesn't invalidate the contract? Easy for basic assignment, but not sure how you would do that when doing arbitrary mutation.

You could prove to the type checker that you're only allowing input values that, when fed to your operation, results in outputs that remain in bounds. For example, if you're doing addition, you first check that each input is between 1 and 49, and you exhaustively handle the cases where the values are out of those bounds. Then the type checker can see that the output is always between 1 and 100.

For operations/mutations where it's more complex to validate the inputs, you could assign the result to an unbounded variable, and then prove to the type checker that you're exhaustively handling the output before you assign it to a bounded variable. For example, multiply two unbounded numbers, store the result in an unbounded variable, then do "if result >= 1 && result <= 100 then assign result to var[1..100] else .... end"

You could prevent arbitrary mutation, pushing computation onto a more flexible type and allowing assignment back to the more constrained type only when first guarded by an appropriate conditional. The whole "parse, don't validate" thing.

The reference (an excellent read!): "Parse, don't validate" https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...

TypeScript does the latter.

The former is difficult to track through arithmetic operations.

Typescript also does the former, albeit with less friendly syntax.

   X: 1 | 2 | 3 // …

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.

There is nothing to suggest that 1..100 understands math.

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.

The difference you are referring to was already asserted in your first comment. I'm afraid whatever you were trying to add here is being lost. Unless you were, strangely, straight up repeating yourself for no reason?

let me say in fewer words:

>There is nothing to suggest that 1..100 understands math.

That's like, your opinion man. I'd like it.

You'd like what? For the type checker to understand math? We know that already. You said that in your first comment. And the second one. And the third one. And now seemingly the fourth one. But let it be known, whatever new information you are trying to add here is getting lost in translation.

In the type-theoeretic world, you want to refer to "refinement types" [0]. Some interesting work that I have seen in this direction is Liquid Types [1][2]. There is some work in Haskell[3], but it is surprisingly very useful in Rust as well.

[0] https://en.wikipedia.org/wiki/Refinement_type [1] https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li... [2] https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [3] https://ucsd-progsys.github.io/liquidhaskell/ [4] https://github.com/flux-rs/flux

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.

What made it seem too restrictive to you? Or what were your experiences trying to apply it to real-world scenarios?

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?

ah, I think I misunderstood. Still getting through the Idris book :)

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.

Indeed. A type means assigning a rigid category to something.

There is not a single taxonomy that is universal, it ends up like the Celestial Emporium of Benevolent Knowledge that decides animals into:

    those belonging to the Emperor,

    those that are embalmed,

    those that are tame,

    pigs,

    sirens,

    imaginary animals,

    wild dogs,

    those included in this classification,

    those that are crazy-acting,

    those that are uncountable,

    those painted with the finest brush made of camel hair,

    miscellaneous,

    those which have just broken a vase, and

    those which, from a distance, look like flies.

Then you have a new use case.

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*?

"plenty" is relative.

You don't see many GAFAM products created in either, and that's because of the trade off OP talks about.

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?

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.

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.)

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 ;)

But most of those don't have a real type system though? And definitely not a strict one.

Scala, OCaml, and Haskell all have very powerful type systems. OCaml and Haskell even have good ones.

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.

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.

> 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.

Sure. If you're Haskell, you call them kinds. In Idris, they're just types.

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.

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.