functional programs, was: Re: [Termtools] Next competition
Peter Schneider-Kamp
psk at informatik.rwth-aachen.de
Thu Mar 16 13:56:14 CET 2006
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1
Johannes Waldmann wrote:
> Peter Schneider-Kamp wrote:
>
>> "-- start term: " or "-- terminates: " would both be okay
>> with me. I do not see the need for multi-line queries, though.
>> What kind of queries do you have in mind?
>
> perhaps there is a misunderstanding. My goals are:
> 1. annotated program should be legal Haskell
> (so a standard Haskell compiler can just ignore the annotation)
That much I agreed on.
> 2. annotations should not be forced to be one-liners
> (because I might want to use my preferred expression layout)
Okay, I get your point. What about allowing TERMINATES expressions
in both kinds of comments? But I am okay with multi-line comments only.
>> Declaring all abstract variables (whatever the syntax) sound like
>> a good idea to me. But declaring the type could be done
>> in the term: foo (x::Integer) (y::Bool)
>
> These are separate issues:
> 1. declare a type for a term (you need this e. g. to disambiguate
> some polymorphic expression)
> 2. declare an all-quantified variable
>
> Of course (1) should be allowed, but I oppose the idea
> that (1) somehow magically implies (2). See your example.
> Presumably you mean x and y to be all-quantified variables,
> but imagine later you add a declaration to the program:
> x :: Num a => a ; x = 42
> Then the type annotation in the query still is correct and sensible,
> but the annotation has silently changed its meaning. (Earlier,
> it declared a new free x, now it disambiguates some existing x.)
This is probably a misunderstanding, too. I agree that we should have
some declaration like "forall x, y" separate from the start term
such that abstract variables are explicitly declared.
I do not see the need to declare the type for these abstract variable
in the "forall"-statement, though. In most cases this is not needed and
in those where it is, type annotations could be used in the start term.
> Ah .. syntax wars.
Let's try diplomatic talks first ;-)
Kind regards,
Peter
- --
Peter Schneider-Kamp mailto:psk at informatik.rwth-aachen.de
LuFG Informatik II http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen phone: ++49 241 80-21211
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.2.1 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFEGWBu3VbrCXkKHhwRAsJFAKDJDhcePHH9xSNr/K97LrQR+iLNTACeNaGY
Tenrk2pB6eXOew9P6XYX+xY=
=CgLy
-----END PGP SIGNATURE-----
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools
More information about the Termtools
mailing list