🚀 go-pugleaf

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.

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