On 2013 Nov 17, at 17:10, Darren Duncan wrote:

I recall reading that at least in certain math/logic papers that aprogramming language type system can be defined logically in termsof pure sets, making it essentially self-defined without needing torely on external definitions of for example what a number is. Insuch a type system, every value is a generic set of 0..N elements,and the value of every element is also such a generic set, which canrecurse arbitrarily such that all leaves are the empty set. In sucha system, you could for example represent the number zero by {}, thenumber 1 by {{}}, 2 by {{{}}} or something else, etc. I'm notsaying that such a type system would be practical to implement in amanner resembling this, but more that it is simply a logical basisfor defining a closed system at the most fundamental level.

`This is how axiomatic set theory (the most common foundation for`

`mathematics) works. The most common way to encode natural numbers is`

`as von Neumann ordinals, where each natural is the set of all previous`

`naturals:`

0 = {} = ∅ 1 = {0} = {∅} 2 = {0, 1} = {∅, {∅}} 3 = {0, 1, 2} = {∅, {∅}, {∅, {∅}}} etc.

`(The 2 = {{∅}} variant has been studied and has a name, but I can't`

`recall it, and it's not that popular anyway.)`

`Ordered pairs usually use the Kuratowski definition: (a,b) := {{a},`

`{a,b}}; if sets are also prohibited from containing themselves and`

`cannot form infinitely-descending hierachies, this can be simplified`

`slightly as {a, {a,b}}. A function is then a set of ordered pairs in`

`which the first element of each pair is an input and the second`

`element is the corresponding output. A list/array/sequence can then`

`be defined as a function whose domain is all naturals from 0 through`

`some n (i.e., the set n+1).`

`After this, you can define all integers and rationals as equivalence`

`classes of pairs of naturals/integers where each pair of numbers in a`

`given class has the same difference/ratio. After that, reals can be`

`defined in terms of either Dedekind cuts or Cauchy sequences, and`

`complex numbers are then pairs of reals. For more information, look`

`up any of these terms on Wikipedia.`

Does Haskell at least conceptually work in terms like I described?I seem to recall reading that how it logically thinks about stringvalues is towards that direction.

`It does not. Strings in Haskell are just lists of Chars, and lists`

`are Lisp-like pairs of elements and sublists (which you could`

`implement in set theory as an alternative to sequences, but I don't`

`know if anyone does that).`