4 ms·

The article is exemplary – it's reasonably short, concise, beautifully visualized and explains a complex topic with simple terms. I'm confused with "type promo

by divan 8y ago

The article is exemplary – it's reasonably short, concise, beautifully visualized and explains a complex topic with simple terms. I'm confused with "type promotion" in the `ConnectionStatus` example, though. When we promote `Open` and `Closed` from terms to types, we make it easy to create a variable that can be either `Open` or `Closed`, but we're also breaking the mental model of the whole thing. `Open`/`Closed` is a property – not a "type" in a traditional way of thinking about types. For me, the type should map onto some abstraction in your mental world map, and `Open`/`Closed` is definitely not a good fit here. How do Haskell programmers address this problem? Do they think about types more in mathematical terms, rather than as tools for describing mental maps of the problem domain?

tiniuclx 8y ago
Open/Closed would still conceptually act as properties, but by promoting them to types you enforce the property at compile time rather than runtime. Note that they are not used on their own, but to describe a `Connection`. This lets you statically enforce the fact that you must only send data through an open connection, for example.
- divan 8y ago
  Right, that's the obvious benefit for the compiler (statically enforcing behaviour, etc), but I'm struggling with not seeing here a detremential effect for the human. To me, when you write code, you're encoding your understanding of the problem domain (mental map) into the code, describing it in a way that permits to restore it back. By reading a code your coworker or you 6 month later should be able to restore the same mental map you had while writing the code. And using type system to describe properties (there is another way to do it already in place – fields in structs), seems like complicating this task and it eventually should hurt readability.
  - almostdeadguy 8y ago
    The advantage is you basically don't have to think about the provenance of data (in this example what state is a connection in? was it closed before being given to me? etc.). It allows the compiler to ensure the user of this code can't perform operations that lead to error states by allowing the programmer to express the state transitions of a connection in their function declarations, as the provided example shows: newConnection :: Address -> Connection Closed openConnection :: Connection Closed -> Connection Open closeConnection :: Connection Open -> Connection Closed connectionAddress :: Connection s -> Address From a readability perspective, I would love this, it's effectively a state machine diagram explained by your function types.
  - thedufer 8y ago
    Statically enforcing behavior helps the human as well - in this example, it would make it more clear what types of things you can do with an open connection vs a closed one just by inspecting the types, whereas otherwise you would have to either find documentation or test it and see. We use type tricks like this (although not exactly in this way, as we don't really have a concept of kinds) in OCaml, and we find that in practice people new to the language aren't actually confused by it much - it actually makes readability better, not worse.
lmm 8y ago
> When we promote `Open` and `Closed` from terms to types, we make it easy to create a variable that can be either `Open` or `Closed`, but we're also breaking the mental model of the whole thing. `Open`/`Closed` is a property – not a "type" in a traditional way of thinking about types. For me, the type should map onto some abstraction in your mental world map, and `Open`/`Closed` is definitely not a good fit here. I don't think I follow? Something open is different from something closed; the construction of an open thing is different from the construction of a closed thing. The operations you can do on them are different. They're different varieties of thing, they should have different types. Edit: is your point that you wouldn't ever have a term that's just Open or Closed, only a Connection[Open] or Connection[Closed]? I guess that's true but it doesn't seem important. If you're comfortable with parameterised types at all then you're already comfortable with types that aren't directly applied to terms - e.g. you'll never have a term that's a List, only a term that's a List[Int] or what have you.
- divan 8y ago
  > Something open is different from something closed Right, but that's just a property of "something", not a type of it. When someone asks you "What type of door you have?" we don't say "I have an open door", rather "I've a timber door" or "glass door". This is how we understand the world after all, and to me type system should reflect our mental and cognitive processes. > If you're comfortable with parameterised types at all I think I have the same issue with parametrized types as well. Having `Vector<int>` is good for compiler, but not necessarily for humans. When you need to put a beads onto the string (the closest real-world analogy I came up with vector, haha), you don't think "hey, I need to find a string of type "beads" and then put beads onto it". You just take a string, and it implicitly "works" for beads. If you try to put something weird (why would you, btw?) onto it, you'll break the whole thing or it just didn't work. I'm not implying that we need to do everything as in offline world, but at least try to minimize discrepancies in the reasoning about the world in the code.
  - lmm 8y ago
    > Right, but that's just a property of "something", not a type of it. When someone asks you "What type of door you have?" we don't say "I have an open door", rather "I've a timber door" or "glass door". I think that's just because a given door can change between open and closed and be the same door? We're used to persistent global state and monotonic wall-clock time, but those are bad for programming and we should take the trouble to cast off those intuitions. > I think I have the same issue with parametrized types as well. Having `Vector<int>` is good for compiler, but not necessarily for humans. When you need to put a beads onto the string (the closest real-world analogy I came up with vector, haha), you don't think "hey, I need to find a string of type "beads" and then put beads onto it". You just take a string, and it implicitly "works" for beads. The point isn't that the string itself has a type, it's that a string of beads is a different kind of thing from a string of charms or a string of lights (at least, to the extent that a bead is a different kind of thing from a charm or a light). And you can't have a "string of" on its own - it's always a string of something - but there are things that it makes sense to do to a string of things without regard to the specific type of thing that's on it (e.g. count how many items are on it). Any kind of abstract concept has that issue. You can't ever get just "a square" in the real world - you can get a square of wood or a square of plastic or a square of cake, but it'll always be a square of something. Or you can't get "three" on its own - you can only ever get three of something. If we ask what type of thing you're sitting on, maybe it's a wheeled chair or a three-legged stool, and those types make sense even though it wouldn't make sense to say that you're sitting on "a wheeled" or "a three-legged".
Fellshard 8y ago
Domain modeling is fungible. In most cases, I'd expect it to be a property. In some cases, it could be it's better represented as separate types, especially if it makes both domain and software logic simpler to reason about and change.

by divan 8y ago

tiniuclx 8y ago

Open/Closed would still conceptually act as properties, but by promoting them to types you enforce the property at compile time rather than runtime. Note that they are not used on their own, but to describe a `Connection`. This lets you statically enforce the fact that you must only send data through an open connection, for example.

divan 8y ago
Right, that's the obvious benefit for the compiler (statically enforcing behaviour, etc), but I'm struggling with not seeing here a detremential effect for the human. To me, when you write code, you're encoding your understanding of the problem domain (mental map) into the code, describing it in a way that permits to restore it back. By reading a code your coworker or you 6 month later should be able to restore the same mental map you had while writing the code. And using type system to describe properties (there is another way to do it already in place – fields in structs), seems like complicating this task and it eventually should hurt readability.
- almostdeadguy 8y ago
  The advantage is you basically don't have to think about the provenance of data (in this example what state is a connection in? was it closed before being given to me? etc.). It allows the compiler to ensure the user of this code can't perform operations that lead to error states by allowing the programmer to express the state transitions of a connection in their function declarations, as the provided example shows: newConnection :: Address -> Connection Closed openConnection :: Connection Closed -> Connection Open closeConnection :: Connection Open -> Connection Closed connectionAddress :: Connection s -> Address From a readability perspective, I would love this, it's effectively a state machine diagram explained by your function types.
- thedufer 8y ago
  Statically enforcing behavior helps the human as well - in this example, it would make it more clear what types of things you can do with an open connection vs a closed one just by inspecting the types, whereas otherwise you would have to either find documentation or test it and see. We use type tricks like this (although not exactly in this way, as we don't really have a concept of kinds) in OCaml, and we find that in practice people new to the language aren't actually confused by it much - it actually makes readability better, not worse.

lmm 8y ago

> When we promote `Open` and `Closed` from terms to types, we make it easy to create a variable that can be either `Open` or `Closed`, but we're also breaking the mental model of the whole thing. `Open`/`Closed` is a property – not a "type" in a traditional way of thinking about types. For me, the type should map onto some abstraction in your mental world map, and `Open`/`Closed` is definitely not a good fit here. I don't think I follow? Something open is different from something closed; the construction of an open thing is different from the construction of a closed thing. The operations you can do on them are different. They're different varieties of thing, they should have different types. Edit: is your point that you wouldn't ever have a term that's just Open or Closed, only a Connection[Open] or Connection[Closed]? I guess that's true but it doesn't seem important. If you're comfortable with parameterised types at all then you're already comfortable with types that aren't directly applied to terms - e.g. you'll never have a term that's a List, only a term that's a List[Int] or what have you.

divan 8y ago
> Something open is different from something closed Right, but that's just a property of "something", not a type of it. When someone asks you "What type of door you have?" we don't say "I have an open door", rather "I've a timber door" or "glass door". This is how we understand the world after all, and to me type system should reflect our mental and cognitive processes. > If you're comfortable with parameterised types at all I think I have the same issue with parametrized types as well. Having `Vector<int>` is good for compiler, but not necessarily for humans. When you need to put a beads onto the string (the closest real-world analogy I came up with vector, haha), you don't think "hey, I need to find a string of type "beads" and then put beads onto it". You just take a string, and it implicitly "works" for beads. If you try to put something weird (why would you, btw?) onto it, you'll break the whole thing or it just didn't work. I'm not implying that we need to do everything as in offline world, but at least try to minimize discrepancies in the reasoning about the world in the code.
- lmm 8y ago
  > Right, but that's just a property of "something", not a type of it. When someone asks you "What type of door you have?" we don't say "I have an open door", rather "I've a timber door" or "glass door". I think that's just because a given door can change between open and closed and be the same door? We're used to persistent global state and monotonic wall-clock time, but those are bad for programming and we should take the trouble to cast off those intuitions. > I think I have the same issue with parametrized types as well. Having `Vector<int>` is good for compiler, but not necessarily for humans. When you need to put a beads onto the string (the closest real-world analogy I came up with vector, haha), you don't think "hey, I need to find a string of type "beads" and then put beads onto it". You just take a string, and it implicitly "works" for beads. The point isn't that the string itself has a type, it's that a string of beads is a different kind of thing from a string of charms or a string of lights (at least, to the extent that a bead is a different kind of thing from a charm or a light). And you can't have a "string of" on its own - it's always a string of something - but there are things that it makes sense to do to a string of things without regard to the specific type of thing that's on it (e.g. count how many items are on it). Any kind of abstract concept has that issue. You can't ever get just "a square" in the real world - you can get a square of wood or a square of plastic or a square of cake, but it'll always be a square of something. Or you can't get "three" on its own - you can only ever get three of something. If we ask what type of thing you're sitting on, maybe it's a wheeled chair or a three-legged stool, and those types make sense even though it wouldn't make sense to say that you're sitting on "a wheeled" or "a three-legged".

Fellshard 8y ago

Domain modeling is fungible. In most cases, I'd expect it to be a property. In some cases, it could be it's better represented as separate types, especially if it makes both domain and software logic simpler to reason about and change.