Re: Polymorphic lambda-calculus

Re: Polymorphic lambda-calculus

[R.A.G. Seely]

My 1987 JSL paper is a start - "Categorical Semantics for
Higher-Order Polymorphic Lambda Calculus", JSL 52 (1987) 4, 
pp 969 - 989.  In particular, look at section 3, where the
model of closure operators is described in categorical terms.

= rags =

On Thu, 18 Mar 1999, Elaine Gouvea Pimentel wrote:

> I'd like to know if there is any categorical model for
> polymorphic lambda-calculus.


=================================
<rags@math.mcgill.ca>
<http://www.math.mcgill.ca/~rags>

Naive question on Polymorphic lambda-calculus, etc

[Ronnie Brown]

This is written from the point of view of someone who would like to see a 
computational system which is much nearer to real mathematics than the 
current widely used systems (Maple, Mathematica, and various more 
specialised systems, e.g. Singular). 

Of these the only one which is clearly typed is Singular. There is also 
AXIOM,  which has parametrised types, types can be variables, there 
is multiple inheritance and coercion. It looks much nearer to what should 
be mathematics. On the other hand, its literature 
does not include any theory of the type system, so consistency is not 
clear, and it is not generally used. 

So my question is: does all this general theory of types give a clear 
indication as to what should be, not necessarily a final, but certainly a 
convenient theory adequate for expressing a majority of present day maths?

Let's make up a test case: one should be able to code reasonably 
conveniently the type  of a general groupoid acting on exterior algebras 
over a commutative ring, and also of course the category of such objects. 
A groupoid acting on exterior algebras with zero multiplication should be 
coercible to a groupoid acting on graded modules. 

I would prefer the sytem to be so simple that it will allow tests for 
consistency of new proposed types. Also it should be easy to understand, 
since it would represent nicely current practice. 

Is this idea a mirage? 

Ronnie







On Thu, 18 Mar 1999, R.A.G. Seely wrote:

> My 1987 JSL paper is a start - "Categorical Semantics for
> Higher-Order Polymorphic Lambda Calculus", JSL 52 (1987) 4, 
> pp 969 - 989.  In particular, look at section 3, where the
> model of closure operators is described in categorical terms.
> 
> = rags =
> 
> On Thu, 18 Mar 1999, Elaine Gouvea Pimentel wrote:
> 
> > I'd like to know if there is any categorical model for
> > polymorphic lambda-calculus.
> 
> 
> =================================
> <rags@math.mcgill.ca>
> <http://www.math.mcgill.ca/~rags>
> 
> 

Prof R. Brown, School of Mathematics, 
University of Wales, Bangor      
Dean St., Bangor, Gwynedd LL57 1UT, United Kingdom                               
Tel. direct:+44 1248 382474|office:     382475
fax: +44 1248 383663    
World Wide Web:
home page: http://www.bangor.ac.uk/~mas010/
New article: Higher dimensional group theory


Symbolic Sculpture and Mathematics:
http://www.bangor.ac.uk/SculMath/
Mathematics and Knots:
http://www.bangor.ac.uk/ma/CPM/exhibit/welcome.htm