Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!think.com!mintaka!bloom-beacon!eru!hagbard!sunic!mcsun!ukc!newcastle.ac.uk!turing!ncmh
From: Chris.Holt@newcastle.ac.uk (Chris Holt)
Newsgroups: comp.lang.misc
Subject: Re: Optional static typing limits
Message-ID: <1991Apr22.153149.8082@newcastle.ac.uk>
Date: 22 Apr 91 15:31:49 GMT
References: <LIBERTE.91Apr16164831@babbage.ncsa.uiuc.edu> <8493:Apr1719:30:0791@kramden.acf.nyu.edu>
Sender: news@newcastle.ac.uk
Organization: University of Newcastle upon Tyne, UK, NE1 7RU
Lines: 25

brnstnd@kramden.acf.nyu.edu (Dan Bernstein) writes:

>And, as a first sample problem to be solved by a typing system: How do
>we write a generic, type-safe sorting routine? What's the best that
>available languages can do to make this work? Remember, type-safe means
>that the sort routine will never tell you ``can't apply < to glorps'' at
>run-time, as a dynamically typed system would.

What would be nice would be something of the form

Sort S <=
    where
    S : sequence of D
    D : domain
    <= : partial_order (D x D -> boolean)
        where
        partial_order : transitive & reflexive & antisymmetric

Of course, partial_order would be part of the standard toolbox of
the programmer; it maps the domain of dyadic D-to-boolean operations
to that subset satisfying the given properties.  I will dream on...
-----------------------------------------------------------------------------
 Chris.Holt@newcastle.ac.uk      Computing Lab, U of Newcastle upon Tyne, UK
-----------------------------------------------------------------------------
 "And when they die by thousands why, he laughs like anything." G Chesterton