Re: more closed-world chatter

On May 7, 12:34 am, David BL <davi..._at_iinet.net.au> wrote:
> On May 7, 1:56 pm, Jon Heggland <jon.heggl..._at_idi.ntnu.no> wrote:
>
> > David BL wrote:
> > > Consider these two types
>
> > > T1 = int
> > > T2 = { 1,5,17,22,105 }
>
> > > I have the feeling it's not such a good idea to treat these in the
> > > same way. Otherwise what does it mean to distinguish between type and
> > > value? I would rather call T2 a value than a type, and keep the type
> > > system simple.
>
> > What criterion do you use to decide between "type" and "value"? Isn't T1
> > as much a set of values (and thus a value) as T2? Consider T1 = byte and
> > T2 = { -128, -127, ..., -1, 0, 1, ... , 126, 127 } ...
>
> The distinction is based on whether a proposed type will in fact tend
> to be treated as a value at run time, and manipulated as such. I
> agree this is rather vague.
>
> My concern is that if types can be manipulated as values at run time,
> then we have the means to solve complex problems using just the type
> system. In that case why make a distinction between types and values?

Why indeed?

The type theory world is busy struggling with this question, and the concern you mention above, which some people consider a virtue. Oh, I guess I'm one of those people, by the way.

Why not have a Turing complete type system?

The usual answer is that it means that type checking may not halt. In fact, all the troubles of runtime are then added to compile time. However I believe this may not be such a big issue as it might seem.

If you are ever looking for some crazy wild reading in this area, allow me to recommend any written work by Conor McBride, (see: http://e-pig.org/). Not what I'm looking for, but tremendously interesting all the same. A working knowledge of Haskell is probably necessary.

> If every user-defined type must in turn have its own type constraints
> then we need some basic, atomic, system provided types to avoid an
> infinite regress.
>
> I note that Marshall neglected constraints on the element type in his
> definition of pricedomain:
>
> def pricedomain = set {1, 2};
>
> ie Marshall possibly suggests an approach where typing is optional in
> order to avoid an infinite regress. I expect he would instead prefer
> the introduction of some system provided types.

As an aside, there are type systems out there with an infinite hierarchy
of values, types, types of types, types of types of types, etc. It solves Girard's paradox, but it's a bit too much frosting and not enough cake for my taste.

Marshall Received on Mon May 07 2007 - 18:48:45 CEST