1

I am trying to figure out how types and variables can work together to represent something in the real world but i am getting stuck. This is how i'm trying to define variables that have normal mathematical types at the moment.

Let F be an Integer that represents the force on a ball" (Here I'm saying that F is an integer, and that F represents the force on a ball.)

But when I try to introduce types and sets i'm getting stuck, for example if I try to define a new type called Card Suit.

"Let the type Card Suit be a set {1...4}" where 1 represents Diamonds, 2 represents Hearts, 3 represents Spades and 4 represents Clubs."

Then if I introduce a variable with that type the logic starts getting funny for example

"Let S be of type Card Suit that represents a Card Suit".

In the end i end up duplicating what i'm saying, doesn't "let S be of type Card Suit" makes the next phrase "... that represents a Card Suit" redundant?

Can anyone help get my logic unstuck here, thanks.

Richard Bamford
  • 111

1 Answers1

2

This is because you use the same name for the type, and for what it represents.

You could say "Let S be of type CardSuit that represents a card suit", distinguishing by typography the name and the kind of objects. That would look less redundant.
But in the end, if you name the type with what it represents, you do not need to add "... that represents ...".

What makes your question particularly interesting, is that some programming languages actually allow to distinguish between a numerical type, and a "business" type (as it is sometimes called), which is an added layer. This in order to say that, for example, NbEmployees and NbTasks are both positive or null integers, but it is not allowed to assign a value of one type to a variable of the other type.
Something similar happens with physical units, a little more complex because units can be multiplied between themselves.

Jean-Armand Moroni
  • 5,632
  • As a mathematical example of a "business" type: when defining an opposite category, instead of saying the objects are precisely the same in $C^{op}$ as in $C$, I prefer to think of the object type of $C^{op}$ as a wrapper type around the object type of $C$, and similarly for the Hom types of $C^{op}$. i.e. $\operatorname{Obj}(C^{op}) := { X^{op} \mid X : \operatorname{Obj}(C) }$ and $\operatorname{Hom}_{C^{op}}(X^{op}, Y^{op}) := { f^{op} \mid f : \operatorname{Hom}_C(Y, X) }$. – Daniel Schepler Sep 12 '23 at 17:15
  • That makes it easier to keep track of what compositions you're talking about, for example in the definition of composition you say that for $f : \operatorname{Hom}(Y^{op}, Z^{op}), g : \operatorname{Hom}(X^{op}, Y^{op})$, then $f = f_0^{op}$ for some unique $f_0 : \operatorname{Hom}(Z, Y)$ and $g = g_0^{op}$ for some unique $g_0 : \operatorname{Hom}(Y, X)$, and you deifne $f \circ g = f_0^{op} \circ g_0^{op} := (g_0 \circ f_0)^{op}$. – Daniel Schepler Sep 12 '23 at 17:20
  • Does it not matter if we introduce types like "CardSuit" into our equations, shouldn't we only be used types defined in maths like sets, functions.etc? – Richard Bamford Sep 14 '23 at 18:32
  • 1
    @RichardBamford There are type theories in mathematics. Cf. https://math.stackexchange.com/questions/431482/type-theory-as-foundations or (more difficult) https://ncatlab.org/nlab/show/type+theory. Whether we want to use them or not is a matter of choice. Types mostly appear on works on foundations and logic; but such theories are used for example by proof assistants (Coq, Agda...), which in turn may be used for verifying proofs of less foundational theorems. Math type theories also influence some programming languages, although not the mainstream ones. – Jean-Armand Moroni Sep 14 '23 at 21:22