Re: static type checking / interface definitions for Python?

Stephen J Bevan (bevan@cs.man.ac.uk)
24 Sep 1994 12:22:46 GMT

In article <35up38$2ot@darum.uni-mannheim.de> mw@ipx2.rz.uni-mannheim.de (Marc Wachowitz) writes:
There has been some work on type inference for Lisp, which is roughly
similar concerning dynamic data types. I don't have any reference ...

@techreport
{ Wright:Cartwright:rice:218:1993
, author= "Andrew K. Wright and Robert Cartwright"
, title= "A Practical Soft Type System for Scheme"
, institution= "Rice University"
, month= dec
, year= 1993
, url= "file://titan.cs.rice.edu/public/languages/tr93-218.dvi.Z"
, url= "file://titan.cs.rice.edu/public/languages/tr93-218.ps.Z"
, pages= 21
, checked= 19940302
, source= "url"
, keywords= "Scheme, type checking, type inference"
, abstract= "{\em Soft type systems} provide the benefits of staitc
typec checking for dynamically typed languages without rejecting
untypable programs. A soft type checker infers types for variables
and expressions and inserts explicit run-time checks to transform
untypable programs to typable form. We describe a practical soft type
system for R4RS Scheme. Our type checker uses a representation for
types that is expressive, easy to interpret, and supports efficient
type inference. {\em Soft Scheme} supports all of R4RS Scheme,
including procedures of fixed and variable arity, assignment,
continuations, and top-level definitions. Our implementation is
available by anonymous FTP."
}

@techreport
{ Lindig:10:1993
, author= "Christian Lindig"
, email= "lindig@ips.cs.tu-bs.de"
, title= "Style -- A practical Type Checker for Scheme"
, institution= "Technical University of Braunschweig, Germany"
, number= "93-10"
, month= oct
, year= 1993
, url= "file://ftp.ips.cs.tu-bs.de/pub/local/softech/papers/style.ps.gz"
, pages= 14
, checked= 19940312
, sjb= "Much simpler type system than Wright's
approach~\cite{Wright:Cartwright:rice:218:1993}, but had the advantage of
producing comprehensible types. Implemented in Scheme using
Aubry Jaffer's SCM. Doesn't have a separate list type, treats them as
pairs and has a hack to deal with the terminator. Can't type some
procedures, such as call/cc. Indicates that the software is available
for ftp, but doesn't include the ftp address."
, abstract= "This paper describes an new tool for finding errors in
$R^{4}RS$-compliant Scheme programs. A polymorphic type system in the
style of Damas \& Milner~\cite{Damas:Milner:popl:1982} with an
additional maximum type is used to type Scheme code. Although Scheme
is dynamically typed, most parts of programs are statically typeable;
type inconsistencies are regarded as hints to possible programming
errors. The paper first introduces a type system which is a careful
balance between rigorous type safety and pragmatic type softness. An
efficient and portable implementation based on order sorted
unification in Scheme is then described. We obtained very
satisfactory results on realistic programs, including the programs in
Abelson, Sussman \& Sussman~\cite{Abelson:Sussman:Sussman:1985}."
}

@inproceedings
{ Wright:Cartwright:acm:lfp:1994
, author= "A. K. Wright and R. Cartwright"
, email= "{wright,cartwright}@cs.rice.edu"
, title= "A Practical Soft Type System for Scheme"
, crossref= "acm:lfp:1994"
, refs= 25
, url= "ftp://cs.rice.edu/public/languages/lfp94-wc.ps"
, keywords= "Scheme, type inference"
, abstract= "{\em Soft typing} is a generalization of static type
checking that accommodates both dynamic typing and static typing in
one framework. A soft type checker infers types for identifiers and
inserts explicit run-time checks to transform untypable programs to
typable form. {\em Soft Scheme} is a practical soft type system for
R4RS Scheme. The type checker uses a representation for types that is
expressive, easy to interpret, and supports efficient type inference.
Soft Scheme supports all of R4RS Scheme, including uncurried
procedures of fixed and variable arity, assignment, and continuations."
}