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

Clash Royale CLAN TAG#URR8PPP

up vote
0
down vote

favorite

1

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 $Etimes 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?

math-software visualization type-theory data-structure

share|cite|improve this question

edited Jul 21 at 3:47

asked Jul 21 at 3:07

EnjoysMath

8,63642154

add a comment | 

up vote
0
down vote

favorite

1

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 $Etimes 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?

math-software visualization type-theory data-structure

share|cite|improve this question

edited Jul 21 at 3:47

asked Jul 21 at 3:07

EnjoysMath

8,63642154

add a comment | 

up vote
0
down vote

favorite

1

up vote
0
down vote

favorite

1

1

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 $Etimes 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?

math-software visualization type-theory data-structure

share|cite|improve this question

edited Jul 21 at 3:47

asked Jul 21 at 3:07

EnjoysMath

8,63642154

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 $Etimes 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?

math-software visualization type-theory data-structure

share|cite|improve this question

edited Jul 21 at 3:47

asked Jul 21 at 3:07

EnjoysMath

8,63642154

share|cite|improve this question

share|cite|improve this question

edited Jul 21 at 3:47

edited Jul 21 at 3:47

edited Jul 21 at 3:47

asked Jul 21 at 3:07

EnjoysMath

8,63642154

asked Jul 21 at 3:07

EnjoysMath

8,63642154

asked Jul 21 at 3:07

EnjoysMath

8,63642154

8,63642154

add a comment | 

add a comment | 

1 Answer
1

active

oldest

votes

up vote
1
down vote



accepted

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.

share|cite|improve this answer

answered Jul 21 at 5:55

Rob

346112

• 
  
  
  

  
  

  
  
  
  
  
  

  
  how is the first one implied?
  – EnjoysMath
  Jul 21 at 16:53
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  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 .
  – Rob
  Jul 21 at 17:39
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I don't see where it's stated....
  – EnjoysMath
  Jul 21 at 18:00
  

  
  
  
  

add a comment | 

Your Answer

StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "69"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
convertImagesToLinks: true,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2858209%2fwould-this-suffice-in-a-visual-type-theory-to-define-an-abstract-list-type%23new-answer', 'question_page');

);

Post as a guest

Name Email

1 Answer
1

active

oldest

votes

1 Answer
1

active

oldest

votes

active

oldest

votes

active

oldest

votes

up vote
1
down vote



accepted

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.

share|cite|improve this answer

answered Jul 21 at 5:55

Rob

346112

• 
  
  
  

  
  

  
  
  
  
  
  

  
  how is the first one implied?
  – EnjoysMath
  Jul 21 at 16:53
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  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 .
  – Rob
  Jul 21 at 17:39
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I don't see where it's stated....
  – EnjoysMath
  Jul 21 at 18:00
  

  
  
  
  

add a comment | 

up vote
1
down vote



accepted

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.

share|cite|improve this answer

answered Jul 21 at 5:55

Rob

346112

• 
  
  
  

  
  

  
  
  
  
  
  

  
  how is the first one implied?
  – EnjoysMath
  Jul 21 at 16:53
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  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 .
  – Rob
  Jul 21 at 17:39
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I don't see where it's stated....
  – EnjoysMath
  Jul 21 at 18:00
  

  
  
  
  

add a comment | 

up vote
1
down vote



accepted

up vote
1
down vote



accepted

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.

share|cite|improve this answer

answered Jul 21 at 5:55

Rob

346112

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.

share|cite|improve this answer

answered Jul 21 at 5:55

Rob

346112

share|cite|improve this answer

share|cite|improve this answer

answered Jul 21 at 5:55

Rob

346112

answered Jul 21 at 5:55

Rob

346112

answered Jul 21 at 5:55

Rob

346112

346112

• 
  
  
  

  
  

  
  
  
  
  
  

  
  how is the first one implied?
  – EnjoysMath
  Jul 21 at 16:53
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  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 .
  – Rob
  Jul 21 at 17:39
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I don't see where it's stated....
  – EnjoysMath
  Jul 21 at 18:00
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  

  
  
  
  
  
  

  
  how is the first one implied?
  – EnjoysMath
  Jul 21 at 16:53
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  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 .
  – Rob
  Jul 21 at 17:39
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  I don't see where it's stated....
  – EnjoysMath
  Jul 21 at 18:00
  

  
  
  
  

how is the first one implied?
– EnjoysMath
Jul 21 at 16:53

how is the first one implied?
– EnjoysMath
Jul 21 at 16:53

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 .
– Rob
Jul 21 at 17:39

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 .
– Rob
Jul 21 at 17:39

I don't see where it's stated....
– EnjoysMath
Jul 21 at 18:00

I don't see where it's stated....
– EnjoysMath
Jul 21 at 18:00

add a comment | 

 

draft saved

draft discarded

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2858209%2fwould-this-suffice-in-a-visual-type-theory-to-define-an-abstract-list-type%23new-answer', 'question_page');

);

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Name Email

Name

Email

Name Email

Name

Email