3 ms·

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

by 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".
uryga 8y ago
> 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 like analogies, but I don't think bringing the real world into this helps – irl, "is a" relationships are pretty fuzzy and arbitrary. What does it mean for something to "be" a door? If I'm using a window as a door, does it become a door? "Being a door" is just another property. And if I have a door and start chopping away pieces of it, at what point does it stop being a door? "things" often don't have well defined boundaries, so even the notion of "objects" becomes meaningless. (see also: Ship of Theseus). A lot of it is up to a person's perception too... So in general, I think it's better to keep the real world separate from formal/mathematical concepts. --- Encoding some "properties" in the type system is a tool for ensuring (some degree of) correctness. Sometimes, a property is important enough that you want to put it in a type variable, as in `data Connection (status :: ConnectionStatus)`. But if you'd prefer your properties to be "disconnected" from the actual type, you might enjoy dependently typed languages[1] like Idris, where you can have statically enforced "proofs" that a value has some property. In such a system, a function `readData` could take a `Connection` and a proof that the connection is open. It'd look something like this: readData : (conn: Connection) -> IsOpen conn -> Bytes Note that the proof, `IsOpen conn`, refers to the value of the first argument. How do we obtain those proofs is up to the connection library. For example, `openConnection` could return a connection along with a proof that the connection is open: openConnection : Address -> ((conn: Connection), IsOpen conn) The library could also supply a "smart predicate" function that gives you proofs of a connection's status: status : (conn: Connection) -> Either (IsOpen conn) (IsClosed conn) Take this with a grain of salt though – I haven't actually used Idris, just read a few tutorials.

by divan 8y ago

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

uryga 8y ago

> 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 like analogies, but I don't think bringing the real world into this helps – irl, "is a" relationships are pretty fuzzy and arbitrary. What does it mean for something to "be" a door? If I'm using a window as a door, does it become a door? "Being a door" is just another property. And if I have a door and start chopping away pieces of it, at what point does it stop being a door? "things" often don't have well defined boundaries, so even the notion of "objects" becomes meaningless. (see also: Ship of Theseus). A lot of it is up to a person's perception too... So in general, I think it's better to keep the real world separate from formal/mathematical concepts. --- Encoding some "properties" in the type system is a tool for ensuring (some degree of) correctness. Sometimes, a property is important enough that you want to put it in a type variable, as in `data Connection (status :: ConnectionStatus)`. But if you'd prefer your properties to be "disconnected" from the actual type, you might enjoy dependently typed languages[1] like Idris, where you can have statically enforced "proofs" that a value has some property. In such a system, a function `readData` could take a `Connection` and a proof that the connection is open. It'd look something like this: readData : (conn: Connection) -> IsOpen conn -> Bytes Note that the proof, `IsOpen conn`, refers to the value of the first argument. How do we obtain those proofs is up to the connection library. For example, `openConnection` could return a connection along with a proof that the connection is open: openConnection : Address -> ((conn: Connection), IsOpen conn) The library could also supply a "smart predicate" function that gives you proofs of a connection's status: status : (conn: Connection) -> Either (IsOpen conn) (IsClosed conn) Take this with a grain of salt though – I haven't actually used Idris, just read a few tutorials.