Re: more closed-world chatter

On May 7, 12:34 am, David BL <davi...@xxxxxxxxxxxx> wrote:
On May 7, 1:56 pm, Jon Heggland <jon.heggl...@xxxxxxxxxxx> 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

.

Relevant Pages

  • Re: more closed-world chatter
    ... I note that Marshall neglected constraints on the element type in his ... order to avoid an infinite regress. ...
    (comp.databases.theory)
  • Re: Countable models of ZFC
    ... Alan Smaill wrote: ... Why would refusing to single out a set (which is uniquely defined ... anyway as we agree) avoid an infinite regress, ...
    (sci.logic)