Research/Study in Logics, Types, Rewriting, & Applications

2000-08-08 Thread Joe Wells

The ULTRA group (Useful Logics, Types, Rewriting, and Applications) at
Heriot-Watt University in Edinburgh is seeking active and energetic
candidates for the following positions:

  * 2 postdoctoral research positions, 6 months each (extendable
depending on performance and funding), starting 1 October 2000
(possibly negotiable)

  * 1 postgrad student position

Preference will be given to candidates with strong backgrounds in one
or more of the following areas:

  * Type inference (i.e., searching for types given an untyped
program) and the use of types for program analysis.  Expertise in
intersection/union types is especially useful, but not necessary.

  * Equational reasoning for programming language semantics, including
imperative features (I/O, assignments, etc.).

  * Logics (both classical and constructive), type theories, rewriting
systems (including lambda calculus), and their interaction in the
Proofs-as-Programs/Propositions-as-Types correspondence
(a.k.a. the Curry/Howard/de Bruijn correspondence).
  
  * Notions of binding, reference, and substitution, including such
areas as explicit substitutions, generalized notions of reduction,
and mechanisms for supporting type definitions in typed calculi.

In all of these areas, there are opportunities both for research in
theoretical foundations (e.g., proving termination, confluence,
subject reduction, extensions to polymorphic types, etc.) and
practical implementations aimed both at programming languages and
theorem provers.

The ULTRA group does research in the design, implementation, and
applications of systems of logic, types, and rewriting.  The group
regularly organizes international events both at Heriot-Watt and
abroad.  The group also has strong international collaborations (in
particular with the AUTOMATH and Type Theory group in Eindhoven (NL)
and the Church Project (USA)) and regularly brings high-level
researchers to visit Heriot-Watt.  Further information about the ULTRA
group can be found at http://www.cee.hw.ac.uk/ultra/>.

Interested candidates should send the following:

  1. Curriculum vitae.
  2. Three letters of recommendation sent to us directly by your
 references.
  3. A two-page description of how your research fits the goals of
 the ULTRA group.

This material should be sent to either Prof. Fairouz Kamareddine or
Dr. Joe Wells at one of these addresses:

  Postal: Heriot-Watt University
  Dept. of Computing & Electrical Eng.
  Riccarton, EDINBURGH, EH14 4AS
  Scotland, UK
  E-mail: [EMAIL PROTECTED], [EMAIL PROTECTED]
  Fax: +44 131 451 3327

Further information can be obtained by contacting either
Prof. Kamareddine or Dr. Wells.




Re: [ANNOUNCE] HDoc: a "javadoc for Haskell"

2000-08-08 Thread Benjamin Leon Russell

Armin,

Is HDoc also designed to work with the February 2000 version of Hugs98?

Will it work under Linux and MacOS as well as under Win 32 (including Windows 2000)?

--Benjamin L. Russell
[EMAIL PROTECTED]
[EMAIL PROTECTED]

On Tue, 8 Aug 2000 20:25:08 +0200 (CEST)
 Armin Groesslinger <[EMAIL PROTECTED]> wrote:
