Would this suffice in a visual type theory to define an abstract List type?

Question

See the image. I got that from: wikipedia article. In that, I don't understand the first function nil : () -> L. What is ()?

I want to make a visual type theory so that we aren't stuck comprehending pure text for eternity.

Also, is the abstract type List a product of some sort? The diagram doesn't indicate this since it's based on a product diagram of $E \times L$.

Assume that product has already been defined by a similar diagram and that there is a system that can interpret these smallish diagrams, so that ideally $E\times L$ and $p_L$ as well as the graphical arrows and blocks show up in a different color indicating that you cannot edit them.

Additionally in the wikipedia article, they say:

for any element e and any list l. It is implicit that

cons (e, l) ≠ l
cons (e, l) ≠ e
cons (e1, l1) = cons (e2, l2) if e1 = e2 and l1 = l2
Note that first (nil ()) and rest (nil ()) are not defined.

But isn't the last one already true!?? How should I indicate the first two in diagram form?

Answer 1

Q: I don't understand the first function nil: () → L. What is ()?

It is an atom, written as an abstract data type. The List is created and initialized as empty, using the atom. In Lisp: Set an atom to NIL and initialize the list with that atom.

nil: () → L

That creates an empty list. It's like: char *L = (char *)malloc(0);

See: What's the point in malloc(0)?.

Q: Also, is the abstract type List a product of some sort?

It's a list, see link above for "list".

Q: But isn't the last one already true!??

It says:

for any element e and any list l. It is implicit that

cons (e, l) ≠ l
cons (e, l) ≠ e
cons (e1, l1) = cons (e2, l2) if e1 = e2 and l1 = l2

It's implicit.

Q: How should I indicate the first two in diagram form?

CONS takes its first argument [which may be either an atom or a list] and inserts it just after the first left parenthesis in the second argument. This second argument should be a list. CONS will actually connect things onto atoms as: "(cons 'a 'b)", but this creates a special form of list called a dotted pair.