Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!wuarchive!rex!caesar!fs
From: fs@caesar.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.functional
Subject: Re: A question about types in ML
Message-ID: <4953@rex.cs.tulane.edu>
Date: 14 Nov 90 15:47:52 GMT
References: <fraser.658398987@melomys> <4906@rex.cs.tulane.edu> <chl.658489695@m1>
Sender: news@rex.cs.tulane.edu
Distribution: comp
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 51


>>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.

In article <chl.658489695@m1> chl@cs.man.ac.uk (Charles Lindsey) writes:
>	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?

I am not sure exactly how to answer your question,
but since I am not expert on this subject.
However, I've gathered these relevant statements
from varied readings.

A) General typechecking is said to be undecidable.

B) In programming languages based on Church's typed lambda calculus,
   typechecking _is_ decidable.  Therefore, if A) is true,
   these languages must impose some restriction to accomodate typechecking.

C) I've never seen a programming language
   based on typed lambda calculus whose typechecking system
   permits the user to define a fixpoint combinator
   out of more primitive elements.  The type signature
   of the necessary lambda expression cannot be written
   as a finite combination of the primitive types
   (so Y-combinators must be added as primitives).

D) Church's typed lambda calculus subsumes the
   pure untyped lambda calculus as a special case.

E) In the pure, untyped lambda calculus
   it _is_ possible to define a fixpoint combinator.

Therefore, I conclude that typed languages (such as ML)
must not permit the kind of type-unions necessary
for definition of self-applicative functions.

	Frank Silbermann	fs@cs.tulane.edu
	Tulane University	New Orleans, Louisianna  USA