[Grace-core] Type Parameters and parametric type
Kim Bruce
kim at cs.pomona.edu
Mon Oct 21 23:56:08 PDT 2013
I'm in the midst of grading and making up midterms at the moment. I'll try to respond in more detail later.
On Oct 21, 2013, at 10:31 AM, Andrew P Black <black at cs.pdx.edu> wrote:
> I'm sending this to grace-core to keep everyone in the loop, but its really addressed to Tim, Kim, and James, the Type Mavens.
>
> I've deliberately stayed out of most of the types discussions, because I don't know the current literature, but I've found some aspects of the recent discussion on methods with type parameters to be disquieting.
>
> It seems to me that there are two very different situations involved in programming with types. The first is where there is a type parameter that actually provides information that would not otherwise be there, and changes the behavior of the program. An obvious example is
>
> class aList.with<T><a*: T> {
> method contains(a:T)-> Bool { ... }
> method add(a:T) { ... }
> a.do { each:T -> self.add(a) }
> }
>
> where the type parameter to the list constructor provides information that is not otherwise available (for example, if a is empty or heterogeneous), and changes the behaviour of the body of the method (which generates objects whose method have behaviors observably different form each other).
Unless you have "exact" types in the language, this doesn't stop a list from being heterogeneous. For example, if Object is the top of the type hierarchy, then aList.with<Object> can take any list as a parameter (are the "< >" around a*:T a typo?). Moreover, adding a constraint (whether matching or subtyping) just provides guarantees on the availability of operations rather than changing the semantics of the operations.
Unless there is some sort of type match operation (or cast or other dynamic check of types), the type information can generally be thrown away at run-time. That is why we decided that the semantics (except in the presence of these checks) is independent of types.
>
> The second situation is rather different. It's what the Haskell folks call parametric type and write as forall alpha: alpha -> f(alpha). The simplest case is a method like:
>
> method id (a:T) -> r:T forall T {
> return r
> }
>
> i.e., a method that simply returns its argument. The type annotations say that the result has the same type as the argument. There is no type parameter, and, in my opinion, calling this type parameterization is a bad idea, because the only parameter is a, and it's a value parameter. It's perhaps better to think of this as a use of dependent type, where the type of the result depends on the type of the argument.
>
> The behavior of the body of the method id does not depend on the value of T: it always does exactly the same thing. The point of the type annotation is to allow type inference in the context that uses the method id.
Both of these really are parametric polymorphism as in neither example does the type affect the computation. Languages like Haskell and ML are really typed languages in which static type inference inserts the type information before the code is run. Mitchell and Harper's paper "The essence of ML" (a tribute to Reynold's essence of ALGOL) http://dl.acm.org/citation.cfm?id=73563 explains ML as an explicitly typed language, for example. The main difference between these implicitly typed languages and explicitly typed languages has to do with expressiveness. Implicitly typed languages (at least those using Hindley-Milner type inference) may not have polymorphic functions as parameters, for example. If you try to extend the type inference, you soon run into problems with undecidability.
The so-called ad hoc polymorphism obtained by overloading "+", etc., on the other hand has a very different semantics that depends on the types. Type classes in Haskell are a very nice way of handling that ad hoc polymorphism that shares some features of subtypes in OO languages.
>
> I have to admit that the distinction that I've drawn between the body of the method depending on the type parameter in the first case, and not depending on the type of the parameter in the second, may be flawed. Perhaps a better distinction is that in the second case, no one would reasonably want to provide a type parameter to id (it would just obscure the program), whereas in the first case, the explicit type parameter clarifies the program.
Trivial programs always look more cluttered by type information. The value shows up mainly in more complicated programs.
>
> The if()then()else() example that we have talked about is a good use for the forall notation:
>
> method if(c:Bool)then(trueBlock:type{apply()->T})else(falseBlock:type{apply()->T}) : T forall T {
> c.ifTrue(trueBlock)ifFalse(falseBlock)
> }
>
> or maybe
>
> method if(c:Bool)then(trueBlock:type{apply()->S})else(falseBlock:type{apply()->T}) : S⊓T forall S,T {
> c.ifTrue(trueBlock)ifFalse(falseBlock)
> }
>
> where S⊓T,the meet of S and T, is the type that contains the operations that are common to both S and T. (Either the lub or the gob, depending on whether one is in the Northern or Southern Hemisphere.)
>
> I'm not sure how we would write a method like id(), or if()the()else(), in Grace at present. I'm afraid that it would be:
>
> method id <T> (a:T) -> T {
> return r
> }
>
> and
>
> method if<T> (c:Bool)then(trueBlock:{apply()->T})else(falseBlock:{apply()->T}) : T {
> c.ifTrue(trueBlock)ifFalse(falseBlock)
> }
>
> I think that this is bogus, because we don't realistically expect anyone to provide T as an argument. Saying that T is inferred when not supplied, but that it can only be inferred as dynamic, means that type information is always lost when using a method like if()then()else(). The forall notation seems to me to more clearly say that, if the program has type information for the trueBlock and the falseBlock, then it will also have it for the if()then()else().
Interestingly, if-then-else expressions have always been problems for OO languages. Java initially broke subtyping with if-then-else expressions. Now they have a very complicated semantics that actually allows them to infer types that cannot be written in the language (essentially intersection types).
Of course one solution is to just have if-then statements rather than expressions, though that would be a bit of a shame. It might be reasonable to have something like Andrew's "forall T" (though I'm not sure I like the name, I'd rather write something like "inferred T" to indicate local type inference). I suspect that would be handy for some of our other uses of blocks as well. I do agree that no one is going to want to write explicit type parameters in all of their "if" statements. It would be good to come up with a good collection of other examples (beyond if-then) so we could try to find a good comprehensive solution that we won't have to revisit again.
>
> So, please regard this a proposal for adding something like forall to Grace. The point of forall is to provide a site for the explicit declaration of what would otherwise be an unbound variable. It complements the idea of constrained types, for example in
>
> method negate(a:T) -> T forall T suchthat T has {¬(x:T)->T} {
> return ¬a
> }
>
> This says that the method negate can be applied to any object that has a ¬ operation. I'm using a CLU-like notation for matching, and a such that keyword that's not in Grace, because I don't know how to write this in Grace. (The Grace spec uses a where keyword, which is OK but less suggestive than forall … suchthat … . It also uses <: instead of matching, which is already annotated as incorrect.) So you can also regard this as a proposal for concrete syntax for constrained types.
>
> Andrew
>
> ____________________________
> Prof. Andrew P. Black
> Department of Computer Science
> Portland State University
> Oregon, USA
>
> http://www.cs.pdx.edu/~black
> Telephone: +1 503 725 2411
>
>
>
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailhost.cecs.pdx.edu/pipermail/grace-core/attachments/20131021/88b79fb9/attachment.html>
More information about the Grace-core
mailing list