functional programs, was: Re: [Termtools] Next competition

[Peter Schneider-Kamp]

-----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