On 2013 Nov 17, at 17:10, Darren Duncan wrote:
I recall reading that at least in certain math/logic papers that a programming language type system can be defined logically in terms of pure sets, making it essentially self-defined without needing to rely on external definitions of for example what a number is. In such 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 can recurse arbitrarily such that all leaves are the empty set. In such a system, you could for example represent the number zero by {}, the number 1 by {{}}, 2 by {{{}}} or something else, etc. I'm not saying that such a type system would be practical to implement in a manner resembling this, but more that it is simply a logical basis for 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} = {∅, {∅}, {∅, {∅}}}

(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 string values 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).

Reply via email to