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

[Johannes Waldmann]

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)
2. annotations should not be forced to be one-liners
   (because I might want to use my preferred expression layout)


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

Ah .. syntax wars.

Best regards.
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools