<p>First of all, I think that there is nothing wrong with your current definition and I think it can be understood by any mathematician. However, if you still want it to look nicer, I can give you a few hints:</p>

<p>Firstly, you might have a look at a few papers that introduce intuitionistic type theory. There, the set of possible proofs for a disjunctive type $A \vee B$ is the <a href="http://en.wikipedia.org/wiki/Disjoint_union" rel="nofollow">disjoint union</a> of all possible proofs for $A$ and all possible proofs for $B$. For example, if you look at <a href="http://www.csie.ntu.edu.tw/~b94087/ITT.pdf" rel="nofollow">this paper by Martin-Lof</a>, on page 7 (page 13 of the pdf file), you see that it uses $i(a)$ and $j(a)$ to mark whether $a$ is a proof of $A$ or a proof of $B$. You can do the same and use notation $a(d)$ and $b(d)$ to denote $\mathcal{A}~Data$ or $\mathcal{B}~Data$.</p>

<p>The second way and, to me, the more elegant way is to use different notations. For example, your definition of $Data$ would look something like this:</p>

<p>$Data$ is the minimal set that contains $\mathbb{N}$ and is closed under the $[.]$ and $\langle .\rangle$ containers, i.e., if $d \in Data$ then so are $[d]$ and $\langle d \rangle$. This way, a function $f : Data \mapsto A$ can be defined by defining it over $\mathbb{N}$ as well as $f([d])$ and $f(\langle d \rangle)$ (for $d \in Data$).</p>

<p>As you can see, this is not very different from your own way as I mentioned in the beginning. The only difference, to me, is the aesthetics. My version just seems cleaner and less like programming (I would also change the name $Data$ in the thesis explanation to a one-letter name to make it even cleaner).</p>

