[Prev][Next][Index][Thread]
Summary for Subtyping Variants
It is time to summarize the responses. Many thanks go to Andrew Wright,
Bob Harper, Thomas Hallgren, Frank Pfenning, and Stephan Diehl.
radu
------------------------------------------------------------------------
Radu Grosu
Institut fuer Informatik
Technische Universitaet Muenchen
Arcisstrasse 21 Email: grosu@informatik.tu-muenchen.de
D-80290 Muenchen Phone: ++49-89-2105-2398
Germany. Fax: ++49-89-2105-8183
------Original Question-Original Question-Original Question------------
Let me remember the original question:
What is the current state of art in (sub)typing variants?
For example consider the following data type declaration:
data I1 = Xcoord | Ycoord | Mv(Real,Real)
I would like to write something like
data I2 = Color | I1
instead of
data I3 = Color | Coerce(I1)
If one considers only non-recursive (polymorphic) data type
declarations then:
1) Are type reconstruction algorithms awailable to compute
the principal type of functions defined by using the
constructors of I2?
2) Is there any functional of the form:
I2-w :: x -> (I1 -> x) -> I2 -> x
I2-w (a)(f)(x) = case x of
Color => a
otherwise => f x
corresponding to the functional obtained for I3:
I3-when :: x -> (I1 -> x) -> I3 -> x
I3-when (a)(f)(bottom) = bottom
I3-when (a)(f)(Color) = a
I3-when (a)(f)(Coerce u) = f u
What about recursive data type declarations?
I would be grateful for relevant references.
I will post a summary if interest is shown.
radu
---------responses-responses-responses-responses-responses------------
Message 4:
>From wright@cs.rice.edu Fri Oct 15 16:35:49 1993
Date: Fri, 15 Oct 1993 16:28:59 +0100
From: wright@cs.rice.edu (Andrew Wright)
To: grosu@informatik.tu-muenchen.de
Subject: subtyping variants
As I have been designing soft type systems for a while now that incorporate
such subtyping algorithms, here is what I know:
This article, and several subsequent ones (INRIA tech reports 1430, 1431)
describe how subtyping on records and variants can be encoded into
Hindley-Milner polymorphism:
@article{Remy89,
author = "Didier R\'{e}my",
year = "1989",
month = "January",
journal = "Proceedings of the 16th Annual Symposium on Principles of Programming Languages",
pages = "77-87",
title = "Typechecking records and variants
in a natural extension of {ML}"
}
This paper describes the first design of a soft type system, based on
the Remy encoding. The underlying static type system includes
"tidy union" types, recursive types, and polymorphism:
@article{Cartwright91b,
key = "Cartwright91",
author = "Robert Cartwright and Mike Fagan",
year = "1991",
month = "June",
journal = "Proceedings of the SIGPLAN '91 Conference on Programming Language Design and Implementation",
pages = "278--292",
title = "Soft Typing"
}
Continuing in this vein, I have augmented this system in several different
ways. One extension adapts Kaes's version of Mitchell/Fuh-Mishra
structural subtyping to add real subtyping:
@article{Kaes92,
author = "Stefan Kaes",
year = "1992",
month = "June",
journal = "Proceedings of the 1992 ACM Conference on
Lisp and Functional Programming",
pages = "193-204",
title = "Type Inference in the Presence of Overloading,
Subtyping and Recursive Types"
}
A different system uses Wand-Tiuryn "shape unification" to keep recursive
types from exploding:
@inproceedings{Tiuryn93,
author = "Jerzy Tiuryn and Mitchell Wand",
year = "1993",
title = "Type Reconstruction with Recursive Types and Atomic Subtyping",
booktitle = "TAPSOFT '93: Theory and Practice of Software Development",
year = 1993,
editor = "Gaudel, M.-C. and Jouannaud, J.-P.",
pages = "686-701",
publisher = "Springer",
address = "Berlin, Heidelber, New York",
month = "apr"
}
Unfortunately, I have not yet written papers on either of these systems.
Aiken and Wimmers have designed soft type systems that solve constraints
in a different manner:
@article{Aiken93,
author = "Alexander Aiken and Edward L. Wimmers",
year = "1993",
journal = "Proceedings of the International Conference on
Functional Programming Languages
and Computer Architecture",
pages = "31-41",
title = "Type Inclusion Constraints and Type Inference"
}
I understand that they will have a paper in POPL '94.
Finally, Tim Freeman (tsf@cs.cmu.edu) has a system of "refinement types"
for ML. I don't have any references for that work.
Hope this helps! Please summarize either to the mailing list or to me
directly.
Andrew Wright
-----------------------------------------------------------------------
Message 5:
>From Robert_Harper@cs.cmu.edu Sun Oct 17 04:50:32 1993
Date: Sun, 17 Oct 1993 04:49:33 +0100
To: Radu Grosu <grosu@informatik.tu-muenchen.de>
From: Robert Harper <Robert_Harper@cs.cmu.edu>
Subject: Re: subtyping variants
Check out Jategaonkar and Mitchell's 1988 or 1989 POPL paper.
Bob Harper
-----------------------------------------------------------------------
Message 6:
>From hallgren@cs.chalmers.se Tue Oct 19 16:09:38 1993
Date: Tue, 19 Oct 1993 16:02:08 +0100
From: Thomas Hallgren <hallgren@cs.chalmers.se>
To: grosu@informatik.tu-muenchen.de
Subject: Re: subtyping variants
Hi.
On the "types" mailing list you wrote:
>> What is the current state of art in (sub)typing variants?
>> For example consider the following data type declaration:
>>
>> data I1 = Xcoord | Ycoord | Mv(Real,Real)
>>
>> I would like to write something like
>>
>> data I2 = Color | I1
>>
>> instead of
>>
>> data I3 = Color | Coerce(I1)
I have been looking for solutions to this problem. I want a type system
which allows you to form a subtype by taking a subset of the
constructors in an existing type, and/or by making the argument types
of some constructors smaller. It should also allow you to form
supertypes by starting with an existing type and adding new
constructors (like in your example above), and/or by making some
constructor argument types bigger.
For example if the type for ordinary lists is defined like
data List a = Nil | Cons a (List a)
it should be possible to define a subtype for non-empty list
subtype NEList a <: List a = Cons a (List a)
and a subtype for infinity lists:
subtype InfList a <: NEList a = Cons a (InfList a)
(the details of the concrete syntax is mostly a pragmatic problem, I
suppose...)
A problem with this approach is what type to assign to constructors.
It seems you need to make clever use of intersection types.
The constructor Cons above could be assigned the type:
Cons :: (InfList a -> InfList a) & (List a -> NEList a)
This problem goes away if you disallow subtype/supertype declarations
to change the argument types of constructors, but this also excludes
some useful(?) subtype relations, like the infinite lists as
a subtype of non-empty lists.
There is also a problem with how to type pattern matching. I think you
need union types to get a good solution.
So, I my favorite type system with subtypes at present is one where
constructors aren't assigned types in the usual way. Instead each
constructor has its own type, and larger types are form by an explicit
union operator. So, you don't need any data type declarations. All
information is inferred automatically (assuming you can distinguish
constructors from variables syntactically).
The type system I am thinking of is described by Aiken and Wimmers in [AW93].
>> If one considers only non-recursive (polymorphic) data type
>> declarations then:
>>
>> 1) Are type reconstruction algorithms awailable to compute
>> the principal type of functions defined by using the
>> constructors of I2?
>>
>> 2) Is there any functional of the form:
>>
>> I2-w :: x -> (I1 -> x) -> I2 -> x
>>
>> I2-w (a)(f)(x) = case x of
>> Color => a
>> otherwise => f x
If I remember correctly, there are no principal types in the type system
described by Aiken & Wimmers. But all expressions which are typable in
the Hindley-Milner type system are typable in Aiken & Wimmers' system.
Furthermore, the types inferred by Akien & Wimmers' type system are at
least as general as the principal Hindley-Milner typing.
Although Akien & Wimmers do not discuss pattern matching, I think the
type assigned to your functional would be something like
I2-w :: a -> (b->c) -> (b+Color) -> (a+c)
where "+" denotes the union operator. Since I2=I1+Color the type
I2-w :: x -> (I1 -> x) -> I2 -> x
is an instance of the above type (set a=c=x, b=I1).
>>
>> What about recursive data type declarations?
>>
Types are described by a type scheme together with a set of inclusion
constraints. (No constraints were needed in the type of I2-w above).
The constraints may be recursive. Recursive types are generated
automatically when needed, e.g. to type the length function:
length Nil = 0
length (Cons x xs) = 1 + length xs
length :: a -> Int where a <: Nil + Cons b a
>> I would be grateful for relevant references.
>> I will post a summary if interest is shown.
Hope this is of some use!
radu
--------------------------------------------------------------------------
Message 8:
>From Frank_Pfenning@ALONZO.TIP.CS.CMU.EDU Fri Oct 22 18:56:10 1993
To: Radu Grosu <grosu@informatik.tu-muenchen.de>
Subject: Re: subtyping variants
In-reply-to: Your message of Tue, 12 Oct 93 19:45:29 +0000.
<199310151138.AA02379@theory.lcs.mit.edu>
Date: Fri, 22 Oct 1993 17:22:12 +0100
From: Frank Pfenning <Frank_Pfenning@ALONZO.TIP.CS.CMU.EDU>
There is a paper on refinement types for ML which treats essentially the
question you are asking. Actually, one would have to slightly extend our
framework to literally allow the declarations you give, but it would be a
benign extension, I suspect. We also treat recursively defined subtypes of
datatyps.
I should also warn you that the paper is somewhat out of date. Tim Freeman's
thesis (scheduled for completion by the end of the year) contains a newer
system and many more details.
Best Regards,
- Frank Pfenning
@inproceedings ( FREEMAN91,
key = "FREEMAN91" ,
author = "Tim Freeman and Frank Pfenning" ,
title = "Refinement Types for {ML}" ,
booktitle= "Proceedings of the {SIGPLAN '91} Symposium on
Language Design and Implementation, Toronto, Ontario" ,
publisher= "ACM Press" ,
month = "June" ,
year = "1991" ,
pages = "268--277"
)
---------------------------------------------------------------------------
Message 10:
>From diehl@dfki.uni-sb.de Tue Nov 2 14:33:13 1993
From: diehl@dfki.uni-sb.de (Stephan Diehl)
Date: Tue, 2 Nov 1993 14:31:40 +0100
To: grosu@informatik.tu-muenchen.de
Subject: Re: subtyping variants
hi,
you probably know the following references, but in case you don't
you should have a look at these;
luca cardelli, a semantics of multiple inheritance
and for recursive types
cook,hill and canning, inheritance is not subtyping
that's the best i can recall these references, if
you want to have the exact references, please
write me a mail
cheers
stephan
------------------------------------------------------------------------