`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