farrell@batserver.cs.uq.oz.au (Friendless) (01/18/91)
Just looking through the tech report lists here, and I found this one: CMU-CS-90-144 Systems of Polymorphic Type Assignment in LF Robert Harper June 1990 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 paper, write to School of Computer Science Carnegie Mellon University Pittsburgh, Pennsylvania 15213 United States of America John
mmcg@bruce.cs.monash.OZ.AU (Mike McGaughey) (01/18/91)
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.
thorinn@diku.dk (Lars Henrik Mathiesen) (01/19/91)
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