User-defined Types

[Shriram Krishnamurthi <address@hidden>]

Herchenroeder, Thomas wrote:

> I think this is a wonderful solution, giving you maximum power to specify
> what your types should be like, in a generic and elegant manner.

This is an ancient idea called predicate typing.  While very powerful,
it also rapidly becomes undecidable.  It sounds like the language you
used gave up on static checking entirely.

Types are coarse approximations.  They are *not meant* to exactly
mirror the run-time set of values.  Indeed, they derive their very
power by making this compromise.  Most of the value of type systems is
that they are *static* -- it seems confusing at best to call a purely
dynamic system a "type" system.  Of course, only an unreasonable
person would deny that you want a dynamic checking system to
complement the static one, and to perform more powerful checks.

In practice, it proves a lot easier to define static checks that work
by partitions, and a lot more powerful for the dynamic checks to work
by predicates.  Some static checking of predicates is possible, but
also very, very hard (and tough to get to a useful point in the
expressiveness/safety trade-off, as decades of work has shown).

Shriram