Rob Turner <[EMAIL PROTECTED]> writes:
| How do you get a subtype in Haskell (or any other functional language
| come to that)? I'm thinking along the lines of (pseudo-notation):
|
| type weekday = {Mon, Tue, Wed, Thur, Fri}
| type weekend = {Sat, Sun}
| type day = weekend + weekday
|
| It springs to mind that this kind of problem is possibly solved by
| inheritance in the class system, but that only works for pre-defined
| classes. Or does it?
|
| Maybe subtypes don't fit elegantly into the functional model. Maybe
| they aren't necessary anyway.
|
| Thoughts appreciated.
|
| Rob
This is interesting. I don't know if there is a nice way of doing this
in Haskell. I've been looking for ways to extend ML with some kind of
subtype/supertype declarations, similar to what you suggest in your
example. What I want to achieve is subtypes based on variant types
as in the langauge Fun, described by Cardelli & Wegner in [1]
(recommended reading for anyone interested in polymorphism, subtypes
and similar type system related issues).
A variant type in Fun is an enumeration of tagged types, enclosed in
square brackets. For example, an element in the type
[ a:Int, b:Bool ]
is either an integer labelled "a" (e.g. [a=5]), or a boolean labelled "b"
(e.g. [b=false]). The subtype relation is defined as follow on variant
types (where <: denotes the subtype relation):
t1<:u1 ... tn<:un
------------------------------------------------------ (n<m)
[l1:t1, ..., ln:tn] <: [l1:u1, ... ln:un, ..., lm:um]
For example [a:Int] <: [a:Int, b:Bool].
To make this carry over to ML, the idea is to view data types in ML as
analogous to (named) variant types. For example the type
[ a:Int, b:Bool ] would correspond to
datatype T = a of Int | b of Bool
You can now imagine a new kind of declarations to obtain subtypes or
supertypes, by adding or removing constructors to an existing type, like
for example
subtype U <: T = a of Int
One can also imagine forming supertypes by taking unions of existing
types, like in the weekday & weekend example. (Exactly what kind of
declaration you should have, and what they should look like, is mainly
a pragmatical problem, I assume.)
The subtype declarations should also extend to parameterized types,
just like it does in Fun. For example I think it would be nice to be
able to declare a type for non-empty lists, as a subtypes of ordinary
lists:
datatype 'a list = nil | cons of 'a * 'a list
subtype 'a non_empty_list <: 'a list = cons of 'a * 'a list
Introducing subtype declarations of this kind causes a number of
problems. I am primarily interested in problems concerning the type
system and type inference.
Does anyone know if someone already has done something like this, or
where to look for possible solutions?
I have tried to use the type system (and type inference algorithm)
described by Fuh & Mishra in "Type Inference with Subtypes" [2,3], but
their system allows relations only between nullary type constructors
(like for example int<:real), and so wouldn't allow the non-empty list
type in the example above. The system could possibly be extended to
allow relations between arbitrary type constructors of the same arity
(has anybody done this?), but there are some other problems, concerning
what type to assign to constructors and how to type case expressions,
which I don't know how to solve.
I have also considered using the type system described by Mishra &
Reddy in "Declaration-free type checking" [4], which provides the kind
of subtype relation I want. The type inference algorithm described in
this paper works only for first-order languages, but the authors
mentions working on an extension for higher-order languages, to be used
in a language called FEL. Does anyone know if this work was
successful?
If you have an answer to any of these questions, or know where to look
for answers, or have any other comments, please email me! I'll post
a summary of the replies I get.
Thanks in advance.
Thomas Hallgren
---
References
[1] Luca Cardelli & Peter Wegner: "On Understanding Types, Data
Abstraction and Polymorphism", in Computing Surveys 17, 1985
[2] You-Chin Fuh & Prateek Mishra, "Type Inference with Subtypes",
Proc. European Symposium on Programming, 1988
[3] You-Chin Fuh & Prateek Mishra, "Polymorphic Subtype Inference,
Closing the Theory-Practice Gap", TAPSOFT 1989, LNCS vol 352
[4] Prateek Mishra & Uday S. Reddy, "Declaration-free type checking',
PoPL, 1984
