0
$\begingroup$

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$.

Definition of list using product

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?

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ how is the first one implied? $\endgroup$ – OlympicComputerChairSitter Jul 21 '18 at 16:53
  • $\begingroup$ It is "any element e and any list l" that is implicit to the following conditions, which are explained. The "first one" isn't implicit, it's stated clearly that it's !=l . $\endgroup$ – Rob Jul 21 '18 at 17:39
  • $\begingroup$ I don't see where it's stated.... $\endgroup$ – OlympicComputerChairSitter Jul 21 '18 at 18:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.