4 ms·

Nix already has a ton written in it and it works... Magically. Gradual typing for a system like this is the proper thing to do. You can always write a static l

by anon291 9mo ago

Nix already has a ton written in it and it works... Magically. Gradual typing for a system like this is the proper thing to do. You can always write a static linter for sections you need tested and maybe eventually you'll be able to type nixpkgs as well. Any solution to the nix typing problem NEEDS graduality. Nixpkgs is too large to make it possible to have one commit that fixes everything. Starting from scratch is not a realistic option either.

lmm 9mo ago
Maybe you need graduality, sure. Plenty of systems (e.g. Typescript) have added a real type system that works gradually onto an existing system. While there are compromises to that approach, it's still a lot more effective than contracts IME.
- anon291 9mo ago
  How are well specified contracts different from type script? Typescript is just annotation. Behavior cannot change. This is annotation plus runtime examinable behavior. This approach seems conducive to static checkers.
  - lmm 9mo ago
    > How are well specified contracts different from type script? Typescript has types, meaning expressions can be typechecked and this is distinct from evaluating them. Typechecking is more complete/consistent/reliable - you can catch type errors that don't show up in a codepath that gets actually executed. E.g. an empty list can be well typed, which as far as I can see you can't do with contracts.
    - anon291 9mo ago
      Typescript does not have a complete, consistent, or reliable type system, no. You can easily skirt around it. Indeed, there is no runtime guarantee at all. There is not even a function to enforce boundary conditions as far as I'm aware of. Contracts are better in every single way. Contracts are also type-checkable. Nix is deterministic and pure. You seem to be getting confused because contracts don't introduce new syntax.
      - lmm 9mo ago
        > Typescript does not have a complete, consistent, or reliable type system, no. You can easily skirt around it. Most practical type systems are not technically complete, consistent, or reliable, and all have "escape hatches". That doesn't make them useless. > Indeed, there is no runtime guarantee at all. There is not even a function to enforce boundary conditions as far as I'm aware of. Contracts are better in every single way. On the contrary. That typescript types do not exist at runtime makes them much better than contracts in many ways. > Contracts are also type-checkable. Not in general. More to the point, not in a way that's general enough to rely on in practice. > Nix is deterministic and pure. And notoriously a nightmare to write and debug. Evidently "deterministic and pure" is insufficient. (I'd also argue that it's not actually pure in the ways that matter - see "The C language is purely functional")

by anon291 9mo ago

lmm 9mo ago

Maybe you need graduality, sure. Plenty of systems (e.g. Typescript) have added a real type system that works gradually onto an existing system. While there are compromises to that approach, it's still a lot more effective than contracts IME.

anon291 9mo ago
How are well specified contracts different from type script? Typescript is just annotation. Behavior cannot change. This is annotation plus runtime examinable behavior. This approach seems conducive to static checkers.
- lmm 9mo ago
  > How are well specified contracts different from type script? Typescript has types, meaning expressions can be typechecked and this is distinct from evaluating them. Typechecking is more complete/consistent/reliable - you can catch type errors that don't show up in a codepath that gets actually executed. E.g. an empty list can be well typed, which as far as I can see you can't do with contracts.
  - anon291 9mo ago
    Typescript does not have a complete, consistent, or reliable type system, no. You can easily skirt around it. Indeed, there is no runtime guarantee at all. There is not even a function to enforce boundary conditions as far as I'm aware of. Contracts are better in every single way. Contracts are also type-checkable. Nix is deterministic and pure. You seem to be getting confused because contracts don't introduce new syntax.
    - lmm 9mo ago
      > Typescript does not have a complete, consistent, or reliable type system, no. You can easily skirt around it. Most practical type systems are not technically complete, consistent, or reliable, and all have "escape hatches". That doesn't make them useless. > Indeed, there is no runtime guarantee at all. There is not even a function to enforce boundary conditions as far as I'm aware of. Contracts are better in every single way. On the contrary. That typescript types do not exist at runtime makes them much better than contracts in many ways. > Contracts are also type-checkable. Not in general. More to the point, not in a way that's general enough to rely on in practice. > Nix is deterministic and pure. And notoriously a nightmare to write and debug. Evidently "deterministic and pure" is insufficient. (I'd also argue that it's not actually pure in the ways that matter - see "The C language is purely functional")