There is a programming language in which types are sets (of values) and that is
designed all on this interpretation (even though integer values are primitive
and not encoded as you suggest).
The language is CDuce where, besides basic function and product types, you
have also (set-theoretic) union, intersection and negation type connectives. You
can try it here http://www.cduce.org. It is also included in all major linux
distributions.
If you are more interested at the theory rather than the implementation,
then I suggest to start with the paper "A gentle introduction on semantic
subtyping" and then move to the reference paper "Semantic subtyping" published
in the Journal of the ACM. Polymorphism is then done in a ICFP 2011 paper and in
a forthcoming POPL 2014 paper.
The type system nicely fits Perl6 (really nicely!). I am currently writing a
primer on how adapt these types and they algorithms and data structures to Perl6
... but do not hold your breath. If you are interested please do not hesitate to
ask more information.
Beppe
P.S. For what concerns homotopy type theory, it tries to overcome some
limitation of set-theory, that is, if I understood correctly just the contrary
of what you intend to do
On 18/11/13 00:33, raiph mellor wrote:
On Sun, Nov 17, 2013 at 5:43 PM, Andrew Suffield <asuffi...@suffields.me.uk
<mailto:asuffi...@suffields.me.uk>> wrote:
While mathematics as a field has mostly settled on set theory as its basis,
type theory is equally expressive and is usually preferred in language
design.
Aiui there is now optimism in some circles that the set theory foundation will
be replaced by a "homotopical interpretation of type theory".
I have about zero understanding of what this stuff is or if it will have any
impact on programming language type systems, but thought I'd speak up. :)
--
raiph
