This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||||
|
I propose merging this page with Recursive data type, which even says in its lead that recursive types are also known as inductive types. siddharthist ( talk) 00:20, 18 January 2018 (UTC)
In the example with natural numbers and lists encoded as W-types, the text suggests that f(12) = 0 is "representing the constructor for zero, which takes no arguments". The constructor for zero is , where is any function (here assumed to be polymorphic). It is difficult to see how f(12) could represent this constructor.
Similarly, the successor function is encoded by , where is defined by .
I propose moving the examples to after the introduction of and updating the examples accordingly.
This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | ||||||||||||||||||||||||||||
|
I propose merging this page with Recursive data type, which even says in its lead that recursive types are also known as inductive types. siddharthist ( talk) 00:20, 18 January 2018 (UTC)
In the example with natural numbers and lists encoded as W-types, the text suggests that f(12) = 0 is "representing the constructor for zero, which takes no arguments". The constructor for zero is , where is any function (here assumed to be polymorphic). It is difficult to see how f(12) could represent this constructor.
Similarly, the successor function is encoded by , where is defined by .
I propose moving the examples to after the introduction of and updating the examples accordingly.