Python from Wise Guy's Viewpoint

[Fergus Henderson]

prunesquallor at comcast.net writes:

>"Andreas Rossberg" <rossberg at ps.uni-sb.de> writes:
>
>> Sorry, but that reply of yours somewhat indicates that you haven't really
>> used modern type systems seriously.
>>
>> All decent type systems allow you to define your own types. You can express
>> any domain-specific abstraction you want in types. Hence the type language
>> gives you additional expressive power wrt the problem domain.
>
>Cool!  So I can declare `Euclidean rings' as a type an ensure that I
>never pass a non-Euclidean ring to a function?

You can easily declare "EuclideanRings" as a type class
(in Haskell/Clean/Mercury, or similar constructs in other languages),
and ensure that you only pass this function values whose type has been
declared to be an instance of that type class.

Generally the type system won't be able to enforce that the
"EuclideanRings" type class really represents Euclidean rings
that conform to all the appropriate axioms.  However, declaring
an abstract type like this is nevertheless very useful as documentation:
it makes it clear where the proof obligation lies.  _If_ you prove that
every declared instance of the type class is really a Euclidean ring,
then that, together with the type system, will be enough to guarantee
that the function's argument is always a Euclidean ring.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.