* Naive question on Polymorphic lambda-calculus, etc
1999-03-18 23:26 Polymorphic lambda-calculus R.A.G. Seely
@ 1999-03-19 16:13 ` Ronnie Brown
0 siblings, 0 replies; 2+ messages in thread
From: Ronnie Brown @ 1999-03-19 16:13 UTC (permalink / raw)
To: categories
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
^ permalink raw reply [flat|nested] 2+ messages in thread