Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!uunet!wuarchive!zaphod.mps.ohio-state.edu!rpi!uupsi!sunic!dkuug!diku!thorinn
From: thorinn@diku.dk (Lars Henrik Mathiesen)
Newsgroups: comp.lang.functional
Subject: Re: Type Assignment
Message-ID: <1991Jan19.061015.26816@odin.diku.dk>
Date: 19 Jan 91 06:10:15 GMT
References: <6817@uqcspe.cs.uq.oz.au> <3615@bruce.cs.monash.OZ.AU>
Sender: news@odin.diku.dk (Netnews System)
Organization: Department of Computer Science, U of Copenhagen
Lines: 88

mmcg@bruce.cs.monash.OZ.AU (Mike McGaughey) writes:
>farrell@batserver.cs.uq.oz.au (Friendless) writes:
>>This sounds to me like the answer to the question MMCG asked about why can't
>>a parameter be multiple instantiations of a polymorphic type.

>Thanks, John.  Actually, any pointers to work on or papers describing
>even partially decidable type systems (ie: which terminate given a
>well-typed program) would be appreciated.

>As for rewriting the code using let..in, the following example
>should illustrate my frustration :-) : (in LML)

>---------

>infixr "OR"; infixr "!";	-- right associative sugar.

>(OR) a b s = a s (b s)
>(!) a b = a b

>Expr follower reduce stream fail =
>let accept tree = follower (reduce tree) in
>    (token "let" ! Decl ! token "in" ! Expr ! accept) (\a.\b.\c.\d.Eletin b d)
>OR  (token "if" ! Expr ! token "then" ! Expr ! token "else" ! Expr ! accept)
>	(\a.\b.\c.\d.\e.\f.Eif b d f)
>OR  (variable ! accept) (\a.Evar a)
>OR...
>OR  (\s.fail)

>-----------

>Expr has a finite type; it's just that it has more than one :-).

Actually not, it only has one (generic) type; but because Expr is
defined in terms of itself, LML can't find it. Most implementations of
Milner typing treat letrec-bound variables as if they were
lambda-bound _in_their_own_definitions_, unless the programmer
explicitly gives a generic typing. In the example above, Expr cannot
have the same non-generic type at all its occurences, so LML fails to
find a type.

I've appended a version in Miranda to this article; unless I've
misunderstood something, it should correspond exactly to the LML
version (I had to apply the righthand side to the stream argument to
make sense of it, though). As it stands, it has an explicit type for
Expr, and Miranda accepts it. If that typing is removed, Miranda
cannot find it.

I don't remember if ML allows types to be given explicitly. If it
does, that should solve your problem. You could also extend the
typechecker to handle letrecs properly. Mycroft [84, LNCS 167] has
shown that principal types exist when generic types are allowed in
letrecs, and shows an extended W-algorithm that can find them. The
problem is, it may not terminate in the presence of type errors (and
it is exponential in the number of nesting levels). Both problems can
probably be solved by using another data structure than the ``simple''
type environment (I'm thinking about it).

--
Lars Mathiesen, DIKU, U of Copenhagen, Denmark      [uunet!]mcsun!diku!thorinn
Institute of Datalogy -- we're scientists, not engineers.      thorinn@diku.dk

------------------Ugly Miranda demonstration hack follows-----------------
stream, res :: type		|| input and output
follow == stream->res->res	|| foo s r: match s, otherwise return r

dec, var, tok :: type		|| unknown types

ex ::= Eletin dec ex | Eif ex ex ex | Evar var

(a $o b) s = a s (b s)
a $t b = a b

expr :: (*->follow)->(ex->*)->follow
decl :: (*->follow)->(dec->*)->follow
variable :: (*->follow)->(var->*)->follow
token :: [char]->(*->follow)->(tok->*)->follow

expr follower reduce stream fail =
   ((token "let" $t decl $t token "in" $t expr $t accept) eletin	$o
    (token "if" $t expr $t token "then" $t expr $t
			   token "else" $t expr $t accept) eif		$o
    (variable $t accept) Evar						$o
    s_fail) stream
      where
	accept tree = follower (reduce tree)
      	eletin a b c d = Eletin b d
	eif a b c d e f = Eif b d f
	s_fail s = fail