Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!mucs!chl
From: chl@cs.man.ac.uk (Charles Lindsey)
Newsgroups: comp.lang.functional
Subject: Re: A question about types in ML
Message-ID: <chl.658489695@m1>
Date: 13 Nov 90 09:48:15 GMT
References: <paula.658247771@shum> <fraser.658398987@melomys> <4906@rex.cs.tulane.edu>
Distribution: comp
Organization: Dept. Of Comp Sci, Univ. of Manchester, UK.
Lines: 20

In <4906@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann) writes:

>One might seek to create a union type which
>contains within it _all_ possible types
>(i.e. as the solution to a recursive type equation).
>Unfortunately this violates the requirement
>that all type signatures be finite constructions
>from the primitive types.

>The problem is that typechecking (and type inference)
>in the typed lambda calculus is not generally decidable.
>To make typechecking decidable, we impose a restriction
>on type signatures, such as the one above.

Please could you explain this more fully?

I.e. can you show us an example of a recursive type equation
that would cause problems in typechecking, together
with the precise restriction that would cause it
to be disallowed?