[lnkForumImage]
TotalShareware - Download Free Software

Confronta i prezzi di migliaia di prodotti.
Asp Forum
 Home | Login | Register | Search 


 

Forums >

comp.lang.lisp

semantics of subtypes of function types vs typed lambda calculus.

Jim Newton

3/17/2016 3:37:00 PM

Can someone please help me understand the semantics of function types
in Common Lisp. Are they somehow backwards from other functional
languages? Are the backward from arrow types in typed lambda
calculus?

I've checked in both sbcl, cmucl and climb. clisp returns NIL,NIL for
both but sbcl and cmucl both behave the same.

(subtypep '(function (integer) number)
'(function (number) number))
returns T,T,
while

(subtypep '(function (number) number)
'(function (integer) number))
returns NIL,T.

This seems set-theoretically wrong to me. And in fact it seems to
violate the typing rule of the typed lambda calculus presented by
Pierce in Types and Programming Languages (TAPL).
http://www.cis.upenn.edu/~bcpi... .

(Notation: In TAPL, Pierce uses "<:" to mean "is a subtype of" and
"->" to indicate function types.)

Any function which expects an object of type Tsuper will also accept
Tsub. E.g., a function which expects a number will of course accept an
integer because integer <: number.

But any function which accepts a Tsub->X will also accept a Tsuper->X.
In particular if F expects an argument of type integer->string, F will
also implicitly accept an argument of type number->string. Why,
because since F expects an integer->string, F will only call the
function with an integer, and a number->string can certainly be called
with an integer. This would lead me to agree with TAPL that
number->string <: integer->string -- the opposite of what subtypep
claims.

TAPL claims (chapter 15, section 15.2.1, page 184) that
If T1 <: S1 and S2 <: T2,
then S1->S2 <: T1->T2

Intutively this means that if you restrict the domain, you get a
larger type, but if you restrict the range you get a smaller type.

Take as an example: T1=integer, S1=number, S2=T2=string

Since integer <: number and string <: string,
then number->string <: integer->string (According to TAPL)

But integer->string <: number->string (According to subtypep)

Let's sanity check this.

Consider the function G.

(defun G (n)
(assert (typep n 'number))
"hello")

G is in (is an element of the type) number->string, because if I call
G with any number it will return a string. Additionally G is in
integer->number, for if I call G with any integer it also return a
string. This is in-keeping with (but does not yet prove) the TAPL
claim: number->string <: integer->string.

Now consider the function H.

(defun H (i)
(assert (type i 'integer))
"hello")

H is in integer->string, because if I call H with any integer it will
return a string. However, H is not in number->string because there
exists a number, (example 3.4), such that H fails to return a
string. (H 3.4) does not return a string.

Therefore, int->string <: number->string is FALSE. Why? Because there
is an element, H, in int->string which is not in number->string.


Curiously, the behavior of subtypep, does seem to be consistent with
the CL specification. In particular with the specification of the
type FUNCTION, (http://clhs.lisp.se/Bod... section Compound
Type Specifier Description:) which claims that the intersection

(and (function (arg0-type1 arg1-type1 ...) val-type1)
(function (arg0-type2 arg1-type2 ...) val-type2))

is

(function ((AND arg0-type1 arg0-type2)
(AND arg1-type1 arg1-type2 ...)
...)
(and val-type1 val-type2)),

not

(function ((OR arg0-type1 arg0-type2)
(OR arg1-type1 arg1-type2 ...)
...)
(and val-type1 val-type2))

as TAPL would otherwise lead me to believe.
8 Answers

Jeff Barnett

3/17/2016 5:54:00 PM

0

Jim Newton wrote on 3/17/2016 9:37 AM:
> Can someone please help me understand the semantics of function types
> in Common Lisp. Are they somehow backwards from other functional
> languages? Are the backward from arrow types in typed lambda
> calculus? --- deleting tons of stuff ---

If a slot, V, has type T, then only objects of type T can be put in that
slot. Since if S is a subtype of T, all objects of type S can be put in
V too since they are also of type T as well as S. The idea is that a
type declaration is an advertisement that if you access V you have the
right to expect to find an object of type T.

Now let's look at what a function type declaration, say (function
(rational) rational), might mean. First it says that V should be
expected to contain a callable object with one argument and one usable
value. Second it says that the function was (probably) written to take
advantage of the fact that its argument is a rational which means that
the argument can be any subtype (e.g., integer) of rational including
rational itself. The third thing that is declared is that the value will
be some sort of rational and that it can be put anyplace where a
rational is legal, i.e, any place expecting a supertype of rational
including rational itself.

So we get the concept that (function (rational) rational) is a subtype
of (function (integer) number) because any function with the first type
can be called when the expectation is using a function of the second type.

I hope this helps.
--
Jeff Barnett

Alan Bawden

3/17/2016 6:21:00 PM

0

Jeff Barnett <jbb@notatt.com> writes:
> ..
> So we get the concept that (function (rational) rational) is a subtype of
> (function (integer) number) because any function with the first type can be
> called when the expectation is using a function of the second type.

And yet in SBCL:

* (subtypep '(function (rational) rational) '(function (integer) number))

nil
t
* (subtypep '(function (integer) rational) '(function (rational) number))

t
t

> I hope this helps.

What you said was correct, but does not explain the behavior of SBCL,
which it what was puzzling the original poster.

--
Alan Bawden

Kaz Kylheku

3/17/2016 7:22:00 PM

0

On 2016-03-17, Alan Bawden <alan@csail.mit.edu> wrote:
> Jeff Barnett <jbb@notatt.com> writes:
>> ..
>> So we get the concept that (function (rational) rational) is a subtype of
>> (function (integer) number) because any function with the first type can be
>> called when the expectation is using a function of the second type.
>
> And yet in SBCL:
>
> * (subtypep '(function (rational) rational) '(function (integer) number))
>
> nil
> t
> * (subtypep '(function (integer) rational) '(function (rational) number))
>
> t
> t

This looks like it is based on the concept that if a set of functions
accepts a number, then the set of functions which requires that number
to specifically be an integer and not just any number is a subset of
that set.

This is an instance in which subtyping by subsetting appears to be at
odds with subtyping by substitutability.

Integer-accepting functions are a special case of number-accepting
functions, belonging to that set. Yet, a number-accepting function (member
of the broad set) can be substituted whenever an integer-accepting
function is required (member of the subset).

By contrast, though circles are a subset of ellipses, an
ellipse cannot be substituted wherever a circle is required.

Same with "animal inheritance". If specifically a bear is required, an
animal will not do.

Can we model a function as a record, together with an evaluate?

That is to say suppose that (function (integer integer) rational)
is regarded similarly to be a (record rational integer integer).
The first slot is the return value (output slot), the remaining ones are
arguments (input slots). This record also has an associated operation,
which is not represented as type.

A function call takes place by stuffing values into input slots. The
record is then operated upon by a generic operator which invokes
the associated procedure. The procedure examines the input slots,
performs some calculation, and deposits a value into the output slot.
record of this type).

So why is it that we have to treat the output and input slots specially?
Both are subject to stuffing and retrieval.

But that's the thing: the caller stuffs the input slots and accesses
the output slot. Whereas the callee does the opposite.

Stuffing and accessing are different uses. If a slot is restricted
to rational, when you're stuffing it, you cannot stuff in any old number;
it has to be an integer or ratio. But you can access the slot under the
expectation of obtaining a number; your expectation isn't violated
by obtaining an integer or ratio, since the are numbers.

So restricting the output slot doesn't matter from the caller's
perspective, but restricting the input slots does.

From the callee's perspective, restricting the input slots
doesn't matter, but restricting the output slot does.

If a function that previously returned number is restricted to return
integer, that doesn't affect any outsiders; they are still getting
a number from the "output slot". That function's code is affected;
it can no longer return a ratio or real as it was doing before.

From the function's own point of view, its own new type is not
substitutable for the old type for the purposes of returning a value.

From the point of view of callers, it is perfectly substitutable.

Grumpus

3/18/2016 8:17:00 AM

0

Jim Newton wrote:
> Can someone please help me understand the semantics of function types
> in Common Lisp. Are they somehow backwards from other functional
> languages? Are the backward from arrow types in typed lambda
> calculus?

Yes, this seems to be backwards.

I guess here's the reason nobody ever notices, from the spec for
"System Class FUNCTION":

The list form of the function type-specifier can be used only for
declaration and not for discrimination

Hard to notice the problem in normal programs when you can't use the
types with TYPECASE or TYPEP or CHECK-TYPE.

It seems safe to assume that none of the affected CLs rely on higher
order type inference for safety, so they don't notice (from crashing
programs) either.

Jim Newton

3/18/2016 1:24:00 PM

0

I found something relevant in a clean-up issue of the spec.
I'm not sure how cleanup issues effect decisions about bug vs feature.
http://clhs.lisp.se/Issues/is...

Here is the quote:

CLtL states that a function such as CONS that is of type
(FUNCTION (T T) CONS)
is also of type
(FUNCTION (FLOAT STRING) LIST).

(t t)->cons <: (float string)->list {which obeys TAPL's typed lambda calculus}

Doesn't this mean that (subtypep '(function (t t) cons) '(function (float string) list))
must forbidden from returning NIL,T ?
Or it at least says that CLtL wished it to be so, maybe the final spec relaxed/changed this?

Or am I thinking of this backward?

In fact sbcl returns NIL,T in this case.

But at the bottom of the page, we see the following paragraph.

The list form of the FUNCTION type specifier is different from most
type specifiers because it cannot be used for discrimination.
Thus, the notion of "subtype" does not make sense, since assertions
about the functional value of a variable are only partially
about the actual value of the variable and mainly about the
values that might be passed to the variables (function) value.

Jim Newton

3/18/2016 1:45:00 PM

0

It appears that another language, Eiffel, defines sub typing
this curious way as well. (if A->X <: B->Y then A<:B)
But it is largely regarded as an embarrassing flaw in the design
of the language.

http://c2.com/cgi/wiki?Language...

Jim Newton

3/21/2016 12:51:00 PM

0

I found a discussion of this from June 2012
https://sourceforge.net/p/sbcl/mailman/message...

Jim Newton

3/23/2016 9:56:00 AM

0

The more I look into this, the more interesting it is.

There is a descent summary on wikipedia.
https://en.wikipedia.org/wiki/Covariance_and_contr...(computer_science)

In addition there are lots of papers particularly one from 1995 which deals a lot with
multi dispatch generic functions.
The paper is "Covariance and Contravariance: Conflict without a Cause" by
Giuseppe Castagna. http://www.pps.univ-paris-diderot.fr/~gc/papers/to...

The issue of the original post was concerning function types. But the more general issue
seems to be parametric types, i.e., types constructed from other types (rather than inherited from).
For example an array of integers vs a vector of integers vs an array of bignums.

What is the relation of T<S1> and T<S2>?
It seems to be implied by several things that I've read that if S1 and S2
are used as read/output operations T is covariant with respect to it argument (meaning that
if S1 is a subtype of S2 then T<S1> is a subtype of T<S2>). However, if S1 and S2 are used as in write/input operations, then T is contravariant (meaning if S1 is a subtype of S2, then T<S1> is a SUPERtype of T<S2>). If it is both, then it is (must be) invariant.

As a special case function types treat their arguments as input and return value as output. So they
should be covariant w.r.t. return type, but contravariant w.r.t argument type.

According to the wikipedia article, the languages C#, Scala, and OCaml allow the variance of
such type parameters to be either annotated by the programmer and checked by the compiler, or inferred by the compiler. Obviously the CL type system is not this sophisticated.

One has to wonder whether a CL compiler would be able to do better type inferencing and hence better optimization if it understood such variance.