On Tue, 12 Feb 2008, Martin Rubey wrote: | Gabriel Dos Reis <[EMAIL PROTECTED]> writes: | | > Hi, | > | > Here is a problem -- currently failing -- for type inference in the | > interpreter. Consider (taken from current testsuite) | > | > primes == [p := nextPrime(i = 0 => 2; p) for i in 1..] | > primes | | I guess you meant to type i = 1 above.
It does not matter -- I copied verbatim the testcase. All that matters is the type. | In that case, the following works: I suspect my question is whether the original code is something we want to have typechecked. I have several ways to rewrite the code to have it `work'. However, from the language semantics point of view, I'm looking at what people consider `reasonable' and what isn't. | | (1) -> p: INT | Type: Void | (2) -> [(p := nextPrime(i = 1 => 2; p)) for i in 1..] | | (2) [3,5,7,11,13,17,19,23,29,31,...] | Type: Stream Integer | | Note that you have to supply a parenthesis around (p := ...). I believe that | this helps the interpreter to notice that (p := ...) is actually a function. | This gives us some more information, in fact: without the p: INT, it tells us | that it cannot compile (p := ...), which I find not so surprising anymore. As you noted, with any sort of declaration for `p', the interperter has no trouble. However, I suspect my question is more general: is that the kind of script we just want to reject? Notice that I'm not talking of this *particular* script, but the kind of program it illustrates. In general, assigning to a variable gives it a type infered from the value being assigned to it; so one might think that p := nextPrime(i = 0 => 2; p) gives `p' the unambiguous type Integer. But it does not. To explain that clearly takes some amount of time. The reason I'm raising this is that over the last six months I've gotten several questions like that -- some having to do with type, some having to do with evaluation. | But | probably, that is exactly what you *did* find surprising, or at least | annoying. Well, personally, I did find the script plain obfuscation to tell the truth :-) So I was not surprising, nor annoyed. But, that isn't a universally hold; which is why I'm raising the question here, to see what people think. | So, what you want is that | | (p := f(firstTime? => someValue; p)) | | can be resolved, namely using the meet of someValue and the result type of | f(someValue)... | | Looks pretty hard to me, though. Indeed, it is in the context of Spad script where the type inference rules are not all written out. I would be happy to sweep it under the rug if people feel comfortable with that. (I've had fundamentally similar questions about definining unnamed functions). Thanks, -- Gaby ------------------------------------------------------------------------- This SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