CC BY-SA 3.0
2013-06-06T12:19:39.720Z
Thanks for you suggestions, this kind of discussion is exactly what I am looking for.
Lii
CC BY-SA 3.0
2013-06-06T12:20:35.850Z
"Firstly...": Interesting alternative! (I find the discussion on disjoint unions on page 29 of Lööf's paper) I'll spend some more time thinking about this.
Lii
CC BY-SA 3.0
2013-06-06T12:22:22.390Z
"The second way..." Interesting alternative! This looks equivalent to you first suggestion, except that you another kind of notation. Is this correct? I like the idea of using named functions more. I think this is the way I should do it.
Lii
CC BY-SA 3.0
2013-06-07T05:24:44.373Z
Yes, both ways are essentially equivalent. I like the second way more just because it is cleaner and you don't have to describe what name functions $i(.)$ and $j(.)$ do.
Shahab
CC BY-SA 3.0
2013-06-11T09:04:13.710Z
Having given this some thought I have some considerations:

Alt 1: It is a bit confusing to use functions without actually caring what kind of objects they signify. I'll have to explain this to the reader, and say things like $b(d) \neq c(d)$.

Alt 2: I would have to explain what this notation really means. Is $\langle . \rangle$ some kind of function? Then it's just different notion for Alt 1. Or is it notation for some special kind of object? This would have to be explained.
Lii
CC BY-SA 3.0
2013-06-11T09:10:16.233Z
I'll accept this answer because it contributes the most to my understanding. But I thank all of you for your valuable suggestions!
Lii
CC BY-SA 3.0
2013-06-06T09:38:38.500Z
2013-06-06T09:38:38.500Z
Shahab
<p>You should get acquainted with <em>inductive definitions</em>.</p>

<p>Instead of saying that $Data$ is recursively defined, say that it is a set constructed <em>inductively</em> by:</p>

<ul>
<li>$(0,i) \in Data$ for every $i \in \mathbb{Z}$,</li>
<li>$(1,d) \in Data$ for every $d \in Data$,</li>
<li>$(2,d) \in Data$ for every $d \in Data$.</li>
</ul>

<p>Another way to say the same thing is that $Data$ is the smallest set such that
$$Data = \lbrace (0,i) \mid i \in \mathbb{Z} \rbrace \cup
\lbrace (1,d) \mid d \in Data \rbrace \cup
\lbrace (2,d) \mid d \in Data \rbrace.$$
Then remark that you use abbreviations $\mathcal{A} = 0$, $\mathcal{B} = 1$, $\mathcal{C} = 2$. Mathematicians are not used to introduction of basic symbols or tags, unless they are considering polynomials in a "variable" $X$ (which they really should call "symbol").</p>

<p>But it may be better not to cater to old-fashioned traditions of mathematicians. We should push them into the 21st century and teach them some math which they think of as "computer science". What is wrong with assuming your reader knows what an inductive data type is?</p>

<p>One word of warning: Haskell does <em>not</em> have inductive datatypes, but rather <em>coindcutive</em> data types. If you define the type in Haskell you will also get infinite elements of the form <code>B (B (C (B ....)))</code>. There is just no way to get this right in Haskell. ML has proper datatypes.</p>

CC BY-SA 3.0
2013-06-06T11:03:18.517Z
I was expecting the phrase "Initial Algebra".
Dave Clarke
CC BY-SA 3.0
2013-06-06T11:48:16.823Z
Mathematicians are freaked out by anything that is an algebra but doesn't have an associative operation, at the very least. It's safer to say "set". Anyways, why are we even talking about mathematicians?
Andrej Bauer
CC BY-SA 3.0
2013-06-06T11:49:58.403Z
Mathematicians get jobs as computer scientists. True story.
Dave Clarke
CC BY-SA 3.0
2013-06-06T12:23:35.647Z
Thanks for your reply. Maybe the correct term is "inductive set" instead of "recursive set". But apart from that, and a few style things, our definitions are basically the same, are they not? About the $\mathcal{A, B, C} things: If I used numbers instead it will get much harder to read because numbers don't suggest the meaning of the element (my "tag" element in the thesis does). Is there some other way to "tag" the elements that is both descriptive and conventional?
Lii
CC BY-SA 3.0
2013-06-06T12:35:15.657Z
@DaveClarke: Excuse me, are you trying to contribute to the discussion? I don't understand what you want to say.
Lii
CC BY-SA 3.0
2013-06-06T12:41:17.577Z
Data types in universal algebra are represented using "initial algebras".
Dave Clarke
CC BY-SA 3.0
2013-06-06T12:44:37.080Z
@Lii: yes, our formulations are essentially the same. You can use tags, just make sure you explain them and say that they could be "anything, for example numbers or symbols", but you chose descriptive ones. "Recursive set" in logic means "a set whose membership can be tested by a computable function", which is not what you want. The correct term is indeed "inductive set".
Andrej Bauer
CC BY-SA 3.0
2013-06-06T14:21:27.807Z
@DaveClarke: If I am going with named tags, do you think $\mathcal{A, B, C}$ a reasonable choice of writing them? Or is there a more conventional way?
Lii
CC BY-SA 3.0
2013-06-06T14:38:05.940Z
I would use $\mathtt{A}, \mathtt{B}, \mathtt{C}$, or actually words, like $\mathtt{Fruit}$, $\mathtt{Veggie}$. This is another obsession of mathematicians' -- they'd rather use exocit alphabets than a name consisting of more than one letter.
Andrej Bauer
CC BY-SA 3.0
2013-06-06T16:08:57.900Z
@Lii, Dave Clarke was making what some of us call a joke, a datatype which can be purchased at the expense of mathematicians. Some of these are only funny to an audience of size $O(1)$.
Vijay D
CC BY-SA 3.0
2013-06-06T16:27:21.487Z
Ah, I see! I much appreciate the existence of field internal jokes even when I don't get them myself.
Lii
CC BY-SA 3.0
2013-06-07T08:48:35.480Z
@VijayD: I don't see how "Initial Algebras" is a joke.
Dave Clarke
CC BY-SA 3.0
2013-06-07T08:55:47.820Z
@DaveClarke  If you are joking, I'm lost. I assumed Lii was referring to your comment about mathematicians getting jobs. Apropos that: http://cdn2-www.craveonline.com/assets/uploads/2013/02/file_205239_2_multiple-choice-theoretical-mathmatics.jpg
Vijay D
CC BY-SA 3.0
2013-06-06T10:47:40.013Z
2013-06-06T10:47:40.013Z
Andrej Bauer
<p>I have an algorithm written in Haskell which I am describing in my thesis. In the code for the algorithm I have a recursive data type similar to this:</p>

<blockquote>
  <p>data Data = A Int | B Data | C Data</p>
</blockquote>

<p>Now I am thinking about how to explain this in a formal way, in a way that feels natural and clear. Note that <code>B</code> and <code>C</code> contain the same data.</p>

<p>The only reasonable alternative I have come up with is to use some kind of tagged union, like this:</p>

<p>Let $Data$ be a recursively defined set given by:</p>

<ul>
<li>Let $i$ be an integer. Then $\langle \mathcal{A}, i \rangle \in Data$.</li>
<li>Let $d \in Data$. Then $\langle \mathcal{B}, d \rangle \in Data$.</li>
<li>Let $d \in Data$. Then $\langle \mathcal{C}, d \rangle \in Data$.</li>
</ul>

<p>With this definition I write functions over $Data$ like this:</p>

<p>$$
func(\langle \mathcal{A}, i \rangle) = \cdots \\
func(\langle \mathcal{B}, d \rangle) = \cdots \\
func(\langle \mathcal{C}, d \rangle) = \cdots \\
$$</p>

<p>And predicated about is like this:
$$
Pred(\langle \mathcal{A}, i \rangle) \text{ holds if ... } \\
Pred(\langle \mathcal{B}, d \rangle) \text{ holds if ... } \\
Pred(\langle \mathcal{C}, d \rangle) \text{ holds if ... } \\
$$</p>

<p>This representation is very close to the Haskell source code, which is good, but it feels rather unnatural to mathematicians.</p>

<p>Is there a more elegant and natural way to do this?</p>

<p><strong>EDIT:</strong>
Thanks for the replays, sorry if I am being unclear.</p>

<p>I am writing a master's thesis in CS about alias analysis. The text should be comprehensible for students on master level in CS with a background in algorithms (does master level mean the same in the USA? In EU you get this degree after 5 years of study including an 1 term thesis project).</p>

<p>I have used <a href="http://suif.stanford.edu/~jwhaley/papers/MIT-LCS-TR-795.pdf" rel="nofollow noreferrer">this paper</a> as a starting point, implemented that algorithm in Haskell and made some extensions. Now I want to describe my extension in a way that is similar to the paper in formulation and level of formalism. However I use a recursive algebraic data type in my extension and I'm not sure about the most natural and clear way to represent it.</p>

<p><strong>EDIT</strong>: The example $Data$ above is intended to have finite values only. </p>

<p><strong>EDIT:</strong>
I see that my question is very similar to this: <a href="https://cstheory.stackexchange.com/questions/12331/formal-representation-of-haskell-data-types?rq=1">Formal Representation of Haskell Data-Types</a></p>

<p>Except that I'm also interested in how to represent recursive data types.</p>

<p><strong>EDIT: Summary of the alternative suggestions I have received</strong></p>

<ol>
<li><p>Tagged tuples (my example above and  Andrej Bauer's alternative)</p></li>
<li><p>Function applications (Shahab's first alternative)
$$
  data(a(d)) = \dots
$$</p></li>
<li><p>Objects with special notation / operators (Shahab's second alternative)
$$
  \langle d \rangle = \dots
$$</p></li>
<li><p>Un-data-type-ization (yatima2975's alternative)</p>

<p>Transform into non-recursive form. Works only for data types with one recursive element.
"the Cartesian product of finite strings over {B,C} and the integers"</p></li>
</ol>

<p>I think all of the have advantages and disadvantages.</p>

CC BY-SA 3.0
2013-06-05T11:32:29.430Z
When you say "in logic" I thnink you mean "in set theory", or more likely "in informal mathematics". That is, is it correct that you are asking how to formulate your datatype so that ordinary mathematicians who do not speak Haskell will understand it?
Andrej Bauer
CC BY-SA 3.0
2013-06-05T11:59:15.340Z
Yes, that is correct. I have to describe the algorithm so that non-programers can understand it in a more or less formal way using ordinary notation for functions and relations. I don't have to use sets to represent data structures but I don't don't come up with any better way of doing it.
Lii
CC BY-SA 3.0
2013-06-05T12:08:58.687Z
Whether or not one should call this "in logic" or "in informal mathematics" is an interesting question in its own right which I don't know to answer to. I should clearly no call it "in set theory", and "in mathematics" doesn't sound right to me either, but maybe I'm wrong. I'm under the impression that it's reasonable to use the phrase "in logic" to mean a description using rather informal first-order logic.
Lii
CC BY-SA 3.0
2013-06-05T21:25:41.517Z
I agree with Andrej. You will be confusing people by calling what you are looking for as "in logic".
Kaveh
CC BY-SA 3.0
2013-06-05T21:27:18.820Z
You want a nice mathematical space of objects satisfying the equation $D \equiv Int + 2\times D$?
Kaveh
CC BY-SA 3.0
2013-06-05T22:07:04.437Z
@lii could you explain the degree for which you are writing the thesis, your background, and the expected audience for your thesis.  It seem to me you want to explain or formalise your work in mathematical terms. That is not the same as explaining your work to working, professional mathematicians. What is your goal?
Vijay D
CC BY-SA 3.0
2013-06-06T00:26:51.170Z
@VijayD, I have made an edit to the question, you may want to also check [the original version](http://cstheory.stackexchange.com/posts/17906/revisions).
Kaveh
CC BY-SA 3.0
2013-06-06T00:41:31.883Z
@Kaveh, thanks for clarifying. I think the use of "mathematicians" here is not good because I assumed it was for working mathematicians. I think the OP is asking a very basic question about mathematical semantics.
Vijay D
CC BY-SA 3.0
2013-06-06T00:42:48.810Z
@Lii, Dave Clarke's answer here http://cstheory.stackexchange.com/a/16128/4155 might help you with the mathematics of inductive definitions.
Vijay D
CC BY-SA 3.0
2013-06-06T09:52:43.090Z
Do you care about infinite structures (such as `let x = B y; y = C x in x`) and undefined values? If not, you can just use a description like 'the Cartesian product of finite strings over `{B,C}` and the integers modulo (at least) 2^30'.
yatima2975
CC BY-SA 3.0
2013-06-06T12:17:50.150Z
@Kaveh: Yes, I think so, although I'm not entirely sure I understand this notation (a variant type of an int and two D's?). I also think this formulation is too type theoretic for my intended readers (and me).
Lii
CC BY-SA 3.0
2013-06-06T12:18:08.947Z
@yatima2975: No, I'm interested only in finite, non-undefined $Data$s. I made an edit. Interesting suggestion. I don't think it is better then what I have right now but it's an interesting possibility. It feels more "mathy".
Lii
CC BY-SA 3.0
2013-06-06T12:18:53.797Z
About the "...in logic" <-> "...in mathematics" <-> "...to mathematicians" question: I'm apparently confused about the meaning of the term "logic". I intended to use the phrase "in logic" as "in the formal language of connectives, functions and predicates". I think maybe "Formal representation of recursive ADTs" would be a better title. Out of curiosity, would "...in predicate logic" or "...using predicate logic" be an acceptable title?
Lii
<pl.programming-languages><functional-programming><semantics>
Formal representation of algorithm using recursive algebraic data types
Lii
# Formal representation of algorithm using recursive algebraic data types

(Asked by: username_0 on 2013-06-05)

I have an algorithm written in Haskell which I am describing in my thesis. In the code for the algorithm I have a recursive data type similar to this:

> data Data = A Int | B Data | C Data

Now I am thinking about how to explain this in a formal way, in a way that feels natural and clear. Note that `B` and `C` contain the same data.

The only reasonable alternative I have come up with is to use some kind of tagged union, like this:

Let $Data$ be a recursively defined set given by:

* Let $i$ be an integer. Then $\langle \mathcal{A}, i \rangle \in Data$.
* Let $d \in Data$. Then $\langle \mathcal{B}, d \rangle \in Data$.
* Let $d \in Data$. Then $\langle \mathcal{C}, d \rangle \in Data$.

With this definition I write functions over $Data$ like this:

$$
func(\langle \mathcal{A}, i \rangle) = \cdots \\
func(\langle \mathcal{B}, d \rangle) = \cdots \\
func(\langle \mathcal{C}, d \rangle) = \cdots \\
$$

And predicated about is like this:
$$
Pred(\langle \mathcal{A}, i \rangle) \text{ holds if ... } \\
Pred(\langle \mathcal{B}, d \rangle) \text{ holds if ... } \\
Pred(\langle \mathcal{C}, d \rangle) \text{ holds if ... } \\
$$

This representation is very close to the Haskell source code, which is good, but it feels rather unnatural to mathematicians.

Is there a more elegant and natural way to do this?

**EDIT:**
Thanks for the replays, sorry if I am being unclear.

I am writing a master's thesis in CS about alias analysis. The text should be comprehensible for students on master level in CS with a background in algorithms (does master level mean the same in the USA? In EU you get this degree after 5 years of study including an 1 term thesis project).

I have used [this paper](http://suif.stanford.edu/~jwhaley/papers/MIT-LCS-TR-795.pdf) as a starting point, implemented that algorithm in Haskell and made some extensions. Now I want to describe my extension in a way that is similar to the paper in formulation and level of formalism. However I use a recursive algebraic data type in my extension and I'm not sure about the most natural and clear way to represent it.

**EDIT**: The example $Data$ above is intended to have finite values only.

**EDIT:**
I see that my question is very similar to this: [Formal Representation of Haskell Data-Types](https://cstheory.stackexchange.com/questions/12331/formal-representation-of-haskell-data-types?rq=1)

Except that I'm also interested in how to represent recursive data types.

**EDIT: Summary of the alternative suggestions I have received**

1. Tagged tuples (my example above and username_1's alternative)
2. Function applications (username_5's first alternative)
   $$
   data(a(d)) = \dots
   $$
3. Objects with special notation / operators (username_5's second alternative)
   $$
   \langle d \rangle = \dots
   $$
4. Un-data-type-ization (username_4's alternative)

   Transform into non-recursive form. Works only for data types with one recursive element.
   "the Cartesian product of finite strings over {B,C} and the integers"

I think all of the have advantages and disadvantages.

**Tags:** pl.programming-languages, functional-programming, semantics

> **Comments:**
> **username_1**: When you say "in logic" I thnink you mean "in set theory", or more likely "in informal mathematics". That is, is it correct that you are asking how to formulate your datatype so that ordinary mathematicians who do not speak Haskell will understand it?  
> **username_0**: Yes, that is correct. I have to describe the algorithm so that non-programers can understand it in a more or less formal way using ordinary notation for functions and relations. I don't have to use sets to represent data structures but I don't don't come up with any better way of doing it.  
> **username_0**: Whether or not one should call this "in logic" or "in informal mathematics" is an interesting question in its own right which I don't know to answer to. I should clearly no call it "in set theory", and "in mathematics" doesn't sound right to me either, but maybe I'm wrong. I'm under the impression that it's reasonable to use the phrase "in logic" to mean a description using rather informal first-order logic.  
> **username_2**: I agree with Andrej. You will be confusing people by calling what you are looking for as "in logic".  
> **username_2**: You want a nice mathematical space of objects satisfying the equation $D \equiv Int + 2\times D$?  
> **username_3**: @lii could you explain the degree for which you are writing the thesis, your background, and the expected audience for your thesis.  It seem to me you want to explain or formalise your work in mathematical terms. That is not the same as explaining your work to working, professional mathematicians. What is your goal?  
> **username_2**: @VijayD, I have made an edit to the question, you may want to also check [the original version](http://cstheory.stackexchange.com/posts/17906/revisions).  
> **username_3**: @username_2, thanks for clarifying. I think the use of "mathematicians" here is not good because I assumed it was for working mathematicians. I think the OP is asking a very basic question about mathematical semantics.  
> **username_3**: @username_0, username_6's answer here http://cstheory.stackexchange.com/a/16128/4155 might help you with the mathematics of inductive definitions.  
> **username_4**: Do you care about infinite structures (such as `let x = B y; y = C x in x`) and undefined values? If not, you can just use a description like 'the Cartesian product of finite strings over `{B,C}` and the integers modulo (at least) 2^30'.  
> **username_0**: @username_2: Yes, I think so, although I'm not entirely sure I understand this notation (a variant type of an int and two D's?). I also think this formulation is too type theoretic for my intended readers (and me).  
> **username_0**: @username_4: No, I'm interested only in finite, non-undefined $Data$s. I made an edit. Interesting suggestion. I don't think it is better then what I have right now but it's an interesting possibility. It feels more "mathy".  
> **username_0**: About the "...in logic" <-> "...in mathematics" <-> "...to mathematicians" question: I'm apparently confused about the meaning of the term "logic". I intended to use the phrase "in logic" as "in the formal language of connectives, functions and predicates". I think maybe "Formal representation of recursive ADTs" would be a better title. Out of curiosity, would "...in predicate logic" or "...using predicate logic" be an acceptable title?  

---

## 2 answers

### Answer by username_5 on 2013-06-06. Score: 4 | Accepted answer

First of all, I think that there is nothing wrong with your current definition and I think it can be understood by any mathematician. However, if you still want it to look nicer, I can give you a few hints:

Firstly, you might have a look at a few papers that introduce intuitionistic type theory. There, the set of possible proofs for a disjunctive type $A \vee B$ is the [disjoint union](http://en.wikipedia.org/wiki/Disjoint_union) of all possible proofs for $A$ and all possible proofs for $B$. For example, if you look at [this paper by Martin-Lof](http://www.csie.ntu.edu.tw/~b94087/ITT.pdf), on page 7 (page 13 of the pdf file), you see that it uses $i(a)$ and $j(a)$ to mark whether $a$ is a proof of $A$ or a proof of $B$. You can do the same and use notation $a(d)$ and $b(d)$ to denote $\mathcal{A}~Data$ or $\mathcal{B}~Data$.

The second way and, to me, the more elegant way is to use different notations. For example, your definition of $Data$ would look something like this:

$Data$ is the minimal set that contains $\mathbb{N}$ and is closed under the $[.]$ and $\langle .\rangle$ containers, i.e., if $d \in Data$ then so are $[d]$ and $\langle d \rangle$. This way, a function $f : Data \mapsto A$ can be defined by defining it over $\mathbb{N}$ as well as $f([d])$ and $f(\langle d \rangle)$ (for $d \in Data$).

As you can see, this is not very different from your own way as I mentioned in the beginning. The only difference, to me, is the aesthetics. My version just seems cleaner and less like programming (I would also change the name $Data$ in the thesis explanation to a one-letter name to make it even cleaner).

> **Comments:**
> **username_0**: Thanks for you suggestions, this kind of discussion is exactly what I am looking for.  
> **username_0**: "Firstly...": Interesting alternative! (I find the discussion on disjoint unions on page 29 of Lööf's paper) I'll spend some more time thinking about this.  
> **username_0**: "The second way..." Interesting alternative! This looks equivalent to you first suggestion, except that you another kind of notation. Is this correct? I like the idea of using named functions more. I think this is the way I should do it.  
> **username_5**: Yes, both ways are essentially equivalent. I like the second way more just because it is cleaner and you don't have to describe what name functions $i(.)$ and $j(.)$ do.  
> **username_0**: Having given this some thought I have some considerations:  Alt 1: It is a bit confusing to use functions without actually caring what kind of objects they signify. I'll have to explain this to the reader, and say things like $b(d) \neq c(d)$.  Alt 2: I would have to explain what this notation really means. Is $\langle . \rangle$ some kind of function? Then it's just different notion for Alt 1. Or is it notation for some special kind of object? This would have to be explained.  
> **username_0**: I'll accept this answer because it contributes the most to my understanding. But I thank all of you for your valuable suggestions!  

---

### Answer by username_1 on 2013-06-06. Score: 7

You should get acquainted with *inductive definitions*.

Instead of saying that $Data$ is recursively defined, say that it is a set constructed *inductively* by:

* $(0,i) \in Data$ for every $i \in \mathbb{Z}$,
* $(1,d) \in Data$ for every $d \in Data$,
* $(2,d) \in Data$ for every $d \in Data$.

Another way to say the same thing is that $Data$ is the smallest set such that
$$Data = \lbrace (0,i) \mid i \in \mathbb{Z} \rbrace \cup
\lbrace (1,d) \mid d \in Data \rbrace \cup
\lbrace (2,d) \mid d \in Data \rbrace.$$
Then remark that you use abbreviations $\mathcal{A} = 0$, $\mathcal{B} = 1$, $\mathcal{C} = 2$. Mathematicians are not used to introduction of basic symbols or tags, unless they are considering polynomials in a "variable" $X$ (which they really should call "symbol").

But it may be better not to cater to old-fashioned traditions of mathematicians. We should push them into the 21st century and teach them some math which they think of as "computer science". What is wrong with assuming your reader knows what an inductive data type is?

One word of warning: Haskell does *not* have inductive datatypes, but rather *coindcutive* data types. If you define the type in Haskell you will also get infinite elements of the form `B (B (C (B ....)))`. There is just no way to get this right in Haskell. ML has proper datatypes.

> **Comments:**
> **username_6**: I was expecting the phrase "Initial Algebra".  
> **username_1**: Mathematicians are freaked out by anything that is an algebra but doesn't have an associative operation, at the very least. It's safer to say "set". Anyways, why are we even talking about mathematicians?  
> **username_6**: Mathematicians get jobs as computer scientists. True story.  
> **username_0**: Thanks for your reply. Maybe the correct term is "inductive set" instead of "recursive set". But apart from that, and a few style things, our definitions are basically the same, are they not? About the $\mathcal{A, B, C} things: If I used numbers instead it will get much harder to read because numbers don't suggest the meaning of the element (my "tag" element in the thesis does). Is there some other way to "tag" the elements that is both descriptive and conventional?  
> **username_0**: @DaveClarke: Excuse me, are you trying to contribute to the discussion? I don't understand what you want to say.  
> **username_6**: Data types in universal algebra are represented using "initial algebras".  
> **username_1**: @username_0: yes, our formulations are essentially the same. You can use tags, just make sure you explain them and say that they could be "anything, for example numbers or symbols", but you chose descriptive ones. "Recursive set" in logic means "a set whose membership can be tested by a computable function", which is not what you want. The correct term is indeed "inductive set".  
> **username_0**: @DaveClarke: If I am going with named tags, do you think $\mathcal{A, B, C}$ a reasonable choice of writing them? Or is there a more conventional way?  
> **username_1**: I would use $\mathtt{A}, \mathtt{B}, \mathtt{C}$, or actually words, like $\mathtt{Fruit}$, $\mathtt{Veggie}$. This is another obsession of mathematicians' -- they'd rather use exocit alphabets than a name consisting of more than one letter.  
> **username_3**: @username_0, username_6 was making what some of us call a joke, a datatype which can be purchased at the expense of mathematicians. Some of these are only funny to an audience of size $O(1)$.  
> **username_0**: Ah, I see! I much appreciate the existence of field internal jokes even when I don't get them myself.  
> **username_6**: @VijayD: I don't see how "Initial Algebras" is a joke.  
> **username_3**: @DaveClarke  If you are joking, I'm lost. I assumed username_0 was referring to your comment about mathematicians getting jobs. Apropos that: http://cdn2-www.craveonline.com/assets/uploads/2013/02/file_205239_2_multiple-choice-theoretical-mathmatics.jpg  

---

