4 ms·

I think that's backwards - ultimately everything on a computer is just bytes, so if you push that philosophy to the limit then you would write untyped functions

by lmm 1y ago

I think that's backwards - ultimately everything on a computer is just bytes, so if you push that philosophy to the limit then you would write untyped functions and they can "just work" on any input (just not necessarily giving results that are sensible or useful if the input is wrong). The point of a type system is to help you avoid writing semantically wrong code, to bring errors forward, and actually the most important and valuable use case is distinguishing values that are structurally identical but semantically different (e.g. customer ID vs product ID, x coordinate vs y coordinate, immutable list vs read view of mutable list, sorted vs unsorted...).

b_e_n_t_o_n 1y ago
I think the structural type approach leans heavily into the "computation is just data and its transformations", so it makes sense for it to treat data as the most important thing. You end up thinking less about classification and more about the transformations. I'm not saying the nominal approach to types is wrong or bad, I just find my way of thinking is better suited for structural systems. I'm thinking less about the semantics around product_id vs user_id and more about what transforms are relevant - the semantics show up in the domain layer. Take a vec3 for example, in a structural system you could apply a function designed for a vec2 on it, which has practical applications.
- valenterry 1y ago
  > I think the structural type approach leans heavily into the "computation is just data and its transformations" But it's never "just data". My password is different in many ways than my username. Don't you ever log/print it by accident! So even if structurally the same, we MUST treat it different. Hence any approach that always only looks at things structurally is deeply flawed in the context of safe software development.
  - deleted 1y ago
    [deleted]
  - b_e_n_t_o_n 1y ago
    Yeah you bring up a good point. A { name: string } dict needs to be treated differently from a { user_pw: string } dict. The difference is that happens in the domain layer instead of the type layer.
    - SkiFire13 1y ago
      That's no difference than using newtype structs. If you remove the extra layer you are left with `string` for both of them. > The difference is that happens in the domain layer instead of the type layer This view greatly reduces the usefulness of the type layer though, as that's the only automated tool that can help the domain layer with handling cases like this.
      - b_e_n_t_o_n 1y ago
        It's not really automated though, it's just another layer of code written by a human, prone to the same types of human error.
        lmm 1y ago
        Bugs in the typechecker are rare (it's widely exercised if the language is at all popular) and generally fixed quickly. If you have an expression of type A you can be pretty confident you're getting a value that's passed through a constructor for type A. Can a human encode something different by that than what they intended to encode? Certainly. But it's got the highest cost-benefit of any approach to double-checking your code I've found.
        b_e_n_t_o_n 1y ago
        That's not what I mean. It's trivial to encode your types in such a way that it incorrectly implements domain logic and there is no meta-meta language enforcing correctness there.
        lmm 1y ago
- lmm 1y ago
  > I'm not saying the nominal approach to types is wrong or bad, I just find my way of thinking is better suited for structural systems. I'm thinking less about the semantics around product_id vs user_id and more about what transforms are relevant - the semantics show up in the domain layer. But that domain layer should make use of the type system! That's where the type system is most useful!
  - RossBencina 1y ago
    I've seen this debate play out before. Often the type theory people and the domain modeling people end up talking past each other. I think type-theoretic safety is a completely different thing to the use of types (and names) in software-as-domain-modeling (for example, but not necessarily OO modelling). At different times, for different people, one perspective is more important than the other. It is important not to confuse the perspectives, and to value both of them, but also to recognise their strengths and weaknesses. One theme that sometimes emerges is that the type theory people don't care about names at all. Not even field names. Taken to the extreme Customer( name: str; age: int) is just a Tuple[str, int]. The words "Customer", "name", "age" have no place in the code base. My take is that when you are dealing with computer-scientific abstract things, e.g. a List of T, then there is no need to reference the domain entities; placeholder names like T, x, xs make sense. On the other hand, if you're writing an application that models domain semantics (eg. business rules), writing software amounts to modelling the domain, it should be easy to correlate software entities with the real-world entities that they model. To do this we use descriptive words, including names, domain events, activities and so on. e.g. List[Customer] not List[Tuple[str, int]]. Then again, you could replace all of the type names with A, B, C, ... and all the variable names with w, x, y, .... The example would end up as X[Y[Z,W]], the software would work exactly the same, and you might get some insights into the structure of the system. However, if you're in the business of building a user management system in general this is not going to fly for very long with your workmates or your client. You will have trouble onboarding new developers.
    - b_e_n_t_o_n 1y ago
      I think this is a superb point. If you look at Clojure and Rich Hickey's justifications for it's design, he talks a lot about designing systems that work with a world that is changing constantly, interfacing with systems where you can't always guarantee a stable contract, solving problems that use non-elegant models, dealing with state and time, and change in ways you can't predict. Eric Normand wrote a great article on this and he comes from a dual Haskel/Clojure background [1]. Nominal static type systems absolutely have their place, especially with closed systems where the abstractions are different. 1: https://ericnormand.me/article/clojure-and-types https://ericnormand.me/article/clojure-and-types

by lmm 1y ago

b_e_n_t_o_n 1y ago

I think the structural type approach leans heavily into the "computation is just data and its transformations", so it makes sense for it to treat data as the most important thing. You end up thinking less about classification and more about the transformations. I'm not saying the nominal approach to types is wrong or bad, I just find my way of thinking is better suited for structural systems. I'm thinking less about the semantics around product_id vs user_id and more about what transforms are relevant - the semantics show up in the domain layer. Take a vec3 for example, in a structural system you could apply a function designed for a vec2 on it, which has practical applications.

valenterry 1y ago
> I think the structural type approach leans heavily into the "computation is just data and its transformations" But it's never "just data". My password is different in many ways than my username. Don't you ever log/print it by accident! So even if structurally the same, we MUST treat it different. Hence any approach that always only looks at things structurally is deeply flawed in the context of safe software development.
- deleted 1y ago
  [deleted]
- b_e_n_t_o_n 1y ago
  Yeah you bring up a good point. A { name: string } dict needs to be treated differently from a { user_pw: string } dict. The difference is that happens in the domain layer instead of the type layer.
  - SkiFire13 1y ago
    That's no difference than using newtype structs. If you remove the extra layer you are left with `string` for both of them. > The difference is that happens in the domain layer instead of the type layer This view greatly reduces the usefulness of the type layer though, as that's the only automated tool that can help the domain layer with handling cases like this.
    - b_e_n_t_o_n 1y ago
      It's not really automated though, it's just another layer of code written by a human, prone to the same types of human error.
      - lmm 1y ago
        Bugs in the typechecker are rare (it's widely exercised if the language is at all popular) and generally fixed quickly. If you have an expression of type A you can be pretty confident you're getting a value that's passed through a constructor for type A. Can a human encode something different by that than what they intended to encode? Certainly. But it's got the highest cost-benefit of any approach to double-checking your code I've found.
        b_e_n_t_o_n 1y ago
        That's not what I mean. It's trivial to encode your types in such a way that it incorrectly implements domain logic and there is no meta-meta language enforcing correctness there.
        lmm 1y ago
lmm 1y ago
> I'm not saying the nominal approach to types is wrong or bad, I just find my way of thinking is better suited for structural systems. I'm thinking less about the semantics around product_id vs user_id and more about what transforms are relevant - the semantics show up in the domain layer. But that domain layer should make use of the type system! That's where the type system is most useful!
- RossBencina 1y ago
  I've seen this debate play out before. Often the type theory people and the domain modeling people end up talking past each other. I think type-theoretic safety is a completely different thing to the use of types (and names) in software-as-domain-modeling (for example, but not necessarily OO modelling). At different times, for different people, one perspective is more important than the other. It is important not to confuse the perspectives, and to value both of them, but also to recognise their strengths and weaknesses. One theme that sometimes emerges is that the type theory people don't care about names at all. Not even field names. Taken to the extreme Customer( name: str; age: int) is just a Tuple[str, int]. The words "Customer", "name", "age" have no place in the code base. My take is that when you are dealing with computer-scientific abstract things, e.g. a List of T, then there is no need to reference the domain entities; placeholder names like T, x, xs make sense. On the other hand, if you're writing an application that models domain semantics (eg. business rules), writing software amounts to modelling the domain, it should be easy to correlate software entities with the real-world entities that they model. To do this we use descriptive words, including names, domain events, activities and so on. e.g. List[Customer] not List[Tuple[str, int]]. Then again, you could replace all of the type names with A, B, C, ... and all the variable names with w, x, y, .... The example would end up as X[Y[Z,W]], the software would work exactly the same, and you might get some insights into the structure of the system. However, if you're in the business of building a user management system in general this is not going to fly for very long with your workmates or your client. You will have trouble onboarding new developers.
  - b_e_n_t_o_n 1y ago
    I think this is a superb point. If you look at Clojure and Rich Hickey's justifications for it's design, he talks a lot about designing systems that work with a world that is changing constantly, interfacing with systems where you can't always guarantee a stable contract, solving problems that use non-elegant models, dealing with state and time, and change in ways you can't predict. Eric Normand wrote a great article on this and he comes from a dual Haskel/Clojure background [1]. Nominal static type systems absolutely have their place, especially with closed systems where the abstractions are different. 1: https://ericnormand.me/article/clojure-and-types https://ericnormand.me/article/clojure-and-types