> Hello,
> 
> I have written a small program, HDoc, which can generate
> HTML documents from specially annoted Haskell sources;
> currently it is possible to document functions, data
> types,
> classes and instances. The resulting documents are cross
> linked and - IMHO - they look pretty nice. So, HDoc
> does pretty the same job as javadoc does for Java.
> 
> Currently, _all_ the information is taken from special
> comments, i.e. the Haskell code is simply ignored (I
> found that it is very difficult (compared to Java) to
> extract the necessary information from Haskell code.
> 
> Here's an example of what the special comments
> for a function can look like (I admit, it looks a bit
> like
> javadoc...)
> 
> {---
>  @fun square :: Integer -> Integer  !  Squares an
> integer.
>  The number is multiplied by itself and the result is
>   returned.
> 
>  @param x :: Integer! the number to be squared.
>  @return res :: Integer ! the input number squared.
> -}
> square x = x * x
> 
> --
> 
> HDoc is not complete or ready for daily use; I'm looking
> for
> some feedback/ideas etc. HDoc runs on Hugs98 and GHC 4.08
> (other compilers may work, but I haven't tried).
> 
> You can get HDoc from its homepage at
> http://www.fmi.uni-passau.de/~groessli/hdoc/
> 
> An example of HDoc's output (for three very simple
> modules) can be viewed at
> http://www.fmi.uni-passau.de/~groessli/hdoc/examples/simple/docs/
> 
> 
> Please note again: HDoc is in a very early stage (it'll
> get a re-write soon to reflect some experiences from the
> first version). The main reason for announcing HDoc at
> this
> time is that I definitely need some feedback on how
> useful
> HDoc is or can eventually be and what concepts it should
> follow etc.
> 
> So if you're interested, please give HDoc a try and send
> me
> your ideas/suggestions/etc.
> 
> I'm looking forward to receiving your comments!
> 
> 
> Cheers,
> 
>  Armin
> 
>  
> 
> 
> 





[ANNOUNCE] HDoc: a "javadoc for Haskell"

2000-08-08 Thread Armin Groesslinger

Hello,

I have written a small program, HDoc, which can generate
HTML documents from specially annoted Haskell sources;
currently it is possible to document functions, data types,
classes and instances. The resulting documents are cross
linked and - IMHO - they look pretty nice. So, HDoc
does pretty the same job as javadoc does for Java.

Currently, _all_ the information is taken from special
comments, i.e. the Haskell code is simply ignored (I
found that it is very difficult (compared to Java) to
extract the necessary information from Haskell code.

Here's an example of what the special comments
for a function can look like (I admit, it looks a bit like
javadoc...)

{---
 @fun square :: Integer -> Integer  !  Squares an integer.
 The number is multiplied by itself and the result is
  returned.

 @param x :: Integer! the number to be squared.
 @return res :: Integer ! the input number squared.
-}
square x = x * x

--

HDoc is not complete or ready for daily use; I'm looking for
some feedback/ideas etc. HDoc runs on Hugs98 and GHC 4.08
(other compilers may work, but I haven't tried).

You can get HDoc from its homepage at
http://www.fmi.uni-passau.de/~groessli/hdoc/

An example of HDoc's output (for three very simple
modules) can be viewed at
http://www.fmi.uni-passau.de/~groessli/hdoc/examples/simple/docs/


Please note again: HDoc is in a very early stage (it'll
get a re-write soon to reflect some experiences from the
first version). The main reason for announcing HDoc at this
time is that I definitely need some feedback on how useful
HDoc is or can eventually be and what concepts it should
follow etc.

So if you're interested, please give HDoc a try and send me
your ideas/suggestions/etc.

I'm looking forward to receiving your comments!


Cheers,

 Armin

 






RE: unlines: the mystery of the trailing \n

2000-08-08 Thread Sigbjorn Finne



Mark P Jones <[EMAIL PROTECTED]> writes:
> 
> | Here's a Prelude inconsistency that's been irking me once 
> | in a while for a loong time - today it came up again, so here goes:
> | 
> |   unlines   ["a","b"]   ==> "a\nb\n"
> |   unwords ["a","b"]   ==> "a b"
> |
> | [... unwords adds space between items, not at the beginning or end;
> | unlines puts a newline after each item, including at the end ...]
> 
> I quite like the fact that the definition for unlines gives us laws
> like:
> 
>   unlines (xs ++ ys) = unlines xs ++ unlines ys
>   unlines . concat   = concat . map unlines
> 
> Of course, the fact that unwords doesn't add a terminating space
> means that we don't get quite such nice laws for unwords ...
> 

Hi Mark,

yes, those laws would be nice to have too. I guess this shows that
treating text as just a list, doesn't give you all the laws you
would like. In my case, prepending some lines to a paragraph should
ideally have resulted in a bigger paragraph (with no trailing newlines.)

Anyway, Pretty gives me the laws I need & is more suitable for
the job. No reason to tweak the defn of unlines.

--sigbjorn




Re: Haskell and the NGWS Runtime

2000-08-08 Thread Marcin 'Qrczak' Kowalczyk

Tue, 8 Aug 2000 09:17:15 +0200, Erik Meijer <[EMAIL PROTECTED]> pisze:

> You hit the nail right on the head wrt to Haskell and .NET. This is
> precisely why I am working on Mondrian, which also goes under the name
> Haskell#, a pure, lazy functional language that seamlessly fits the .NET
> type system.

This is what worries me: modifying a bunch of languages to make them
incompatible with the rest of the world, locking their users to the
.NET platform. Embrace and extend. AFAIK this happened to Java, and
is common in C/C++ (using own functions and types instead of ISO/ANSI).

-- 
 __("<  Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
 \__/
  ^^  SYGNATURA ZASTĘPCZA
QRCZAK





Re: unlines: the mystery of the trailing \n

2000-08-08 Thread Marcin 'Qrczak' Kowalczyk

Mon, 7 Aug 2000 17:58:40 -0700, Sigbjorn Finne <[EMAIL PROTECTED]> pisze:

> Here's a Prelude inconsistency that's been irking me once 
> in a while for a loong time - today it came up again, so here goes:
> 
>   unlines   ["a","b"]   ==> "a\nb\n"
>   unwords ["a","b"]   ==> "a b"

IMHO it should be that way. Because text files generally do have
the final '\n', but lines don't have a final space. Spaces are word
separators, '\n' are line terminators.

When I map each line of the file, I don't expect dealing with a final
empty line.

unlines a ++ unlines b = unlines (a++b)

> I'd find it a little more useful without the trailing \n
> (esp. considering now that putStrLn is std.)

writeFile "foo" (unlines listOfLines)
Using putStrLn here would be less convenient.

-- 
 __("<  Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
 \__/
  ^^  SYGNATURA ZASTĘPCZA
QRCZAK





Re: Haskell and the NGWS Runtime

2000-08-08 Thread Erik Meijer

Good idea to leave platform wars behind and return to language wars.

You hit the nail right on the head wrt to Haskell and .NET. This is
precisely why I am working on Mondrian, which also goes under the name
Haskell#, a pure, lazy functional language that seamlessly fits the .NET
type system. As you can imagine, the type system for such a language will be
quite a challenge. The current Mondrian implementation is much like SASL
(who remembers that great language) waiting to evolve to Miranda (watching
too much Pokemon these days :-)

Erik

- Original Message -
From: "Doug Ransom" <[EMAIL PROTECTED]>
To: <[EMAIL PROTECTED]>
Sent: Monday, August 07, 2000 7:44 PM
Subject: RE: Haskell and the NGWS Runtime


Back to the language wars then.

It does seem like integration of Haskell and the NGWS is a graunch, largely
because Haskell is not OO.

Is there anything preventing Haskell from becoming OO and seamlessly fitting
into the NGWS? Or from designing a functional language that would be a good
fit into the NGWS.

A major problem I see is that there is probably a standard set of container
classes in NGWS which have a high impedance mismatch with the lists
functional languags use for their constructions.

Can we ever have functional programming "in the large" given the OO paradigm
and NGWS are both here to stay?  This can not happen until I can get a
language which seamlessly fits into NGWS (or some similar thing on a
non-windows platform).












-Original Message-
From: Antony Courtney [mailto:[EMAIL PROTECTED]]
Sent: Sunday, August 06, 2000 3:49 PM
To: Jürgen A. Erhard
Cc: [EMAIL PROTECTED]
Subject: Re: Haskell and the NGWS Runtime


"Jürgen A. Erhard" wrote:
>
> > "Manuel" == Manuel M T Chakravarty <[EMAIL PROTECTED]> writes:
>
> Manuel> "Erik Meijer" <[EMAIL PROTECTED]> wrote,
> >> [...] The lab is *sponsored* by Microsoft, but definitively not
*at*
> >> Microsoft. I doubt there are any Linux boxes at Microsoft :-)
>
> Manuel> [...] There have also been reports of Linux boxes in the main
> Manuel> company, but the validity of these reports is of course not
>
> But easy to believe... I mean, wouldn't you take a good look at your
> competition?

Having spent five years doing Windows and Win32 hacking, and 10+ years
doing Unix hacking before that, I can assure you there is little evidence
that Microsoft are interested in learning anything whatsoever from Linux
or any other Unix work-alike.  Rather than re-iterate the argument, I'll
simply point interested readers towards the excellent article
"Working with Win32: the good, the bad and the ugly"
by David G. Korn
http://www.usenix.org/publications/login/1997-11/win32.html

which mostly reinforces the quote:
Those who do not understand Unix are condemned to reinvent
it, poorly. -- Henry Spencer

Now that I've gotten MY little barb in, can we PLEASE end this tangent on
OS wars, and return to our regularly scheduled language wars?  :-)

Thanks,

-Antony
(haskell list lurker)

--
Antony Courtney
[EMAIL PROTECTED]
http://www.apocalypse.org/pub/u/antony