Algebraic types and subclassing

Nick Kallen phantom@earthlink.net
Thu, 12 Mar 1998 15:47:10 -0800


>>    You could define OSType as a record and define an instance of toString
>>and fromString. This might very well be the best way to go, although I
have
>>to admit, the excessive usage of toString with all the standard string
>>manipulation tools might be a pain.
>
>I don't think that this is the way to go. Maybe much more overloading
>in the standard environment makes things better, e.g.:
>
>class SupportsStringOperations a where
>  index  :: Int      a -> Char
>  update :: Int Char a -> a
>  etc.


This is a very good idea. A revamp of the library would be required to make
this possible, obviously.

>>    I propose an extension to Clean's existing type class system, such
that
>>constraints and invariants and the like can be defined in classes.
Imagine,
>>if you will, a class String. Now, imagine:
>>
>>instance String OSType
>>asserts
>>    ForAll o :: OSType
>>        len o = 4
>>    ForAll i in [1..4]
>>        o.[i] <- [0..255]
>
>Someone will look into this in the future, but it is unknown so far who
>and when.

Since Clean's new funding is coming from that Radar company, which might
have an interest in writing provably correct software (because of military
applications), I would assume that these sorts of things would be in high
demand. Things like pre and post conditions, and the above "traits" or
invariants are standard elements of Formal Method systems that I believe
have had practical use in the defense industry.
    A theorem prover that could reason through the traits, pre and post
conditions, and prove that all of these things are satisfied (at compile
time) is probably a long way off. But having the run time environment
continually check these propositions (at run time) and abort when they are
false is not impractical, nor *that* big of a deal (I think), and could
obviously facilitate debugging. Moreover, the ability to have formal
specifications syntax checked, type checked, etc. (probably something
simple) is one more tool with which to show validity of software. Extending
Clean so that these specifications could be well integrated with the code
would make the programmer's job that much easier.


>>Unfortunately, this example is not great, for several reasons. Since
classes
>>only define the types of functions, a Clean extended with the above
feature
>>would still need to re-implement all the String functions. The possible
>>solutions to this problem are:
>>    1. to expand classes so that they can actually implement functions,
not
>>just define the them, (this is similar to classes that are neither
abstract
>>nor concrete in OO languages);
>>    2. allow instances or classes to inherit from other *instances*, (this
>>resembles the ability to inherit from concrete classes in OO languages);
>>    3. allow not just multiple parameter classes (coming in Clean 2.0?),
but
>>parameterLESS classes. Yes, this essentially identical to an instance, but
>>you can *inherit* from them. This would eliminate the need for the
instance
>>construct altogether. This requires (1) and eliminates the need for (2).
>
>This sounds very much like an object-oriented typing system. I must say
>that, personally, I am very interested in combinations of OO with
functional
>languages, too. I will probably look into it during my PhD.

Well, it's not intended to sound like an OO system so much. I suppose at the
essence of object orientation is state. What my suggestions do is allow for
inheritance. Type classes already allow inheritance, but it is limited
compared to a Class based language. I *think* my proposal will eliminate
that limitation, allowing functional programming to have the same extent of
inheritance that most OO languages have.
    I suggest that something to look into I think is to see if type classes
can be extended to have the abilities of Prototype-based OO languages (e.g.,
Self.). I don't know if this is possible, since prototypes seem to heavily
rely on state (more so than Classes), but it's an interesting question.
since prototypes can accurately be described as a superset to a class based
system.

>>- Make the language more orthogonal. Clean is already beautifully small,
but
>>I think it could be a bit smaller. An example is the case construct.
Perhaps
>>I'm missing something, but couldn't case be defined like:
>>    case` :: a [(a, b)] -> b | Eq a
>>    case` x l = snd (hd (filter (((==) x) o fst) l))
>
>You can't bind variables in this way and you need equality on type a (not
>needed when doing pattern-matching).

I'm not proposing eliminating pattern matching, I'm proposing elminating the
case construct, the if construct, etc.

>>- OK, this is a pipe dream, but I'd like to see first class types (i.e.,
>>type can be passed as arguments to functions). This eliminates the need
for
>>a special construct for dynamic types, special constructs for parametered
>>types (e.g., :: Parser s r :== [s] -> [([s],r)]), etc.
>
>Your example can be expressed in Clean. I don't see what else you want.

My example can be expressed in Clean, yes. But my proposed system will unify
dynamic types, parameterized types, existential types, etc. into one
construct. Dynamic types introduce all sorts of concepts like type pattern
variables, which would be subsumed by the more fundamental first class
type.Something previously impossible, like:

:: Env a b :== [(a, b)]
:: Member (Env a b) :== (a, b)

will all of the sudden be simple. When one feature can unify and simplify
numerous others, I think it is useful.

>>- Another pipe dream: reflection. I think reflection might be a useful
>>feature in some contexts.
>
>Why?

I answered this to some extent in my reply to Rinus's posting. It has proven
to be very useful in Lisp and Scheme, and I'll just direct you toward
applications written in them for conclusive proof.