From: Howard R. Stearns
Subject: Re: declaring types with variable bits of precision
Date: 
Message-ID: <340C4A76.5656AEC7@elwood.com>
Others have noted how CL does not evaluate the components of type
declarations, though reader macros and deftypes may be used to provide a
somewhat clean READ/COMPILE TIME PARAMETERIZATION.

It has also been noted that to do any optimization, the compiler must
know the specific type at compile time.

I believe, however, that there are some case where the compiler could do
some optimization if it was able to determine the type modulo some
parameter which remained consistent throught the code.  The precise
value of the parameter is not known at compile time, but it compiler
does know what depends on the parameter. This occurs most often, I
suspect, with arrays.

For example:
  (defun foo (array &aux (length (length array))
                         (etype (array-element-type array))
    (declare (type (simple-array TP (LP))
             (type (integer LP LP) length)
             (type (eql TP) etype))
     ....)

For some optimizations, it is enough for the compiler to know that LP is
the same everywhere it is used above, as opposed to actually needing to
know its specific value.  (There may be analogous optimizations based on
TP, but I can't think of any off-hand.)

Alas, such declarations are not legal in Common Lisp.  Does anyone know
of any work to support this sort of thing (paper references, etc.)  Do I
understand correctly that ML supports such parameterized type
declarations?


Bruce L. Lambert, Ph.D. wrote:
> 
> Hi people,
> 
> I want to write a fucntion that uses an array of unsigned-bytes, but I
> want to let the user decide how many bits of precision to use in each
> unsigned-byte. How do I write a declaration that allows me to do this?
> 
> For example:
> (defparameter *num-bits* 8)
> ...
> (defun foo (an-array)
>   (declare (type (simple-array (unsigned-byte *num-bits*) (*))
>                  an-array))
>   (dotimes (i (length an-array))
> 
>    ...))
> 
> The CLISP compiler chokes on this declaration. I could rewrite it as a
> macro, and then it will work. But in my system, many functions need to
> know how many bits are going to be in an unsigned-byte. Must I rewrite
> all these functions as macros? There must be a better way.
> 
> Thanks.
> 
> -bruce
> 
> --
> 
> Bruce L. Lambert
> Department of Pharmacy Administration
> University of Illinois at Chicago
> Phone:  (312) 996-2411
> Fax:    (312) 996-3272
> email:  ········@uic.edu
> WWW:    http://ludwig.pmad.uic.edu/~bruce/
From: Matthias Hoelzl (tc)
Subject: Polymorphic types,  Was: declaring types with...
Date: 
Message-ID: <87u3fzmftc.fsf_-_@gauss.muc.de>
"Howard R. Stearns" <······@elwood.com> writes:

> I believe, however, that there are some case where the compiler could do
> some optimization if it was able to determine the type modulo some
> parameter which remained consistent throught the code.  The precise
> value of the parameter is not known at compile time, but it compiler
> does know what depends on the parameter. This occurs most often, I
> suspect, with arrays.
> 
> For example:
>   (defun foo (array &aux (length (length array))
>                          (etype (array-element-type array))
>     (declare (type (simple-array TP (LP))
>              (type (integer LP LP) length)
>              (type (eql TP) etype))
>      ....)
> 
> For some optimizations, it is enough for the compiler to know that LP is
> the same everywhere it is used above, as opposed to actually needing to
> know its specific value.  (There may be analogous optimizations based on
> TP, but I can't think of any off-hand.)
> 
> Alas, such declarations are not legal in Common Lisp.  Does anyone know
> of any work to support this sort of thing (paper references, etc.)  Do I
> understand correctly that ML supports such parameterized type
> declarations?

If I understand you correctly, what you are describing are polymorphic
types, and your LP and TP correspond to two different types of
polymorphism: The polymorphism exhibited by TP is sometimes called
"parametric polymorphism", the one shown by LP "inclusion
polymorphism".  I'll use some pseudo-code to exemplify these two
concepts.

Let's say you want to write a projection function for pairs: 
`fst((a, b))' evaluates to `a' (where `(a, b)' represents the pair
consisting of `a' and `b').  Then `fst' should work e.g. for pairs of
integers and return an integer value, `fst' should work for pairs of
booleans and return a boolean value, and `fst' should also work on
pairs consisting of an integer as first component and a boolean value
as second component and return an integer in this case.  However fst
should not take a single integer as argument.  If we use * and ** as
names for types, -> as the constructor for function types and ( , ) as
the constructor for products, then we can express the type of `fun' as
`forall*: forall**: (*, **) -> *'.  This is the type that ML would
infer for this function (with implicit quantification and different
syntax), and this corresponds to `TP' in your example (if I didn't
miss your point).  [In ML you don't have to declare the type, the 
type system is designed in such a manner that the compiler can
figure out the most general type of function definitions.]

For LP the case is different since you don't want to specify that
`foo' works for arguments LP of arbitrary type, but since you declare
LP to be a subtype of `integer', or to express this more formally, you
don't use an universal quantification of the form "For all types *",
you use a bounded quantification "For all subtypes ** of *".  (Of
course you need a type * such that the subtypes of * are precisely
single integers if you want to preserve the semantics of your
expample.)  I don't think that inclusion polymorphism for function
arguments is supported in ML.

There is quite a lot of research going on in this area, the best
starting point is (in my opinion, of course) a paper by Luca Cardelli
and Peter Wegner:

"On understanding types, data abstraction and polymorphism."

You will probably find a pointer to this paper and to some more recent
papers on Luca Cardelli's home page:

<http://www.research.digital.com/SRC/personal/Luca_Cardelli/home.html>

(if not I can look it up next week).

Hope this helps,

  Matthias