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

[Johannes Waldmann]

Peter Schneider-Kamp wrote:

> The terms could be given inside the program as comments
> (prefixed with "-- ") or supplied as arguments to the runme
> executables.

I'd prefer to have them in the program, as annotations.

Sadly enough, Haskell has no flexible annotation syntax
http://hackage.haskell.org/trac/haskell-prime/ticket/88
so we have to live with pragmas or comments.

But then let's have some special symbol, e. g. "-- terminates:"
*but* this would make multi-line  queries inconvenient,
so I suggest a block pragma {-# TERMINATES: foo x y #-}

I am a bit worried about variables in such expressions:
I would feel much better to declare them.
{-# TERMINATES: forall  x :: [Integer] , y :: Bool . foo x y #-}

I am totally against the convention "every undeclared identifier
is considered an all-quantified variable" because it breaks all too easy
(imagine you add some declaration for a constant "x" to the program).

It should be OK to have several such TERMINATES annotations
in one program.

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