Context: I am trying to formalize the definition of a polynomial ring in a programming language. One way to think about it, is to start by formulating the definition of a ring extension by adjoining elements. In my programming formulation, I created a type for rings, and a type for variables. I am working from the following definition for polynomial rings: Let $R$ be a ring and $x$ be a variable. $R[x]$ is a polynomial ring. That is, the smallest ring that contains both $R$ and $x$.
My question: What is the type for the 'adjoin' operator? My guess is $[\ ]: \mbox{Ring} \times \mbox{Variable} \rightarrow \mbox{Ring}$ (I'm just concerned with the type, not the semantics). Also, what is this called (a function that takes a ring and produces a ring)? Because I can use any properties of such operator (e.g. identity laws, associativity, etc.) in my program and do some reasoning.
Note: These are possibly the wrong tags.