From: David Golden
Subject: Type Variables
Date: 
Message-ID: <235b265c.0305170452.40d5f1f0@posting.google.com>
Just following this thread on kuro5hin
http://www.kuro5hin.org/comments/2003/5/6/16516/53433/134#134

As someone who hasn't really cared much about typing until now:

Are there "type variables" in Common Lisp that I've missed? 

Example from above link:


So the type of [haskell] map is "for any types a and b, 
take a function from a to b and a list of a, and
return a list of b". 


not-real-lisp-hypothetical-example:

(declare 
  (ftype 
    (function ((function (tvar a) (tvar b)) (vector (tvar a) *))
      (vector (tvar b) *)))
  hmap)

where tvar denotes a type variable lexically scoped to the type
declaration???
Or maybe bare keywords in type declarations could be type variables...
I dunno, clutching at straws here...

Perhaps CMUCL already tracks this sort of thing internally, I don't
know.

Probably people shaking their heads now and going "why are there so
many people trying to turn CL into a statically-typed language
lately?" - I'm not, I'm just curious. I know a pragmatic solution if
you wanted such type checking would be to make a macro hmap that
expands into different type-declared functions for different types
given as parameters to the macro, but perhaps there would be
advantages for type-checking and compiler-optimisation if
type-variables were possible in a standard manner in type
declarations.

From: Kaz Kylheku
Subject: Re: Type Variables
Date: 
Message-ID: <cf333042.0305171545.7b4b436e@posting.google.com>
············@oceanfree.net (David Golden) wrote in message news:<····························@posting.google.com>...
> Just following this thread on kuro5hin
> http://www.kuro5hin.org/comments/2003/5/6/16516/53433/134#134
> 
> As someone who hasn't really cared much about typing until now:
> 
> Are there "type variables" in Common Lisp that I've missed? 

Types are objects in Lisp, for instance:

 (type-of 3) ==> INTEGER

They can be bound to variables, etc.

But I think you are asking about compile-time meta-variables, like C++
template parameters and the like. The answer is that in Lisp we don't
need them, because compile time isn't any different or special
compared to run time. The full language is there, and so entities like
type expressions are manipulated using ordinary code with ordinary
variables.

When you write a macro with a backquote template in it, you are
meta-manipulating the language source code, but using ordinary Lisp.

> Example from above link:
> 
> 
> So the type of [haskell] map is "for any types a and b, 
> take a function from a to b and a list of a, and
> return a list of b". 

Of course, in Lisp we just write:

  (mapcar #'function-from-a-to-b list-of-a) 

and hope that list-of-a really is a list of A things, and that the
function accepts A things and puts out only B things. If not, some
run-time type check will hopefully catch the problem.

> not-real-lisp-hypothetical-example:
> 
> (declare 
>   (ftype 
>     (function ((function (tvar a) (tvar b)) (vector (tvar a) *))
>       (vector (tvar b) *)))
>   hmap)
> 
> where tvar denotes a type variable lexically scoped to the type
> declaration???

You could use a backquote template to insert variant pieces into a
declaration.

  (defmacro declare-binary-func-with-types (a-type b-type)
    `(declare  ... ,a-type ,b-type ...)

Now you have a language construct whose arguments, which are ordinary
variables, behave semantically like type variables. Their bindings are
established at macroexpansion time, and connect to type expressions.

> lately?" - I'm not, I'm just curious. I know a pragmatic solution if

But you want non-pragmatic solutions too? :)

> you wanted such type checking would be to make a macro hmap that
> expands into different type-declared functions for different types
> given as parameters to the macro, but perhaps there would be
> advantages for type-checking and compiler-optimisation if
> type-variables were possible in a standard manner in type
> declarations.

Declarations don't follow the normal rules of evaluation. If a symbol
occurs there, it won't be reduced to its value binding, lexical or
otherwise. The meta-syntactic approach is the right one: interpolate
whatever pieces you want into the source code of the form prior to its
evaluation.
From: Joe Marshall
Subject: Re: Type Variables
Date: 
Message-ID: <smraoosz.fsf@ccs.neu.edu>
···@ashi.footprints.net (Kaz Kylheku) writes:

> Of course, in Lisp we just write:
> 
>   (mapcar #'function-from-a-to-b list-of-a) 
> 
> and hope that list-of-a really is a list of A things, and that the
> function accepts A things and puts out only B things. If not, some
> run-time type check will hopefully catch the problem.

or if we are paranoid:

(defun make-paranoid-function (original-function input-type result-type)
  (lambda (input-value)
    (unless (subtypep (type-of input-value) input-type)
      (error 'simple-type-error :datum input-value 
                                :expected-type input-type))
    (let ((result (funcall original-function input-value)))
      (unless (subtypep (type-of result result-type))
        (error 'simple-type-error :datum result
                                  :expected-type result-type))
      result)))

(mapcar (make-paranoid-function #'function-from-a-to-b type-a type-b)
        list-of-a)
From: David Golden
Subject: Re: Type Variables
Date: 
Message-ID: <235b265c.0306070445.1f18f1a0@posting.google.com>
> but perhaps there would be
> advantages for type-checking and compiler-optimisation if
> type-variables were possible in a standard manner in type
> declarations.


A following-up on my earlier vagueness, that provides some of what
those american television shrinks call "closure":

The idea is actually called "Dependent Types" in CompSci literature,
and is a feature of a 1999 haskell-like research language called
"Cayenne" by Lennart Augustsson,
http://www.math.chalmers.se/~augustss/cayenne/

Unfortunately, according to the above link:

"The drawback of such a powerful type system is that the type checking
becomes undecidable."

The papers on Cayenne make for interesting reading.  If you're into
that sort of thing :-).