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} = {∅, {∅}, {∅, {∅}}}
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 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).
