Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!uunet!munnari.oz.au!bruce!mmcg
From: mmcg@bruce.cs.monash.OZ.AU (Mike McGaughey)
Newsgroups: comp.lang.functional
Subject: Re: Type Assignment
Message-ID: <3615@bruce.cs.monash.OZ.AU>
Date: 18 Jan 91 15:38:56 GMT
References: <6817@uqcspe.cs.uq.oz.au>
Organization: Monash Uni. Computer Science, Australia
Lines: 60

farrell@batserver.cs.uq.oz.au (Friendless) writes:

>Several formulations of type assignment for the Damas-Milner language are
>studied, with a view toward their formalization in logical framework LF, and
>the suitability of these encodings for direct executions by the logic
>programming language Elf.

>  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. To get this

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 :-).
Unfortunately, the elegance is lost if one rewrites it using let..in
(you need one bound variable per occurrence of 'Expr'); writing a large
nondeterministic parser this way would be a headache!  There are other
ways around it (for instance, by collecting all the different types of
parse tree into one union type), but none are totally satisfactory, as
they all serve to clutter the program.

I believe an escape mechanism (from the type system) would be useful in
these cases - a way of *overriding* the derived type (expanding it)
rather than just restricting it.  A compiler could then check that all
your uses of the function were consistent with the type you specified,
and that the function itself was consistent with your type definition.
But this, too, may be only partially decidable.

Comments?

Cheers,

    Mike.
-- 
Mike McGaughey			ACSNET:	mmcg@bruce.cs.monash.oz

"His state is kingly; thousands at his bidding speed,
 And post o'er land and ocean without rest."		- Milton.