5 ms·
It's nice when you can use common, general language to talk between languages. I made a joke about Java finally getting 'structs' [1] and was told that records
by mrkeen 2y ago
It's nice when you can use common, general language to talk between languages.
I made a joke about Java finally getting 'structs' [1] and was told that records weren't structs. I don't think I would have gotten the same pushback if I just called them product types instead.
> It's the overload of concepts that makes it harder to grasp.
Have you come across the OR-PLUS similarity in predicate logic, as well as AND-MULTIPLY? Those ones help me think about logic even though they don't have anything to do with each other. It helps me parse their precedence in my mind, and think about their commutativity/distributivity quickly, e.g.
P ∧ (Q ∨ R)
could be expanded to
P ∧ Q ∨ P ∧ R
which is the same as
(P ∧ Q) ∨ (P ∧ R)
> Sums and products are operations in muggle math (functions)
Anyway, these ones refer to adding up their state spaces (number of possible inhabitants). A sum type can have this inhabitant (TRUE) or [2] that inhabitant (FALSE). A product type can have this type (e.g. first element in a tuple) and [3] that type (second element in a tuple). And since you mentioned "functions" - those are exponential types!
[1] https://docs.oracle.com/en/java/javase/17/language/records.html
[2] Oh, there's that "or" again lol!
[3] "and !
- taeric 2y agoWhat makes records not structs? Seems a fair statement.
- fjuwnsd 2y agoBecause most devs don't think from type theory principles. They see the keyword "struct" and associate it to C# struct which is stack allocated. Then they see the keyword "record" and think Java record which is syntax sugar for class which is heap allocated. They never draw the connection that they are both ways to express product types.
- ndriscoll 2y agoWhether something is boxed or not is relevant in practice for performance. It's reasonable to have a jargon where products, records, and structs are distinct concepts.
- taeric 2y agoI still don't necessarily follow. I would expect them to be structs in the LISP DEFSTRUCT sense. Outside of somewhat fringe reasons, caring about allocation style is something I'd imagine most people just don't do?
- js8 2y agoActually, sum type would be more analogous to XOR in Boolean logic.
- abeppu 2y agoI think it lines up with OR in the sense that x:(S+T) <==> x:S OR x:T If you know x:S you may find conclude x:(S+T) without also stipulating that x is not a T. It may be permitted (if pointless) to use S+T even in contexts where S is a subtype of T (and hence the XOR is not true).
- ndriscoll 2y agoOR and XOR are both "wrong". It's a disjoint union. T+T = 2T, not T or 0. When S and T are disjoint, then it's OR-like (and also XOR-like). You can't conclude x: S+T from x:S (because it's false). What you can do is use x to build an S+T. If S=T there are two ways to do that. From what I've seen, usually subtyping is also defined via embeddings, and if x: T then x: S is false for all S != T by definition.