type systems and #f and '() 
Author Message
 type systems and #f and '()

I think #f and '() are disjoint, but Tom Lord is one of the people that
taught me Scheme in the first place, so I decided to think through the
consequences of not distinguishing between #f and '() to see if there
was more to it than I was aware of.

One of the functions of a type system is to help guarantee logical
consistency. It's not important that types be disjoint. Subtyping allows
for one type to be passed in place of another. What is important is that
type systems not allow for any circularities in any subtyping graph.

An integer can (in theory) be used anywhere a real number is expected,
but not vice versa. The integer type is a subtype of the real type.

Let's consider the possibility that either #f and '() are completely
identical values, or that one may be a subtype of the other.

Case 1: #f and '() are indistinguishable. This would make '()/#f
effectively a subtype of both the boolean type and the list type. Since
we have an implicit cast to #t of every value except #f/'(), we can
safely use a list (either a pair or null) any place a bool was expected.

On the other hand, we can't safely pass a bool any place a list is
expected--which is as it should be. Strangely we can pass a specific
subtype of bool (i.e. #f) in place of a list. Expecting this to work
makes it inappropriate to consider passing a bool as a list a statically
checkable type error. And the benefit of allowing it is unclear. (I
suspect there is no benefit. This case is equivalent to allowing a real
to be passed as an integer on the slight chance that it actually is an
integer. Of course Scheme doesn't statically type check anything anyway,
so maybe this point is moot except with regard to external type checkers
and optimizers.)

Case 2: '() is a subtype of #f--that is, a '() can be used anywhere a #f
is expected, but not vice versa. This would map well with the idea that
every value other than #f and '() was a subtype of the value #t. I'm not
sure this is so bad. It would allow for

        (if '() 'not-finished 'finished) => 'finished

kind of constructs. However:

        (eq? '() #f) => #f

If you don't think this is ugly, then I don't think (if '() #t #f) => #f
is ugly. (At least no uglier than an implicit cast to #t of every other
value (which I do consider ugly, but it's the Scheme way).) I would be
curious to know how much--if any--of code that depends on the
disjointedness of '() and #f would still work in this system.

(Don't get me wrong. If I was on a religious crusade to 'fix' Scheme,
I'd complain about things like the fact that '+' doesn't take a fixed
number of (i.e. two) arguments. I'd use fold to do what '+' does now.
But when I start getting those kinds of feelings, I just switch to SML.)

-thant



Tue, 23 Mar 2004 02:44:27 GMT  
 type systems and #f and '()

Quote:

>Case 2: '() is a subtype of #f--that is, a '() can be used anywhere a #f
>is expected, but not vice versa. This would map well with the idea that
>every value other than #f and '() was a subtype of the value #t. I'm not
>sure this is so bad. It would allow for

> (if '() 'not-finished 'finished) => 'finished

>kind of constructs. However:

> (eq? '() #f) => #f

>If you don't think this is ugly, then I don't think (if '() #t #f) => #f
>is ugly. (At least no uglier than an implicit cast to #t of every other
>value (which I do consider ugly, but it's the Scheme way).) I would be
>curious to know how much--if any--of code that depends on the
>disjointedness of '() and #f would still work in this system.

I've suggested something which I think is quite similar in its effects
(although it apparently qualifies as "ugly" in your book, which I don't
necessarily disagree with):

Retain (eq? '() #f) => #f, but use the implicit casting mechanism you
mentioned to implicitly cast '() to #f and all other values to #t, only in
certain contexts, specifically in control structures.  I'm not sure how
something like that would be viewed from the type-theory perspective.  The
fact that a conversion between two types is possible, and done automatically
in certain contexts, doesn't seem to require that the behavior of the
underlying type system be changed.  It seems to me that this could be
achieved as a sort of optional behavior of the control structures.

My suggestion might be less pervasive than your subtyping solution, since it
could be set up to only affect control structures which were designed to
work this way; other uses of '() and #f could be treated as completely
distinct.  This might not be sufficiently pervasive to achieve Tom's goals,
I'm not sure.

Quote:
>(Don't get me wrong. If I was on a religious crusade to 'fix' Scheme, ...

I, too, am not seriously arguing that anything like this should be done, and
I quite strongly believe in '() <> #f (especially since I haven't seen any
solid arguments to the contrary).  But I was interested to separate out some
of the component issues in the question.  Your subtyping approach does that,
too, and also seems preferable to simply saying '() == #f.

Quote:
> But when I start getting those kinds of feelings, I just switch to SML.

Yeah, yeah.  ML is just waiting around for Scheme to come up with the next
big breakthrough so it can statically type it and act all theoretically pure
about it...   :P

Anton



Tue, 23 Mar 2004 06:35:31 GMT  
 type systems and #f and '()

[...]

Quote:
> My suggestion might be less pervasive than your subtyping
> solution, since it could be set up to only affect control
> structures which were designed to work this way; other
> uses of '() and #f could be treated as completely
> distinct.  [...]

I think that in practice, with regard to Scheme, your proposal and mine
are identical. The only way mine would have additional consequences is
if you could declare the argument types of your own functions, or build
your own types.

-thant



Tue, 23 Mar 2004 23:28:33 GMT  
 type systems and #f and '()

Quote:
> Retain (eq? '() #f) => #f, but use the implicit casting mechanism you
> mentioned to implicitly cast '() to #f and all other values to #t, only in
> certain contexts, specifically in control structures.  I'm not sure how
> something like that would be viewed from the type-theory perspective.  

Badly. Since every function returns something (whether specified or
implementation defined, or not), casting '() to #f and everything else to #t
means any expression can be used in a control structure, even functions that
are only used for their side effects.

By forcing the boolean type to be distinct, accidental misuse of expressions
in control structures is prevented. If you want it in a control structure,
then explicitly say so by ensuring the expression is a boolean one, no
surprises.

Safety, provability, correctness, etc., is enhanced if implicit conversions
are avoided, generally speaking.

What I would like to see some discussion about is whether or not '() is an
empty list or nothing at all. I.e. can it also be used to denote "no
hashtable" or "no record" or "no vector", etc.?

If so, then I would like to see the reinstatement of nil as a keyword that
denotes this idea, since '() seems too list-specific for the general case. Of
course, I could always do a (define nil '()) somewhere myself, I suppose.

--
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,



Wed, 24 Mar 2004 01:04:03 GMT  
 type systems and #f and '()

Quote:

> Anton>I'm not sure how
> Anton>something like that would be viewed from the type-theory
perspective.

>Badly. Since every function returns something (whether specified or
>implementation defined, or not), casting '() to #f and everything else to
#t
>means any expression can be used in a control structure, even functions
that
>are only used for their side effects.

Which is pretty much what Scheme does now.  I wasn't saying that I think
this is good, but rather that a minor change to Scheme's existing casting
behavior could achieve what I think Tom wants, without losing the ability to
distinguish '() from '#f.

My question about the type theoretic view of this was intended more along
the lines of whether this change would have broader implications for
Scheme's existing type system - but it seems to me that it wouldn't.

Quote:
>By forcing the boolean type to be distinct, accidental misuse of
expressions
>in control structures is prevented. If you want it in a control structure,
>then explicitly say so by ensuring the expression is a boolean one, no
>surprises.

I have no problem with that.  A "Strict Scheme" specification which
eliminated fuzzy items like this one would be fine with me.  Perhaps it
would be easier to reach consensus on Strict Scheme than on a larger R6RS,
since the goals would be clearer...

Quote:
>What I would like to see some discussion about is whether or not '() is an
>empty list or nothing at all.

That's an easy one, going back to R2RS at least: '() is an empty list, by
definition.

Also by definition, it is not nothing at all.  If it were nothing at all, it
wouldn't be a list.

Quote:
>I.e. can it also be used to denote "no
>hashtable" or "no record" or "no vector", etc.?

Of course Scheme doesn't stop you from doing this (as it might do if it were
statically typed).  But isn't the use of '() for these purposes a somewhat
arbitrary implementation decision?  I say "somewhat" because use of '() is,
of course, quite convenient and tempting - no other Scheme value suits the
purpose quite so well.

Quote:
>If so, then I would like to see the reinstatement of nil as a keyword that
>denotes this idea, since '() seems too list-specific for the general case.

I think that list-specificness was the intent.  Scheme has no value which
represents no value - isn't that nice and consistent?  I would think "Strict
Scheme" would want to inherit this feature.

But I have a variation on the same question: is it "fair" for Scheme to
provide a special, distinguished, magic value like '(), needed in the
context of lists, but then to implicitly discourage its use, or the creation
of other such values, in other cases?

Quote:
> Of course, I could always do a (define nil '()) somewhere myself, I

suppose.

Isn't it better to do exactly this, if you need or want to, because it
recognizes that the value associated with nil is just an implementation
detail?  After all, you could also use: (define nil '(this is not a value)).
You're giving meaning to the symbol nil, but what its value is doesn't
really matter, as long as it doesn't conflict with other values in the
domain in which it is used.

Anton



Wed, 24 Mar 2004 05:41:33 GMT  
 type systems and #f and '()

Quote:

> > Of course, I could always do a (define nil '()) somewhere myself, I
> > suppose.

> Isn't it better to do exactly this, if you need or want to, because it
> recognizes that the value associated with nil is just an implementation
> detail?  After all, you could also use: (define nil '(this is not a value)).
> You're giving meaning to the symbol nil, but what its value is doesn't
> really matter, as long as it doesn't conflict with other values in the
> domain in which it is used.

I guess what I am after is a universal "bottom" value. '() as a particular
example I don't really care about, since using a list-looking item for non-list
purposes just rubs the wrong way, even ignoring type correctness
considerations.

Given that Scheme is dynamically typed, a bottom value seems like a useful
thing (i.e. this variable contains "nothing at all"). Calling it nil comes to
mind because of standard practice in other languages and lisp history.

--
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,



Fri, 26 Mar 2004 15:54:20 GMT  
 type systems and #f and '()

Quote:

> >What I would like to see some discussion about is whether or not '() is an
> >empty list or nothing at all.

> That's an easy one, going back to R2RS at least: '() is an empty list, by
> definition.

> Also by definition, it is not nothing at all.  If it were nothing at all, it
> wouldn't be a list.

And in fact R5RS 7.2 defines an entity #unspecified which is more
correctly interpreted as 'nothing at all'. Unfortunately, that value
is neither denotable nor testable, although it *is* expressible [via
(if #f #f)]. This is very high on my 'fix it' list for R6RS.

Quote:
> >I.e. can it also be used to denote "no
> >hashtable" or "no record" or "no vector", etc.?

Not really, but it depends on what you mean by those phrases. If you
mean uninitialized value which is bound to a name, then it can work as
Anton points out:

Quote:
> Of course Scheme doesn't stop you from doing this...[it] is,
> of course, quite convenient and tempting - no other Scheme value suits the
> purpose quite so well.

And that is because is is a 'bottom'-ish sort of value. It is the
denegenerate base case of the most common recursive type in
Scheme. IMO, the real debate should be about the validity of lists as
a primitive type [which I brought up in another recent post]. Vectors,
SRFI-9 [or other] records, and #unspecified are pretty much all that
is needed for building anything.

Quote:
> >If so, then I would like to see the reinstatement of nil as a keyword that
> >denotes this idea, since '() seems too list-specific for the general case.

I would be pretty happy with that, too.

Quote:
> I think that list-specificness was the intent.  Scheme has no value which
> represents no value - isn't that nice and consistent?  I would think "Strict
> Scheme" would want to inherit this feature.

nonononononono. Scheme has a value which is *in fact*
unspecified. There are just no operations defined on that value. This
is bad, from Tom's lambda mysticism POV. Scheme operations are not
total on the type lattice either because of the under-specification of
error mechanisms. All of this needs fixed.

Quote:
> But I have a variation on the same question: is it "fair" for Scheme to
> provide a special, distinguished, magic value like '(), needed in the
> context of lists, but then to implicitly discourage its use, or the creation
> of other such values, in other cases?

No. But I'm already advocating that lists get chucked out of R6RS [SACRILEGE!].

Quote:
> You're giving meaning to the symbol nil, but what its value is doesn't
> really matter, as long as it doesn't conflict with other values in the
> domain in which it is used.

Which is why I think that reifiying #unspecified is a good idea. Then
you have a true bottom in the type [and value] lattice. #unspecified
*can't* conflict with values in any domain, by definition.

david rush
--
There's man all over for you, blaming on his boots the faults of his feet.
        -- Samuel Becket (Waiting For Godot)



Fri, 26 Mar 2004 17:46:43 GMT  
 type systems and #f and '()

Quote:



> > > Of course, I could always do a (define nil '()) somewhere myself, I
> > > suppose.

> > Isn't it better to do exactly this, if you need or want to, because it
> > recognizes that the value associated with nil is just an implementation
> > detail?  After all, you could also use: (define nil '(this is not a value)).
> > You're giving meaning to the symbol nil, but what its value is doesn't
> > really matter, as long as it doesn't conflict with other values in the
> > domain in which it is used.

> I guess what I am after is a universal "bottom" value. '() as a particular
> example I don't really care about, since using a list-looking item for non-list
> purposes just rubs the wrong way, even ignoring type correctness
> considerations.

`Bottom' is usually considered the `result' of a non-terminating
program, not a general `null' value.


Sat, 27 Mar 2004 22:10:42 GMT  
 type systems and #f and '()

Quote:

> `Bottom' is usually considered the `result' of a non-terminating
> program, not a general `null' value.

Ok. What do you call a value that belongs to all types in the hierarchy? Isn't
that also the "bottom" of the implied partially ordered set?

--
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,



Sun, 28 Mar 2004 00:11:30 GMT  
 type systems and #f and '()

Quote:


>>`Bottom' is usually considered the `result' of a non-terminating
>>program, not a general `null' value.

> Ok. What do you call a value that belongs to all types
> in the hierarchy? Isn't that also the "bottom" of the
> implied partially ordered set?

I thought "bottom" was the type to which no value belongs, and "top" was
the type to which every value belongs.

-thant



Sun, 28 Mar 2004 00:36:42 GMT  
 type systems and #f and '()

Quote:

> Anton> Scheme has no value which
> Anton> represents no value - isn't that nice and consistent?  I would
> Anton> think "Strict Scheme" would want to inherit this feature.

>nonononononono. Scheme has a value which is *in fact*
>unspecified. There are just no operations defined on that value.

Thanks for pointing this out.

Quote:
>But I'm already advocating that lists get chucked out of R6RS [SACRILEGE!].

This sounds like another case for a "strict" version of the spec, which
would not necessarily be R6RS.  R6RS might then be expressed as a superset
of the strict spec, e.g. with lists/pairs described in terms of records.

Quote:
>Which is why I think that reifiying #unspecified is a good idea. Then
>you have a true bottom in the type [and value] lattice. #unspecified
>*can't* conflict with values in any domain, by definition.

Are there any good technical reasons for having left this out of the spec?

I notice that real Scheme implementations (e.g. mzscheme, Scheme48, SCM)
support this well enough:

    (define nil (if #f #f))

creates a "value" which can be assigned, compared etc.  Is anything more
needed in these implementations, other than a name for this "value"?  What
more is required in the spec?

Anton



Sun, 28 Mar 2004 00:48:30 GMT  
 type systems and #f and '()


Quote:
>nonononononono. Scheme has a value which is *in fact*
>unspecified. There are just no operations defined on that value.

No it doesn't.  R5RS says:

  If the value of an expression is said to be ``unspecified,'' then the
  expression must evaluate to some object without signalling an error, but
  the value depends on the implementation; this report explicitly does not
  say what value should be returned.

"Unspecified" is a concept, not a specific value.  Different functions with
unspecified return values could return different values, and a single
function could return different values at different times.  For instance,
the statement that the result of a set! expression is unspecified doesn't
preclude it from always returning the value that it stored, like Common
Lisp's SETQ; it just means that a portable program may not *depend* on
this.

Some *implementations* have a unique object that they use for unspecified
return values, for the benefit of the top-level evaluator, so that it can
avoid printing out the value of expression.

Perhaps in R6RS these situations could be defined to return (values).  This
would make it an error to use an expression with an unspecified return
value as an parameter in a function call, the source of an assignment or
let-binding, etc.  However, this would break programs that make use of
implementation-specific behavior (such programs may be intentionally
non-portable).

--

Genuity, Woburn, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.



Sun, 28 Mar 2004 01:08:22 GMT  
 type systems and #f and '()

Quote:
> I notice that real Scheme implementations (e.g. mzscheme, Scheme48, SCM)
> support this well enough:

>     (define nil (if #f #f))

> creates a "value" which can be assigned, compared etc.  Is anything more
> needed in these implementations, other than a name for this "value"?  What
> more is required in the spec?

In UMB Scheme on my linux box, this gives nil a value of '(), which is
probably not what is wanted if '() is to be used for lists only.

--
Cheers,                                        The Rhythm is around me,
                                               The Rhythm has control.
Ray Blaak                                      The Rhythm is inside me,



Sun, 28 Mar 2004 01:28:34 GMT  
 type systems and #f and '()

Quote:

> Some *implementations* have a unique object that they use for unspecified
> return values, for the benefit of the top-level evaluator, so that it can
> avoid printing out the value of expression.

That's right.  As a side note, for the non-benefit of those who try to
emulate a top-level evaluator, (display (if #f #f)) outputs "#<void>"
(or "#!void", etc.).  That's good behavior for (write (if #f #f)), but
I'd much prefer that display output "".

My apologies if I've missed an implementation that does it the way I'd
like.



Sun, 28 Mar 2004 01:36:26 GMT  
 type systems and #f and '()

Quote:


>> Some *implementations* have a unique object that they use for unspecified
>> return values, for the benefit of the top-level evaluator, so that it can
>> avoid printing out the value of expression.

>That's right.  As a side note, for the non-benefit of those who try to
>emulate a top-level evaluator, (display (if #f #f)) outputs "#<void>"
>(or "#!void", etc.).  That's good behavior for (write (if #f #f)), but
>I'd much prefer that display output "".

If it did that, the output of

(let ((unspec (if #f #f)))
  (display (list unspec unspec)))

would be "( )", which doesn't seem desirable to me.

--

Genuity, Woburn, MA
*** DON'T SEND TECHNICAL QUESTIONS DIRECTLY TO ME, post them to newsgroups.
Please DON'T copy followups to me -- I'll assume it wasn't posted to the group.



Sun, 28 Mar 2004 01:41:45 GMT  
 
 [ 111 post ]  Go to page: [1] [2] [3] [4] [5] [6] [7] [8]

 Relevant Pages 

1. Difference between a type system and a type constraint system

2. Difference between a type system and a type constraint system

3. Miranda's Type System

4. Biff's-own-guide to type systems?

5. An Attempt to Formalise Dylan's Type System (Part 2)

6. An Attempt to Formalise Dylan's Type System (Part 1)

7. Dylan's type system

8. Dylan's type system

9. Visual Prolog's type system

10. Papers/Info on Type Systems/Type Theory ?

11. Types-SIG: Special Interest Group on the Python type system

12. Types-SIG: Special Interest Group on the Python type system

 

 
Powered by phpBB® Forum Software