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 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.


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 <
<>> 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 

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. :)


Reply via email to